About

Code

Mailing list

Projects

Recent developments

• The University of Kent has funded a PhD studentship to work on CakeML. Click here for further details. Application deadline: January 15, 2015.
• A preliminary version of the CakeML Compiler Explorer is available. This web service lets you run the verified compiler and see the results of various stages of compilation.
• Our ITP'14 paper describes work on formalising the semantics and soundness of higher-order logic, including support for its principles of definition, and producing a verified implementation of the kernel of a theorem prover in CakeML. The paper describes a method for supporting definitions via translation into Stateless HOL.

  We have since developed a direct semantics for all of HOL (supporting both definitions and non-definitional context extensions including new axioms). This version was presented in our ITP'14 talk, and is described in more detail in our upcoming JAR paper (preprint).

  Paper © Springer 2014. The final publication is available at link.springer.com.

• We gave an MPhil course at Cambridge on specifying, implementing, and verifying functional programming languages.
• Our POPL'14 paper describes CakeML and a verified x86-64 implementation of a read-eval-print loop for CakeML, using the bootstrapped compiler below, a verified translation from bytecode to x86-64, and a mostly-synthesised verified runtime.

  Paper © the authors 2014. This is the authors' version of the work. It is posted here for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, here.

• We have written, verified, and bootstrapped a compiler (including lexing, parsing, type inference, and code generation) from CakeML to CakeML Bytecode. The correctness theorem covers both terminating and diverging programs, and says that the generated code behaves according to the semantics in either case. The compiler is written in HOL; we use the translator, mentioned below, to generate a verified CakeML implementation, and then evaluate the compiler on this implementation (bootstrap) to generate verified bytecode.
• One of our initial target case studies is to construct a verified CakeML version of the HOL light theorem prover. For this case study, we extended the translation tool, mentioned below, to be able to translate into stateful CakeML code. Initial results are described in our ITP'13 short paper.

  Paper © Springer 2013. The final publication is available at link.springer.com.

• We have developed a tool which translates functions from higher-order logic into CakeML. This tool is proof producing: for each translation it proves a theorem which states that the generated CakeML code correctly implements the original HOL function, according to the operational semantics of CakeML. See our ICFP'12 paper, and subsequent JFP paper, for more details.

  ICFP Paper © ACM 2012. This is the authors' version of the work. It is posted here for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, here. JFP Paper © Cambridge University Press 2014. The definitive version was published in Journal of Functional Programming, Volume 24, Issue 2-3, 2014, and is available here.

Contributors

• Rob Arthan,
• Gregorio Curello,
• Anthony Fox,
• Mike Gordon,
• David Greaves,
• John Harrison,
• Ramana Kumar,
• Robert Künnemann,
• Guoqiang Liang,
• Magnus Myreen,
• Michael Norrish,
• Scott Owens,
• Christopher Pulte,
• Konrad Slind,
• Yong Kiam Tan,
• Freek Wiedijk.