Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, and Michael Norrish.
Verified characteristic formulae for CakeML.
In European Symposium on Programming (ESOP), 2017.
[ bib |
Characteristic Formulae (CF) offer a productive, principled approach to generating verification conditions for higher-order imperative programs, but so far the soundness of CF has only been considered with respect to an informal specification of a programming language (OCaml). This leaves a gap between what is established by the verification framework and the program that actually runs. We present a fully-fledged CF framework for the formally specified CakeML programming language. Our framework extends the existing CF approach to support exceptions and I/O, thereby covering the full feature set of CakeML, and comes with a formally verified soundness theorem. Furthermore, it integrates with existing proof techniques for verifying CakeML programs. This validates the CF approach, and allows users to prove end-to-end theorems for higher-order imperative programs, from specification to language semantics, within a single theorem prover.
Armaël Guéneau, François Pottier, and Jonathan Protzenko.
The ins and outs of iteration in Mezzo.
Talk proposal for HOPE 2013, July 2013.
[ bib |
This is a talk proposal for HOPE 2013. Using iteration over a collection as a case study, we wish to illustrate the strengths and weaknesses of the prototype programming language Mezzo.
This file was generated by bibtex2html 1.98.