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

"FabULous Interoperability for ML and a Linear Language" ,
Gabriel Scherer, Max New, Nicholas Rioux and Amal Ahmed, Draft, supplementary material.

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

Workshops

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

Manuscripts

"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