The ins and outs of iteration in Mezzo. - Armaël Guéneau; François Pottier; Jonathan Protzenko (CoRR, 2013)

Verified Characteristic Formulae for CakeML. - Armaël Guéneau; Magnus O. Myreen; Ramana Kumar; Michael Norrish (ESOP, 2017)

A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. - Armaël Guéneau; Arthur Charguéraud; François Pottier (ESOP, 2018)

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. - Armaël Guéneau; Jacques-Henri Jourdan; Arthur Charguéraud; François Pottier (ITP, 2019)

Mechanized Verification of the Correctness and Asymptotic Complexity of Programs. (Vérification mécanisée de la correction et complexité asymptotique de programmes). - Armaël Guéneau (2019)

Theorems for free from separation logic specifications. - Lars Birkedal; Thomas Dinsdale-Young; Armaël Guéneau; Guilhem Jaber; Kasper Svendsen; Nikos Tzevelekos (Proc. ACM Program. Lang., 2021)

Efficient and provable local capability revocation using uninitialized capabilities. - Aïna Linn Georges; Armaël Guéneau; Thomas Van Strydonck; Amin Timany; Alix Trieu; Sander Huyghebaert; Dominique Devriese; Lars Birkedal (Proc. ACM Program. Lang., 2021)

Proving full-system security properties under multiple attacker models on capability machines: Coq mechanization. - Thomas Van Strydonck; Aïna Linn Georges; Armaël Guéneau; Alix Trieu; Amin Timany; Frank Piessens; Lars Birkedal; Dominique Devriese (Zenodo, 2021)

Proving full-system security properties under multiple attacker models on capability machines. - Thomas Van Strydonck; Aïna Linn Georges; Armaël Guéneau; Alix Trieu; Amin Timany; Frank Piessens; Lars Birkedal; Dominique Devriese (CSF, 2022)

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. - Armaël Guéneau; Johannes Hostert; Simon Spies; Michael Sammler; Lars Birkedal; Derek Dreyer (Proc. ACM Program. Lang., 2023)

The Logical Essence of Well-Bracketed Control Flow (Artifact). - Amin Timany; Armaël Guéneau; Lars Birkedal (Zenodo, 2023)

The Logical Essence of Well-Bracketed Control Flow (Artifact). - Amin Timany; Armaël Guéneau; Lars Birkedal (Zenodo, 2023)

The Logical Essence of Well-Bracketed Control Flow (Artifact). - Amin Timany; Armaël Guéneau; Lars Birkedal (Zenodo, 2023)

Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. - Aïna Linn Georges; Armaël Guéneau; Thomas Van Strydonck; Amin Timany; Alix Trieu; Dominique Devriese; Lars Birkedal (J. ACM, 2024)

Thunks and Debits in Separation Logic with Time Credits. - François Pottier; Armaël Guéneau; Jacques-Henri Jourdan; Glen Mével (Proc. ACM Program. Lang., 2024)

The Logical Essence of Well-Bracketed Control Flow. - Amin Timany; Armaël Guéneau; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Verified Purely Functional Catenable Real-Time Deques. - Jules Viennot; Arthur Wendling; Armaël Guéneau; François Pottier (CoRR, 2025)