Edwin C. Brady

According to our database, Edwin C. Brady authored at least 33 papers between 2003 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

Frex: dependently-typed algebraic simplification.

Guillaume Allais, Edwin C. Brady, Nathan Corbyn, Ohad Kammar, Jeremy Yallop

CoRR, 2023

Type Theory as a Language Workbench.

Jan de Muijnck-Hughes, Guillaume Allais, Edwin C. Brady

Proceedings of the Eelco Visser Commemorative Symposium, 2023

2021

Idris 2: Quantitative Type Theory in Practice (Artifact).

Edwin C. Brady

Dagstuhl Artifacts Ser., 2021

Idris 2: Quantitative Type Theory in Practice.

Edwin C. Brady

Proceedings of the 35th European Conference on Object-Oriented Programming, 2021

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

A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Pearl).

Jan de Muijnck-Hughes, Edwin C. Brady, Wim Vanderbauwhede

Proceedings of the 34th European Conference on Object-Oriented Programming, 2020

2019

Value-Dependent Session Design in a Dependently Typed Language.

Jan de Muijnck-Hughes, Edwin C. Brady, Wim Vanderbauwhede

Proceedings of the Proceedings Programming Language Approaches to Concurrency- and Communication-cEntric Software, 2019

2018

Subtype polymorphism à la carte via machine learning on dependent types.

Jerry Swan, Colin G. Johnson, Edwin C. Brady

Proceedings of the Companion Proceedings for the ISSTA/ECOOP 2018 Workshops, 2018

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

Type-driven Development of Concurrent Communicating Systems.

Edwin C. Brady

Comput. Sci., 2017

Automatically Proving Equivalence by Type-Safe Reflection.

Franck Slama, Edwin C. Brady

Proceedings of the Intelligent Computer Mathematics - 10th International Conference, 2017

2016

Elaborator reflection: extending Idris in Idris.

David R. Christiansen, Edwin C. Brady

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

2014

Resource-Dependent Algebraic Effects.

Edwin C. Brady

Proceedings of the Trends in Functional Programming, 2014

Idris: Implementing a Dependently Typed Programming Language.

Edwin C. Brady

Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2014

2013

Idris, a general-purpose dependently typed programming language: Design and implementation.

Edwin C. Brady

J. Funct. Program., 2013

Idris: general purpose programming with dependent types.

Edwin C. Brady

Proceedings of the 7th Workshop on Programming languages meets program verification, 2013

Sequential decision problems, dependently-typed solutions.

Nicola Botta, Cezar Ionescu, Edwin C. Brady

Proceedings of the Joint Proceedings of the MathUI, 2013

Dependent Types for Safe and Secure Web Programming.

Simon Fowler, Edwin C. Brady

Proceedings of the 25th Symposium on Implementation and Application of Functional Languages, 2013

Programming and reasoning with algebraic effects and dependent types.

Edwin C. Brady

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

The Idris Programming Language - Implementing Embedded Domain Specific Languages with Dependent Types.

Edwin C. Brady

Proceedings of the Central European Functional Programming School - 5th Summer School, 2013

2012

Resource-Safe Systems Programming with Embedded Domain Specific Languages.

Edwin C. Brady, Kevin Hammond

Proceedings of the Practical Aspects of Declarative Languages, 2012

2011

Epic - A Library for Generating Compilers.

Edwin C. Brady

Proceedings of the Trends in Functional Programming, 12th International Symposium, 2011

IDRIS ---: systems programming meets full dependent types.

Edwin C. Brady

Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, 2011

2010

Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols.

Edwin C. Brady, Kevin Hammond

Fundam. Informaticae, 2010

Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation.

Edwin C. Brady, Kevin Hammond

Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

2009

Domain Specific Languages (DSLs) for Network Protocols (Position Paper).

Saleem Bhatti, Edwin C. Brady, Kevin Hammond, James McKinna

Proceedings of the 29th IEEE International Conference on Distributed Computing Systems Workshops (ICDCS 2009 Workshops), 2009

2008

Lightweight Invariants with Full Dependent Types.

Edwin C. Brady, Christoph A. Herrmann, Kevin Hammond

Proceedings of the Nineth Symposium on Trends in Functional Programming, 2008

2007

Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types.

Edwin C. Brady, James McKinna, Kevin Hammond

Proceedings of the Eighth Symposium on Trends in Functional Programming, 2007

2006

Ivor, a Proof Engine.

Edwin C. Brady

Proceedings of the Implementation and Application of Functional Languages, 2006

A verified staged interpreter is a verified compiler.

Edwin C. Brady, Kevin Hammond

Proceedings of the Generative Programming and Component Engineering, 2006

2005

Practical implementation of a dependently typed functional programming language.

Edwin C. Brady

PhD thesis, 2005

A Dependently Typed Framework for Static Analysis of Program Execution Costs.

Edwin C. Brady, Kevin Hammond

Proceedings of the Implementation and Application of Functional Languages, 2005

2003

Inductive Families Need Not Store Their Indices.

Edwin C. Brady, Conor McBride, James McKinna

Proceedings of the Types for Proofs and Programs, International Workshop, 2003