Inductive Families Need Not Store Their Indices. - Edwin C. Brady; Conor McBride; James McKinna (TYPES, 2003)

A Dependently Typed Framework for Static Analysis of Program Execution Costs. - Edwin C. Brady; Kevin Hammond (IFL, 2005)

Practical implementation of a dependently typed functional programming language. - Edwin C. Brady (2005)

A verified staged interpreter is a verified compiler. - Edwin C. Brady; Kevin Hammond (GPCE, 2006)

Ivor, a Proof Engine. - Edwin C. Brady (IFL, 2006)

Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types. - Edwin C. Brady; James McKinna; Kevin Hammond (Trends in Functional Programming, 2007)

Lightweight Invariants with Full Dependent Types. - Edwin C. Brady; Christoph A. Herrmann; Kevin Hammond (Trends in Functional Programming, 2008)

Domain Specific Languages (DSLs) for Network Protocols (Position Paper). - Saleem Bhatti; Edwin C. Brady; Kevin Hammond; James McKinna (ICDCS Workshops, 2009)

Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation. - Edwin C. Brady; Kevin Hammond (ICFP, 2010)

Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols. - Edwin C. Brady; Kevin Hammond (Fundam. Informaticae, 2010)

IDRIS —: systems programming meets full dependent types. - Edwin C. Brady (PLPV, 2011)

Epic - A Library for Generating Compilers. - Edwin C. Brady (Trends in Functional Programming, 2011)

Resource-Safe Systems Programming with Embedded Domain Specific Languages. - Edwin C. Brady; Kevin Hammond (PADL, 2012)

The Idris Programming Language - Implementing Embedded Domain Specific Languages with Dependent Types. - Edwin C. Brady (CEFP, 2013)

Programming and reasoning with algebraic effects and dependent types. - Edwin C. Brady (ICFP, 2013)

Dependent Types for Safe and Secure Web Programming. - Simon Fowler 001; Edwin C. Brady (IFL, 2013)

Sequential decision problems, dependently-typed solutions. - Nicola Botta; Cezar Ionescu; Edwin C. Brady (CICM Workshops, 2013)

Idris: general purpose programming with dependent types. - Edwin C. Brady (PLPV, 2013)

Idris, a general-purpose dependently typed programming language: Design and implementation. - Edwin C. Brady (J. Funct. Program., 2013)

Idris: Implementing a Dependently Typed Programming Language. - Edwin C. Brady (LFMTP, 2014)

Resource-Dependent Algebraic Effects. - Edwin C. Brady (Trends in Functional Programming, 2014)

Elaborator reflection: extending Idris in Idris. - David R. Christiansen; Edwin C. Brady (ICFP, 2016)

Automatically Proving Equivalence by Type-Safe Reflection. - Franck Slama; Edwin C. Brady (CICM, 2017)

Type-driven Development of Concurrent Communicating Systems. - Edwin C. Brady (Comput. Sci., 2017)

Sequential decision problems, dependent types and generic solutions. - Nicola Botta; Patrik Jansson; Cezar Ionescu; David R. Christiansen; Edwin C. Brady (Log. Methods Comput. Sci., 2017)

Subtype polymorphism à la carte via machine learning on dependent types. - Jerry Swan; Colin G. Johnson; Edwin C. Brady (ISSTA/ECOOP Workshops, 2018)

Value-Dependent Session Design in a Dependently Typed Language. - Jan de Muijnck-Hughes; Edwin C. Brady; Wim Vanderbauwhede (PLACES@ETAPS, 2019)

A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Pearl). - Jan de Muijnck-Hughes; Edwin C. Brady; Wim Vanderbauwhede (ECOOP, 2020)

A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Artifact). - Jan de Muijnck-Hughes; Edwin C. Brady; Wim Vanderbauwhede (Dagstuhl Artifacts Ser., 2020)

Idris 2: Quantitative Type Theory in Practice. - Edwin C. Brady (ECOOP, 2021)

Idris 2: Quantitative Type Theory in Practice (Artifact). - Edwin C. Brady (Dagstuhl Artifacts Ser., 2021)

Type Theory as a Language Workbench. - Jan de Muijnck-Hughes; Guillaume Allais; Edwin C. Brady (Eelco Visser Commemorative Symposium, 2023)

Frex: dependently-typed algebraic simplification. - Guillaume Allais; Edwin C. Brady; Nathan Corbyn; Ohad Kammar; Jeremy Yallop (CoRR, 2023)

Type-Level Property Based Testing. - Thomas Ekström Hansen; Edwin C. Brady (TyDe@ICFP, 2024)