On Irrelevance and Algorithmic Equality in Predicative Type Theory - Andreas Abel 001; Gabriel Scherer (Log. Methods Comput. Sci., 2012)

GADT meet Subtyping - Gabriel Scherer; Didier Rémy (CoRR, 2012)

GADTs Meet Subtyping. - Gabriel Scherer; Didier Rémy (ESOP, 2013)

Tracking Data-Flow with Open Closure Types. - Gabriel Scherer; Jan Hoffmann 002 (LPAR, 2013)

Full Reduction in the Face of Absurdity. - Gabriel Scherer; Didier Rémy (ESOP, 2015)

Which simple types have a unique inhabitant? - Gabriel Scherer; Didier Rémy (ICFP, 2015)

Polarised Intermediate Representation of Lambda Calculus with Sums. - Guillaume Munch-Maccagnoni; Gabriel Scherer (LICS, 2015)

Multi-Focusing on Extensional Rewriting with Sums. - Gabriel Scherer (TLCA, 2015)

Which types have a unique inhabitant? : Focusing on pure program equivalence. (Quels types ont un habitant unique ? / Quels types ont un habitant unique ? : Focalisons-nous sur l'équivalence de programmes). - Gabriel Scherer (2016)

Deciding equivalence with sums and the empty type. - Gabriel Scherer (POPL, 2017)

Search for Program Structure. - Gabriel Scherer (SNAPL, 2017)

FabULous Interoperability for ML and a Linear Language. - Gabriel Scherer; Max S. New; Nicholas Rioux; Amal Ahmed 001 (CoRR, 2017)

Fab ous Interoperability for ML and a Linear Language. - Gabriel Scherer; Max S. New; Nick Rioux; Amal Ahmed 001 (FoSSaCS, 2018)

Unboxing Mutually Recursive Type Definitions in OCaml. - Simon Colin; Rodolphe Lepigre; Gabriel Scherer (CoRR, 2018)

A right-to-left type system for mutually-recursive value definitions. - Alban Reynaud; Gabriel Scherer; Jeremy Yallop (CoRR, 2018)

Merlin: a language server for OCaml (experience report). - Frédéric Bour; Thomas Refis; Gabriel Scherer (Proc. ACM Program. Lang., 2018)

Correctness of speculative optimizations with dynamic deoptimization. - Olivier Flückiger; Gabriel Scherer; Ming-Ho Yee; Aviral Goel; Amal Ahmed 001; Jan Vitek (Proc. ACM Program. Lang., 2018)

Capturing the future by replaying the past (functional pearl). - James Koppel; Gabriel Scherer; Armando Solar-Lezama (Proc. ACM Program. Lang., 2018)

Functional programming with λ-tree syntax. - Ulysse Gérard; Dale Miller 001; Gabriel Scherer (PPDP, 2019)

Functional programming with lambda-tree syntax. - Ulysse Gérard; Dale Miller 001; Gabriel Scherer (CoRR, 2019)

Dependent Pearl: Normalization by realizability. - Pierre-Évariste Dagand; Lionel Rieg; Gabriel Scherer (CoRR, 2019)

Tail Modulo Cons. - Frédéric Bour; Basile Clément; Gabriel Scherer (CoRR, 2021)

A practical mode system for recursive definitions. - Alban Reynaud; Gabriel Scherer; Jeremy Yallop (Proc. ACM Program. Lang., 2021)

Debootstrapping without Archeology - Stacked Implementations in Camlboot. - Nathanaëlle Courant; Julien Lepiller; Gabriel Scherer (Art Sci. Eng. Program., 2022)

Snapshottable Stores. - Clément Allain; Basile Clément; Alexandre Moine 001; Gabriel Scherer (Proc. ACM Program. Lang., 2024)

Coqlex: Generating Formally Verified Lexers. - Wendlasida Ouedraogo; Gabriel Scherer; Lutz Straßburger (Art Sci. Eng. Program., 2024)

Unboxed Data Constructors: Or, How cpp Decides a Halting Problem. - Nicolas Chataing; Stephen Dolan; Gabriel Scherer; Jeremy Yallop (Proc. ACM Program. Lang., 2024)

Tail Modulo Cons, OCaml, and Relational Separation Logic. - Clément Allain; Frédéric Bour; Basile Clément; François Pottier; Gabriel Scherer (Proc. ACM Program. Lang., 2025)