publis.bib

@unpublished{gueneau-pottier-protzenko-13,
  author = {Armaël Guéneau and François Pottier and Jonathan
                 Protzenko},
  title = {The ins and outs of iteration in {Mezzo}},
  note = {Talk proposal for HOPE 2013},
  month = jul,
  year = {2013},
  pdf = {http://gallium.inria.fr/~fpottier/publis/gueneau-pottier-protzenko-iteration-in-mezzo.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}.}
}
@inproceedings{gueneau-myreen-kumar-norrish-17,
  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 = {http://gallium.inria.fr/~agueneau/publis/gueneau-myreen-kumar-norrish-cf-cakeml.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. }
}
@unpublished{gueneau-chargueraud-pottier-coq-bigO,
  author = {Armaël Guéneau and Arthur Charguéraud and François Pottier},
  title = {A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification},
  year = {2018},
  pdf = {http://gallium.inria.fr/~agueneau/publis/gueneau-chargueraud-pottier-coq-bigO.pdf},
  abstract = { We present a framework for simultaneously verifying the
                  functional correctness and the worst-case asymptotic time
                  complexity of higher-order imperative programs. We build on
                  top of Separation Logic with Time Credits, embedded in an
                  interactive proof assistant. We formalize the O notation,
                  which is key to enabling modular specifications and proofs. We
                  cover the subtleties of the multivariate case, where the
                  complexity of a program fragment depends on multiple
                  parameters. We propose a way of integrating complexity bounds
                  into specifications, present lemmas and tactics that support a
                  natural reasoning style, and illustrate their use with a
                  collection of examples. },
  soft = {http://gallium.inria.fr/~agueneau/bigO/}
}