51 citations · 113 across the 16 of their papers we have counts for
17 papers
Coqlex: Generating Formally Verified Lexers
Wendlasida Ouedraogo, Gabriel Scherer, Lutz Strassburger
A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of…
Debootstrapping without Archeology: Stacked Implementations in Camlboot
Nathanaëlle Courant, Julien Lepiller, Gabriel Scherer
Context: It is common for programming languages that their reference implementation is implemented in the language itself. This requires a "bootstrap": a copy of a previous version…
Tail Modulo Cons
Frédéric Bour, Basile Clément, Gabriel Scherer
OCaml function calls consume space on the system stack. Operating systems set default limits on the stack space which are much lower than the available memory. If a program runs ou…
Functional programming with lambda-tree syntax
Ulysse Gérard, Dale Miller, Gabriel Scherer
We present the design of a new functional programming language, MLTS, that uses the lambda-tree syntax approach to encoding bindings appearing within data structures. In this appro…
Dependent Pearl: Normalization by realizability
Pierre-Évariste Dagand, Lionel Rieg, Gabriel Scherer
For those of us who generally live in the world of syntax, semantic proof techniques such as reducibility, realizability or logical relations seem somewhat magical despite -- or pe…
Proceedings ML Family / OCaml Users and Developers workshops
Sam Lindley, Gabriel Scherer
This volume contains the joint post-proceedings of the 2017 editions of the ML Family Workshop and the OCaml Users and Developers Workshop which took place in Oxford, UK, September…
Unboxing Mutually Recursive Type Definitions in OCaml
Simon Colin, Rodolphe Lepigre, Gabriel Scherer
In modern OCaml, single-argument datatype declarations (variants with a single constructor, records with a single field) can sometimes be `unboxed'. This means that their memory re…
A Practical Mode System for Recursive Definitions
Alban Reynaud, Gabriel Scherer, Jeremy Yallop
In call-by-value languages, some mutually-recursive value definitions can be safely evaluated to build recursive functions or cyclic data structures, but some definitions (let rec…
Merlin: A Language Server for OCaml (Experience Report)
Frédéric Bour, Thomas Refis, Gabriel Scherer
We report on the experience of developing Merlin, a language server for the OCaml programming language in development since 2013. Merlin is a daemon that connects to your favourite…
Correctness of Speculative Optimizations with Dynamic Deoptimization
Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee +3
High-performance dynamic language implementations make heavy use of speculative optimizations to achieve speeds close to statically compiled languages. These optimizations are typi…
Capturing the Future by Replaying the Past
James Koppel, Gabriel Scherer, Armando Solar-Lezama
Delimited continuations are the mother of all monads! So goes the slogan inspired by Filinski's 1994 paper, which showed that delimited continuations can implement any monadic effe…
FabULous Interoperability for ML and a Linear Language
Gabriel Scherer, Max New, Nick Rioux +1
Instead of a monolithic programming language trying to cover all features of interest, some programming systems are designed by combining together simpler languages that cooperate…
Deciding equivalence with sums and the empty type
Gabriel Scherer
The logical technique of focusing can be applied to the -calculus; in a simple type system with atomic types and negative type formers (functions, products, the unit type), its…
Tracking Data-Flow with Open Closure Types
Gabriel Scherer, Jan Hoffmann
Type systems hide data that is captured by function closures in function types. In most cases this is a beneficial design that favors simplicity and compositionality. However, some…
GADTs meet subtyping
Gabriel Scherer, Didier Rémy
While generalized algebraic datatypes (\GADTs) are now considered well-understood, adding them to a language with a notion of subtyping comes with a few surprises. What does it mea…
GADT meet Subtyping
Gabriel Scherer, Didier Rémy
While generalized abstract datatypes (GADT) are now considered well-understood, adding them to a language with a notion of subtyping comes with a few surprises. What does it mean f…
On Irrelevance and Algorithmic Equality in Predicative Type Theory
Andreas Abel, Gabriel Scherer
Dependently typed programs contain an excessive amount of static terms which are necessary to please the type checker but irrelevant for computation. To separate static and dynamic…