- Type-driven Development with Idris, Edwin Brady
Book to be published by Manning late 2016 (estimated), available via the Manning Early Access Program
- Resource-dependent Algebraic Effects, Edwin Brady
Revised version to appear in proceedings of TFP 2014
- Dependent Types for Safe and Secure Web Programming, Simon Fowler and Edwin Brady
In proceedings of IFL 2013
- Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation, Edwin Brady
In Journal of Functional Programming, October 2013.
- 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.