Generative Programming for Embedded Systems

Aims

The aim of this project is to develop formally-based techniques capable of specifying and verifying the functional and extra-functional properties of automatically generated programs. The work is undertaken in the context of the domain-specific research language Hume, a language targeting real-time embedded systems and designed to support high-level programming constructs, whilst guaranteeing that well-typed programs satisfy strong time and space resource bounds.

The final report is available.

People

• Kevin Hammond
• Edwin Brady

Publications and Drafts

• Project final report.
• Correct by Construction Concurrency
  Edwin Brady and Kevin Hammond, submitted, October 2008. With an accompanying implementation in Idris.
• Idris, a language with dependent types
  Edwin Brady, in draft proceedings of IFL 2008.
• Lightweight Invariants with Full Dependent Types
  Edwin Brady, Christoph Herrmann and Kevin Hammond, to appear in proceedings of TFP 2008
• Formally-Based Resource Usage Verification using a Dependently-Typed MetaLanguage to Specify and Implement Domain-Specific Languages.
  Edwin Brady and Kevin Hammond, unpublished draft, 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.
• Embedding a Language with Certified Size Constraints in a Dependently Typed Metalanguage,
  Edwin Brady, Kevin Hammond and James McKinna, unpublished draft, July 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.
• Phase Distinctions In The Compilation Of Epigram
  James McKinna and Edwin Brady, unpublished draft, November 2005.

Software

• Idris, an experimental language with full dependent types.
• Ivor, a type theory based theorem proving engine with a Haskell API.
• Epic, a supercombinator compiler.