| 2026 | FORTE | Harmony in Rocq. | Savan Kan, Sergue Lenglet |
| 2024 | FORTE | Leaf-First Zipper Semantics. | Sergue Lenglet, Alan Schmitt |
| 2024 | FSCD | Optimizing a Non-Deterministic Abstract Machine with Environments. | Malgorzata Biernacka, Dariusz Biernacki, Sergue Lenglet, Alan Schmitt |
| 2022 | CONCUR | Non-Deterministic Abstract Machines. | Malgorzata Biernacka, Dariusz Biernacki, Sergue Lenglet, Alan Schmitt |
| 2022 | CPP | Certified abstract machines for skeletal semantics. | Guillaume Ambal, Sergue Lenglet, Alan Schmitt |
| 2022 | PPDP | Certified Derivation of Small-Step From Big-Step Skeletal Semantics. | Guillaume Ambal, Sergue Lenglet, Alan Schmitt, Camille Nos |
| 2020 | FSCD | A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers. | Dariusz Biernacki, Sergue Lenglet, Piotr Polesiuk |
| 2019 | FOSSACS | A Complete Normal-Form Bisimilarity for State. | Dariusz Biernacki, Sergue Lenglet, Piotr Polesiuk |
| 2018 | CPP | HOπ in Coq. | Sergue Lenglet, Alan Schmitt |
| 2017 | LICS | Fully abstract encodings of λ-calculus in HOcore through abstract machines. | Malgorzata Biernacka, Dariusz Biernacki, Sergue Lenglet, Piotr Polesiuk, Damien Pous, Alan Schmitt |
| 2015 | CONCUR | Howe's Method for Contextual Semantics. | Sergue Lenglet, Alan Schmitt |
| 2014 | POPL | Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation. | Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergue Lenglet, Luca Padovani |
| 2013 | APLAS | Environmental Bisimulations for Delimited-Control Operators. | Dariusz Biernacki, Sergue Lenglet |
| 2012 | ESOP | Expansion for Universal Quantifiers. | Sergue Lenglet, Joe B. Wells |
| 2012 | FLOPS | Normal Form Bisimulations for Delimited-Control Operators. | Dariusz Biernacki, Sergue Lenglet |
| 2012 | FOSSACS | Applicative Bisimulations for Delimited-Control Operators. | Dariusz Biernacki, Sergue Lenglet |
| 2011 | PPDP | Typing control operators in the CPS hierarchy. | Malgorzata Biernacka, Dariusz Biernacki, Sergue Lenglet |
| 2009 | CONCUR | Howe's Method for Calculi with Passivation. | Sergue Lenglet, Alan Schmitt, Jean-Bernard Stefani |
| 2009 | FOSSACS | Normal Bisimulations in Calculi with Passivation. | Sergue Lenglet, Alan Schmitt, Jean-Bernard Stefani |
| 2006 | MFCS | A Core Calculus for Scala Type Checking. | Vincent Cremet, Franois Garillot, Sergue Lenglet, Martin Odersky |