Gabriel Scherer

41 papers A* 2A 3B 2C 1Journal 29Unranked 2

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic. Proc. ACM Program. Lang. Clément Allain, Gabriel Scherer
2025	J	`jnl`	Omnidirectional type inference for ML: principality any way. CoRR Alistair O'Brien, Didier Rémy, Gabriel Scherer
2025	J	`jnl`	Tail Modulo Cons, OCaml, and Relational Separation Logic. Proc. ACM Program. Lang. Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer
2025	J	`jnl`	The free bifibration on a functor. CoRR Bryce Clarke, Gabriel Scherer, Noam Zeilberger
2024	J	`jnl`	Coqlex: Generating Formally Verified Lexers. Art Sci. Eng. Program. Wendlasida Ouedraogo, Gabriel Scherer, Lutz Straßburger
2024	J	`jnl`	Snapshottable Stores. Proc. ACM Program. Lang. Clément Allain, Basile Clément, Alexandre Moine, Gabriel Scherer
2024	J	`jnl`	Tail Modulo Cons, OCaml, and Relational Separation Logic. CoRR Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer
2024	J	`jnl`	Unboxed Data Constructors: Or, How cpp Decides a Halting Problem. Proc. ACM Program. Lang. Nicolas Chataing, Stephen Dolan, Gabriel Scherer, Jeremy Yallop
2023	J	`jnl`	Coqlex: Generating Formally Verified Lexers. CoRR Wendlasida Ouedraogo, Gabriel Scherer, Lutz Straßburger
2023	J	`jnl`	Unboxed data constructors - or, how cpp decides a halting problem. CoRR Nicolas Chataing, Stephen Dolan, Gabriel Scherer, Jeremy Yallop
2022	J	`jnl`	Debootstrapping without Archeology - Stacked Implementations in Camlboot. Art Sci. Eng. Program. Nathanaëlle Courant, Julien Lepiller, Gabriel Scherer
2022	J	`jnl`	Debootstrapping without Archeology: Stacked Implementations in Camlboot. CoRR Nathanaëlle Courant, Julien Lepiller, Gabriel Scherer
2021	J	`jnl`	A practical mode system for recursive definitions. Proc. ACM Program. Lang. Alban Reynaud, Gabriel Scherer, Jeremy Yallop
2021	J	`jnl`	Tail Modulo Cons. CoRR Frédéric Bour, Basile Clément, Gabriel Scherer
2019	J	`jnl`	Dependent Pearl: Normalization by realizability. CoRR Pierre-Évariste Dagand, Lionel Rieg, Gabriel Scherer
2019	J	`jnl`	Functional programming with lambda-tree syntax. CoRR Ulysse Gérard, Dale Miller, Gabriel Scherer
2019	C	`conf`	Functional programming with λ-tree syntax. PPDP Ulysse Gérard, Dale Miller, Gabriel Scherer
2019	—	`ed.`	Proceedings ML Family / OCaml Users and Developers workshops, ML/OCaml 2017, Oxford, UK, 7th September 2017. ML/OCaml Sam Lindley, Gabriel Scherer
2018	J	`jnl`	A right-to-left type system for mutually-recursive value definitions. CoRR Alban Reynaud, Gabriel Scherer, Jeremy Yallop
2018	J	`jnl`	Capturing the future by replaying the past (functional pearl). Proc. ACM Program. Lang. James Koppel, Gabriel Scherer, Armando Solar-Lezama
2018	J	`jnl`	Correctness of speculative optimizations with dynamic deoptimization. Proc. ACM Program. Lang. Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, Jan Vitek
2018	B	`conf`	Fab ous Interoperability for ML and a Linear Language. FoSSaCS Gabriel Scherer, Max S. New, Nick Rioux, Amal Ahmed
2018	J	`jnl`	Merlin: A Language Server for OCaml (Experience Report). CoRR Frédéric Bour, Thomas Refis, Gabriel Scherer
2018	J	`jnl`	Merlin: a language server for OCaml (experience report). Proc. ACM Program. Lang. Frédéric Bour, Thomas Refis, Gabriel Scherer
2018	J	`jnl`	Unboxing Mutually Recursive Type Definitions in OCaml. CoRR Simon Colin, Rodolphe Lepigre, Gabriel Scherer
2017	J	`jnl`	Correctness of Speculative Optimizations with Dynamic Deoptimization. CoRR Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, Jan Vitek
2017	A*	`conf`	Deciding equivalence with sums and the empty type. POPL Gabriel Scherer
2017	J	`jnl`	FabULous Interoperability for ML and a Linear Language. CoRR Gabriel Scherer, Max S. New, Nicholas Rioux, Amal Ahmed
2017	—	`conf`	Search for Program Structure. SNAPL Gabriel Scherer
2016	J	`jnl`	Deciding equivalence with sums and the empty type. CoRR Gabriel Scherer
2016	—	`—`	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
2015	A	`conf`	Full Reduction in the Face of Absurdity. ESOP Gabriel Scherer, Didier Rémy
2015	—	`conf`	Multi-Focusing on Extensional Rewriting with Sums. TLCA Gabriel Scherer
2015	A*	`conf`	Polarised Intermediate Representation of Lambda Calculus with Sums. LICS Guillaume Munch-Maccagnoni, Gabriel Scherer
2015	A	`conf`	Which simple types have a unique inhabitant? ICFP Gabriel Scherer, Didier Rémy
2013	A	`conf`	GADTs Meet Subtyping. ESOP Gabriel Scherer, Didier Rémy
2013	J	`jnl`	GADTs meet subtyping CoRR Gabriel Scherer, Didier Rémy
2013	B	`conf`	Tracking Data-Flow with Open Closure Types. LPAR Gabriel Scherer, Jan Hoffmann
2013	J	`jnl`	Tracking Data-Flow with Open Closure Types. CoRR Gabriel Scherer, Jan Hoffmann
2012	J	`jnl`	GADT meet Subtyping CoRR Gabriel Scherer, Didier Rémy
2012	J	`jnl`	On Irrelevance and Algorithmic Equality in Predicative Type Theory Log. Methods Comput. Sci. Andreas Abel, Gabriel Scherer