author = {Armaël Guéneau and François Pottier and Jonathan
  title = {The ins and outs of iteration in {Mezzo}},
  note = {Talk proposal for HOPE 2013},
  month = jul,
  year = {2013},
  pdf = {},
  abstract = {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}.}
  author = {Armaël Guéneau and Magnus O. Myreen and Ramana Kumar and Michael Norrish},
  title = {Verified Characteristic Formulae for {CakeML}},
  booktitle = {European Symposium on Programming (ESOP)},
  year = {2017},
  pdf = {},
  abstract = { 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. }

This file was generated by bibtex2html 1.98.