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. }
  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},
  booktitle = {European Symposium on Programming (ESOP)},
  year = {2018},
  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 = {}
  author = {Armaël Guéneau},
  title = {Procrastination, a proof engineering technique},
  note = {Talk proposal for the FLoC Coq Workshop 2018},
  month = apr,
  year = {2018},
  pdf = {},
  abstract = {We present a small Coq library for collecting side conditions and deferring their proof.}
  author = {Armaël Guéneau and Jacques-Henri Jourdan and
                 Arthur Charguéraud and François Pottier},
  title = {Formal Proof and Analysis of an Incremental Cycle
                 Detection Algorithm},
  note = {Submitted},
  month = feb,
  year = {2019},
  url = {},
  abstract = {
    We exploit Separation Logic with Time Credits to verify
    the correctness and worst-case amortized asymptotic complexity of a
    state-of-the-art incremental cycle detection algorithm.