(Last page update: May 2024)
"Tail Modulo Cons, OCaml, and Relational Separation Logic"
,
Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer,
POPL 2025
"Snapshottable Stores"
,
Clément Allain, Basile Clément, Alexandre Moine, Gabriel Scherer,
ICFP 2024
"Unboxed data constructors -- or, how cpp decides a halting problem"
,
Nicolas Chataing, Stephen Dolan, Gabriel Scherer, Jeremy Yallop,
POPL 2024
"Coqlex: Generating formally verified lexers"
,
Wendlasida Ouedraogo, Gabriel Scherer, Lutz Straßburger,
Programming 2023
"Boxroot, fast movable GC roots for a better FFI"
,
Guillaume Munch-Maccagnoni, Gabriel Scherer,
Draft, 2022-current
"Debootstrapping without Archeology: Stacked implementations in Camlboot"
,
Nathanaëlle Courant, Julien Lepiller, and Gabriel Scherer,
Programming 2022
"Dependent Pearl: Normalization by realizability"
,
Pierre-Évariste Dagand, Lionel Rieg and Gabriel Scherer,
Draft, 2018-2021
"A right-to-left type system for mutually-recursive value definitions"
,
Alban Reynaud, Gabriel Scherer and Jeremy Yallop,
POPL 2021
"Functional programming with lambda-tree syntax"
,
Ulysse Gérard, Dale Miller and Gabriel Scherer,
PPDP 2019.
"Experience report: Merlin, a Language Server for OCaml"
,
Frédéric Bour, Thomas Refis and Gabriel Scherer,
ICFP 2018.
"Capturing the Future by Replaying the Past -- Functional Pearl"
,
James Koppel, Gabriel Scherer and Armando Solar-Lezama,
ICFP 2018.
"FabULous Interoperability for ML and a Linear Language"
,
Gabriel Scherer, Max New, Nicholas Rioux and Amal Ahmed,
FoSSaCS 2018.
(supplementary material)
"Correctness of Speculative Optimizations with Dynamic Deoptimization"
,
Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed and Jan Vitek,
POPL 2018.
"Deciding equivalence with sums and the empty type"
,
Gabriel Scherer,
POPL 2017.
"Which simple types have a unique inhabitant?"
,
Gabriel Scherer and Didier Rémy,
ICFP 2015.
"Polarised Intermediate Representation of Lambda Calculus with Sums"
,
Guillaume Munch-Maccagnoni and Gabriel Scherer,
LICS 2015.
"Multi-focusing on extensional rewriting with sums"
,
Gabriel Scherer,
TLCA 2015.
"Full reduction in the face of absurdity"
,
Gabriel Scherer and Didier Rémy,
ESOP 2015.
"Tracking Data-Flow with Open Closure Types"
,
Gabriel Scherer and Jan Hoffmann,
LPAR'19 -- 2013.
"GADTs meet subtyping"
,
Gabriel Scherer and Didier Rémy,
ESOP 2013.
"On Irrelevance and Algorithmic Equality in Predicative Type Theory"
,
Andreas Abel and Gabriel Scherer,
LMCS 2012.
« Correct tout seul, sûr à plusieurs »
,
Clément Allain, Gabriel Scherer,
JFLA 2024
"Backtracking reference stores"
,
Camille Noûs, Gabriel Scherer,
JFLA 2023
"Tail Modulo Cons"
,
Frédéric Bour, Basile Clément, Gabriel Scherer,
JFLA 2021
"Search for Program Structure"
,
Gabriel Scherer,
SNAPL 2017.
"Unboxing Mutually Recursive Type Definitions in OCaml"
,
Simon Colin, Rodolphe Lepigre and Gabriel Scherer,
JFLA 2019
"Normalization by realizability also evaluates"
,
Pierre-Évariste Dagand and Gabriel Scherer,
JFLA 2015.
« Macaque: Interrogation sûre et flexible de bases de données depuis OCaml »
,
Gabriel Scherer and Jérôme Vouillon,
JFLA 2010.
"The combinatorics of free bifibrations"
,
Bryce Clarke, Gabriel Scherer, Noam Zeilberger,
CLA 2023
"Boxroot, fast movable GC roots for a better FFI"
,
Guillaume Munch-Maccagnoni, Gabriel Scherer,
ML workshop 2022.
"An OCaml use case for strong call-by-need reduction"
,
Gabriel Scherer, Nathanaëlle Courant,
ML Workshop 2022.
"Unfolding ML datatype declarations without loops"
,
Nicolas Chataing, Gabriel Scherer,
ML Workshop 2021.
"Frozen inference constraints for type-directed disambiguation"
,
Olivier Martinot, Gabriel Scherer,
ML Workshop 2021.
"Quantified Applicatives – API design for type-inference constraints"
,
Olivier Martinot, Gabriel Scherer,
ML workshop 2020.
"Translation-validation of a pattern-matching compiler"
,
Francesco Mecca, Gabriel Scherer,
ML workshop 2020.
"Ambiguous pattern variables"
,
Gabriel Scherer, Luc Maranget, and Thomas Réfis,
ML workshop 2016. (talk)
"Well-typed generic smart-fuzzing for APIs"
,
Thomas Braibant, Jonathan Protzenko, and Gabriel Scherer,
ML Workshop 2014. (long version)
"Deciding unique inhabitants with sums"
,
Gabriel Scherer,
TYPES 2014. (talk)
"Github Pull Requests for OCaml development: a field report"
,
Gabriel Scherer,
OCaml Workshop 2014.
"Mining opportunities for unique inhabitants in dependent programs"
,
Gabriel Scherer,
Dependently Typed Programming (DTP) 2013. (talk)
"GADTs meet subtyping"
,
Gabriel Scherer and Didier Rémy,
ML workshop 2012.
"Which types have a unique inhabitant?
Focusing on pure program equivalence"
,
PhD thesis, 2016
(webpage)
"Suites de Goodstein et incomplétude de l'arithmétique de Peano"
,
Gabriel Scherer et Silvain Rideau,
Juin 2009