"Which simple types have a unique inhabitant?"
,
Gabriel Scherer and Didier Rémy,
Draft.
"On Irrelevance and Algorithmic Equality in Predicative Type Theory"
,
Andreas Abel and Gabriel Scherer,
LMCS 2012.
Experience Report: debootstraping the OCaml compiler
,
Anonymous authors,
Draft, 2018-2021.
Dependent Pearl: Normalization by realizability
,
Pierre-Évariste Dagand, Lionel Rieg and Gabriel Scherer,
Draft, 2018-2021.
Tail Modulo Cons
,
Frédéric Bour, Basile Clément, Gabriel Scherer,
JFLA 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.
Unboxing Mutually Recursive Type Definitions in OCaml
,
Simon Colin, Rodolphe Lepigre and Gabriel Scherer,
JFLA 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.
"Search for Program Structure"
,
Gabriel Scherer
SNAPL 2017.
"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.
"Normalization by realizability also evaluates"
,
Pierre-Évariste Dagand and Gabriel Scherer,
JFLA 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.
"Macaque: Interrogation sûre et flexible de bases de données depuis OCaml"
,
Gabriel Scherer and Jérôme Vouillon,
JFLA 2010.
"Unfolding ML datatype declarations without loops"
,
Nicolas Chataing, Gabriel Scherer,
Draft, 2021
"Frozen inference constraints for type-directed disambiguation"
,
Olivier Martinot, Gabriel Scherer,
Draft, 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