85 citations · 95 across the 4 of their papers we have counts for
4 papers
Invertible Syntax without the Tuples (Functional Pearl)
Mathieu Boespflug, Arnaud Spiwack
In the seminal paper Functional unparsing, Olivier Danvy used continuation passing to reanalyse printf-like format strings as combinators. In the intervening decades, the conversat…
Linear Haskell: practical linearity in a higher-order polymorphic language
Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton +2
Linear type systems have a long and storied history, but not a clear path forward to integrate with existing languages such as OCaml or Haskell. In this paper, we study a linear ty…
Multi-level Contextual Type Theory
Mathieu Boespflug, Brigitte Pientka
Contextual type theory distinguishes between bound variables and meta-variables to write potentially incomplete terms in the presence of binders. It has found good use as a framewo…
From Self-Interpreters to Normalization by Evaluation
Mathieu Boespflug
We characterize normalization by evaluation as the composition of a self-interpreter with a self-reducer using a special representation scheme, in the sense of Mogensen (1992). We…