3 citations · 5 across the 6 of their papers we have counts for
9 papers
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…