- Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation, Edwin Brady
Accepted for publication in Journal of Functional Programming, August 2013. To appear.
- Programming and Reasoning with Algebraic Effects and Dependent Types, Edwin Brady
Revised version to appear in proceedings of ICFP 2013
Sequential decision problems, dependently typed solutions, Nicola Botta, Cezar Ionescu and Edwin Brady
In proceedings of PLMMS 2013
- Programming in Idris: a tutorial, Edwin Brady
- Resource-safe Systems Programming with Embedded Domain Specific Languages, Edwin Brady and Kevin Hammond
In proceedings of PADL 2012
Epic – A Library for Generating Compilers, Edwin Brady
In proceedings of TFP 2011
- Idris – Systems Programming meets Full Dependent Types, Edwin Brady
In proceedings of PLPV 2011.
- Scrapping your Inefficient Engine: using Partial Evaluation to Improve Domain-Specific Language Implementation, Edwin Brady and Kevin Hammond
In proceedings of ICFP 2010.
- Correct-by-Construction Concurrency: using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols, Edwin Brady and Kevin Hammond
In Fundamenta Informaticae, Volume 102, 2010.
- Domain Specific Languages (DSLs) for Network Protocols, Saleem Bhatti, Edwin Brady, Kevin Hammond and James McKinna.
In NGNA 2009.
- Lightweight Invariants with Full Dependent Types, Edwin Brady, Christoph Herrmann and Kevin Hammond.
In proceedings of TFP 2008.
- Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types, Edwin Brady, James McKinna and Kevin Hammond.
In proceedings of TFP 2007.
- Ivor, a Proof Engine, Edwin Brady.
In proceedings of IFL 2006.
- A Verified Staged Interpreter is a Verified Compiler (Multi-stage Programming with Dependent Types), Edwin Brady and Kevin Hammond.
In proceedings of GPCE 2006.
- A Dependently Typed Framework For Static Analysis Of Program Execution Costs, Edwin Brady and Kevin Hammond
In proceedings of IFL 2005.
- Practical Implementation of a Dependently Typed Functional Programming Language,
PhD thesis, Durham University, 2005.
- Inductive Families Need Not Store Their Indices, Edwin Brady, Conor McBride and James McKinna.
In proceedings of TYPES 2003.