| 2024 | FSCD | On the Logical Structure of Some Maximality and Well-Foundedness Principles Equivalent to Choice Principles. | Hugo Herbelin, Jad Koleilat |
| 2021 | LICS | On the logical structure of choice and bar induction principles. | Nuria Brede, Hugo Herbelin |
| 2020 | LICS | A calculus of expandable stores: Continuation-and-environment-passing style translations. | Hugo Herbelin, tienne Miquey |
| 2018 | FOSSACS | Realizability Interpretation and Normalization of Typed Call-by-Need \lambda -calculus with Control. | tienne Miquey, Hugo Herbelin |
| 2014 | POPL | 30 years of research and development around Coq. | Grard P. Huet, Hugo Herbelin |
| 2012 | FLOPS | Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts. | Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, Alexis Saurin |
| 2012 | LICS | A Constructive Proof of Dependent Choice, Compatible with Classical Logic. | Hugo Herbelin |
| 2010 | LICS | An Intuitionistic Logic that Proves Markov's Principle. | Hugo Herbelin |
| 2010 | LICS | Equality Is Typable in Semi-full Pure Type Systems. | Vincent Siles, Hugo Herbelin |
| 2009 | WoLLIC | Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus. | Hugo Herbelin, Gyesik Lee |
| 2008 | POPL | An approach to call-by-name delimited continuations. | Hugo Herbelin, Silvia Ghilezan |
| 2004 | ICFP | A type-theoretic foundation of continuations and prompts. | Zena M. Ariola, Hugo Herbelin, Amr Sabry |
| 2003 | ICALP | Minimal Classical Logic and Control Operators. | Zena M. Ariola, Hugo Herbelin |
| 2000 | ICFP | The duality of computation. | Pierre-Louis Curien, Hugo Herbelin |
| 1998 | FLOPS | Computing with Abstract Bhm Trees. | Pierre-Louis Curien, Hugo Herbelin |
| 1996 | LICS | Game Semantics & Abstract Machines. | Vincent Danos, Hugo Herbelin, Laurent Regnier |
| 1994 | CSL | A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure. | Hugo Herbelin |