Idris 2: Quantitative Type Theory in Practice, Edwin Brady, ECOOP 2021

• There is a corresponding artifact available
• There is also a recording of the conference talk

A Framework for Resource Dependent EDSLs in a Dependently Typed Language, Jan de Muijnck-Hughes, Wim Vanderbauwhede and Edwin Brady, ECOOP 2020

Value Dependent Session Design in a Dependently Typed Language, PLACES 2019

Automatically Proving Equivalence by Type-Safe Reflection, Franck Slama and Edwin Brady, Conference on Intelligent Computer Mathematics (CICM) 2017

Type-driven Development of Concurrent Communicating Systems, Edwin Brady, Computer Science Journal (AGH University of Science and Technology) 2017

Sequential decision problems, dependent types and generic solutions, Nicola Botta, Patrik Jansson, Cezar Ionescu, David Christiansen and Edwin Brady Logical Methods in Computer Science, Volume 13, Issue 1 (March 2017)

Elaboration Reflection: Extending Idris in Idris, David Christiansen and Edwin Brady In proceedings of ICFP 2016

Resource-dependent Algebraic Effects, Edwin Brady 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 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 January 2012

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 Next Generation Network Architectures (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.

Inductive Families Need Not Store Their Indices, Edwin Brady, Conor McBride and James McKinna. In proceedings of TYPES 2003.