Edwin Brady

Research Interests

I am a SICSA Advanced Research Fellow, interested in type theory, dependently typed functional programming, compilers and domain specific languages (DSLs). I am currently working on the implementation of DSLs for stateful, resource-aware programming, especially for correct network protocol design and implementation, using Idris, a dependently typed functional programming language.

I previously worked on the EPSRC-funded project Generative Programming for Embedded Systems; you can see the details, including a final report and a list of publications.

You can see my publications and drafts below, occasionaly some talks, as well as some of the software I've written. You can also see some twittering, if you like that sort of thing. Also new is the Functional Programming Group Blog.

The picture was taken by James Caldwell on 3rd May 2008, at the top of Stob Coire Sgreamhach.

• Scrapping your Inefficient Engine: using Partial Evaluation to Improve Domain-Specific Language Implementation, Edwin Brady and Kevin Hammond
  January 2010.

Publications

• Domain Specific Languages (DSLs) for Network Protocols, Saleem Bhatti, Edwin Brady, Kevin Hammond and James McKinna
  In NGNA 2009.
  Slides available.
• 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. With accompanying Proof scripts.
• 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, Edwin Brady
  PhD thesis, Durham University, 2005. Also a PDF.
• Inductive Families Need Not Store Their Indices, Edwin Brady, Conor McBride and James McKinna
  In proceedings of TYPES 2003.

Drafts and Work in Progress

• Ensuring Correct-by-Construction Resource Usage by using Full-Spectrum Dependent Types , Edwin Brady and Kevin Hammond
  March 2009.
  With accompanying implementation in Idris.
• Correct by Construction Concurrency, Edwin Brady and Kevin Hammond,
  Submitted, October 2008. With an accompanying implementation in Idris.
• Idris, a language with dependent types (Extended Abstract), Edwin Brady
  In draft proceedings of IFL 2008.
• Formally-Based Resource Usage Verification using a Dependently-Typed MetaLanguage to Specify and Implement Domain-Specific Languages, Edwin Brady and Kevin Hammond
  Draft, November 2007.
• Embedding a Language with Certified Size Constraints in a Dependently Typed Metalanguage, Edwin Brady, Kevin Hammond and James McKinna
  Draft, July 2006.
• Phase Distinctions In The Compilation Of Epigram, James McKinna and Edwin Brady
  Draft, November 2005.

• Domains Specific Language Implementation with Dependent Types
• DSLs for Network Protocols, presented at NGNA 2009

• Idris, an experimental language with full dependent types.
• Ivor, a type theory based theorem proving engine with a Haskell API.
• A Supercombinator Compiler, intended as a back end for Epigram.

Some other toys:

• A simple functional language with a built-in theorem prover, implemented with the help of Ivor.
• An implementation of the simply typed lambda calculus in Ivor, with a Haskell driver.
• An SK calculus evaluator, being a small experiment in modelling partial functions in Coq.

Other Stuff

• I play Go, and you should give it a try too. I'm about 3 kyu, which means I'm barely competent, but average by British standards. There is now a St Andrews Go Club.
• I have a LaTeX thesis document class for Durham University, which should also be easy to modify for use for other universities' thesis guidelines.
• I'm afraid I also perpetrated the whitespace programming language.
• I've just rediscovered this unusual method for computing pi that I wrote while an undergraduate, and no doubt meant to be doing something else...

Edwin Brady -- eb@cs.st-andrews.ac.uk -- 14th October 2009