Gabriel Scherer: Publications

My picture

Journal articles

"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.

Conference articles

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.


"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