I am a young researcher in computer science, currently working as a postdoctoral researcher at Inria in the Deducteam project, hosted by the LSV at ENS Cachan (now ENS ParisSaclay). Although my interests are diverse, my main area of expertise is the application of semantic techniques to programming languages and proof assistants. I also make a point of backing my theoretical work with a substantial amount of implementation, for which I developed specific tools and libraries in OCaml. I most recently proposed a new implementation of the Dedukti logical framework called Lambdapi, which enables the development of mathematical proofs in the system, while the original Dedukti was only usable as the target of translations.
Between 2014 and 2017 I was a PhD student at the LAMA (LAboratoire de MAthématiques), in Chambéry (in the French Alps). During that time, I mainly worked with Christophe Raffalli and Pierre Hyvernat, although my official advisor was Karim Nour. In my thesis work, I designed the theoretical foundation of (and implemented) the PML₂ language, which mixes programming and program certification in a uniform (MLlike) setting.
Research
The most personal part of my research project revolves around the design and implementation of PML₂ [PML2], which is a programming language with support for program certification. The main idea is to extend an MLlike language, similar to OCaml or SML, with the means of specifying and proving equational properties of its own programs. We thus combine the flexibility of a fullfledged programming language with the great specification power of a proof assistant. Although the development of PML₂ is one of my leading goals, it is first and foremost an excuse for attacking difficult theoretical and practical questions. Of course, the answers to such questions go beyond the scope of PML₂, although I often present them in its light. In this sense, the implementation of the language can be seen as an experimentation platform for driving theoretical investigations. I strongly believe that mixing abstract theoretical questions with pragmatic implementation aspects mutually benefits to both fields. For example, the type system given in [Lepigre2016] could not be implemented in a natural way due to the fact that PML₂ is a socalled Currystyle language. As a result, we developed a new framework for dealing with such languages, including new techniques using subtyping, choice operators and circular proofs [LepRaf2018a].
As part of my current postdoctoral research position at Inria, I am involved in a team effort to transform the Dedukti logical framework into a fullfledged, interactive proof system. This new line of work in Deducteam was envisioned by Frédéric Blanqui, and it is now based on the new implementation of the λΠcalculus that I initiated [Lambdapi]. This new implementation has several major advantages over the previous version of Dedukti. First and foremost, it provides a primitive notion of metavariable which is used for representing proof goals as well as omitted elements (e.g., implicit arguments). Moreover, the implementation relies on the Bindlib library [Bindlib], which allows for highlevel manipulations of structures with bound variables without sacrificing efficiency.
Classical realizability and observational equivalence
To prove the correctness of the PML₂ system (logical consistency and runtime safety), I designed a theoretical framework based on Krivine's classical realisability [Lepigre2016]. This semantical model accounts for the specificities of the system, and in particular the notion of program equivalence that is used for specifying computational behaviours. I thus defined a relation of observational equivalence over terms, which can be naturally expressed in the classical realizability settings. Indeed, quantifying over all the evaluation contexts simply amounts to quantifying over all the stacks in a Krivine abstract machine. Another specificity of the model lies in its callbyvalue nature, which yields an interpretation with three layers, against two in the usual (callbyname) presentation of Krivine's classical realizability (this was already noticed by Guillaume MunchMaccagnoni). Indeed, a type A is interpreted by a set of (fullyevaluated) values ⟦A⟧, a set of stack (evaluation contexts), and a set of terms ⟦A⟧^{⊥⊥} linked by an orthogonality relation. In some sense, this means that ⟦A⟧^{⊥⊥} is the completion of ⟦A⟧ with terms computing elements of ⟦A⟧. It is essential for these sets to be closed under observational equivalence.
Dependent functions, effects and value restriction
In PML₂, program properties are specified and proved by manipulating terms as the firstorder objects of the type system. In particular, this gives a way of expressing properties that should hold for all terms. For example, we can write ∀n, ∀m, n+m ≡ m+n to express the commutativity of an addition function. However, the firstorder quantification that is used here ranges over every possible values, without any type consideration. Whereas functions like addition are usually not defined on all values, but on a restricted domain like the natural numbers, and may crash when fed with something else. Hence, we often need to rely on a stronger, typed form of quantification, with which we can write ∀n∈ℕ, ∀m∈ℕ, n+m ≡ m+n. Such types correspond to a form of dependent function. For instance, the previous example is inhabited by functions taking two number x and y, and returning a proof of x+y ≡ y+x. In PML₂, working with such dependent function types is delicate because of the presence of effects. Indeed, as for polymorphism in ML, dependent functions require some restriction to preserve soundness. The usual value restriction used in ML also applies here, but it is not satisfactory. Indeed, it restricts the application of dependent function to values, which breaks the compositionality of the system.
To solve this issue, I proposed to relax value restriction using the idea that a term that is (observationally) equivalent to a value can be considered to be a value [Lepigre2016]. Although this socalled semantical value restriction is simple, it is extremely hard to justify in the model. Indeed, it requires an essential property relating the different levels of interpretation of types in a novel way. As mentioned previously, a type A is interpreted both as a set of values ⟦A⟧ and as a set of terms ⟦A⟧^{⊥⊥} defined as a completion of ⟦A⟧, which implies ⟦A⟧ ⊆ ⟦A⟧^{⊥⊥}. The property that is required for justifying the semantical value restriction is the following: every value of ⟦A⟧^{⊥⊥} should already be in ⟦A⟧. In other words, the completion operation on sets of values should be closed for values. To obtain this property, I extended the programming language with a new instruction, which provides new tests for observational equivalence (see [Lepigre2016] and [Lepigre2017PhD]).
Typechecking and subtyping in Currystyle languages
Type checking (verifying that a given term inhabits a given type) and type inference (finding a type that is inhabited by a given term) tend to be undecidable in Currystyle languages like System F or PML₂. As a consequence, these system are sometimes considered impractical, although practicality and decidability are two different problems. The main issue with Currystyle languages is that their type systems are generally not syntaxdirected, meaning that they cannot be easily implemented. In particular, there is no canonical way of deciding what typing rule should be applied first when attempting to prove a typing judgment. To solve this problem, we designed (with Christophe Raffalli) a framework based on subtyping [LepRaf2018a]. The main, innovating idea is to use a ternary relation t ∈ A ⊆ B instead of the usual binary relation A ⊆ B. We interpret the former as the implication “if the term t has type A, then it also has type B”, while the latter is interpreted as the inclusion “every element of type A is an element of type B”. In the obtained system, only one typing rule applies for every term constructor, and only one subtyping rule applies for every pair of types (up to commutation). In particular, the connectives that do not have algorithmic contents (those that are not reflected in the syntax of the terms) are handled using subtyping exclusively. Such connectives include the quantifiers, but also the equality types of PML₂ and the least and greatest fixpoint constructors used by inductive and coinductive types.
Choice operators for a closed semantics
Our work on Currystyle languages [LepRaf2018a] not only involves a new notion of subtyping, but also a new way of dealing with variables based on choice operators, inspired by Hilbert's Epsilon operator. With this new presentation, bound variables are systematically substituted by closed symbols playing the role of witnesses for semantical properties. As a consequence, terms and types remain closed throughout the typing and subtyping rules, and the usual typing contexts are not requires anymore. This presentation has several advantages, the first of which being a simplification of the semantics. Indeed, free variables are usually handled (in realizability models) using socalled valuations, assigning them a semantic value. In our presentation, such maps are not required since all the necessary information is carried by the symbolic witnesses that are substituted to free variables. As an indirect consequence of this technique, structural rules such as weakening become completely transparent, and implementation only requires firstorder unification. Finally, the elimination of contexts facilitates the construction of circular proofs (see below).
Circular proofs and termination checking
As mentioned earlier, the framework based on subtyping developed in [LepRaf2018a] is compatible with inductive and coinductive types. They are added to the syntax of types in the form of least and greatest fixpoint operators, which are annotated by ordinals to form sizedtypes. To handle these constructors in a sound way, we introduce a notion of circular proof with a related wellfoundedness criterion. In particular, the subtyping rules that are given for the fixed points induce a form of infinite unfolding. This is due to the fact that we work with symbolic ordinals that are not given a concrete value, and it is thus impossible to know when the zero ordinal will be reached in a decreasing sequence. However, assuming that the proof is wellfounded, we know that it will indeed be reached after finitely many unfolding steps. To keep the proof representation finite, we introduce circularity in our proofs, and check that they are wellformed using the sizechange principle of Lee, Jones and Ben Amram. The notion of circular proof that we consider is in fact very general, and can also be applied to typing rules in our context. This allows us to type recursive programs in a very simple way, while proving their termination. The normalisation proof is obtained using standard reducibility candidates (or realizability) techniques. Indeed, as the structure of our circular proofs is wellfounded, it is still possible to reason by (wellfounded) induction on the structure of our typing (or subtyping) derivations.
Publications
Abstract. In modern OCaml, singleargument datatype declarations (variants with a single constructor, records with a single field) can sometimes be “unboxed”. This means that their memory representation is the same as their single argument (omitting the variant or record constructor and an indirection), thus achieving better time and memory efficiency. However, in the case of generalized/guarded algebraic datatypes (GADTs), unboxing is not always possible due to a subtle fact about the runtime representation of OCaml values. The current correctness check is incomplete, rejecting many valid definitions, in particular those involving mutuallyrecursive datatype declarations. In this paper, we explain the notion of separability as a semantic for the unboxing criterion, and propose a set of inference rules to check separability. From these inference rules, we derive a new implementation of the unboxing check that properly supports mutuallyrecursive definitions.
@inproceedings{CLS2019,
author = {Simon Colin and Rodolphe Lepigre and Gabriel Scherer},
title = {Unboxing Mutually Recursive Type Definitions in OCaml},
booktitle = {Proceedings of JFLA, Les Rousses, France, 30th January to 2nd February 2019.},
year = {2019}
}
Abstract. We present a new, syntaxdirected framework for Curry style typesystems with subtyping. It supports a rich set of features, and allows for a reasonably simple theory and implementation. The system we consider has sum and product types, universal and existential quantifiers, inductive and coinductive types. The latter two may carry size invariants that can be used to establish the termination of recursive programs. For example, the termination of quicksort can be derived by showing that partitioning a list does not increase its size. The system deals with complex programs involving mixed induction and coinduction, or even mixed polymorphism and (co)induction. One of the key ideas is to separate the notion of size from recursion. We do not check the termination of programs directly, but rather show that their (circular) typing proofs are wellfounded. Termination is then obtained using a standard (semantic) normalisation proof. To demonstrate the practicality of the system, we provide an implementation accepting all the examples discussed in the paper.
@article{LepRaf2018a,
author = {Rodolphe Lepigre and Christophe Raffalli},
title = {Practical Subtyping for CurryStyle Languages},
journal = {{ACM} Trans. Program. Lang. Syst.},
year = {2018}
}
Abstract. We present the PML₂ language, which provides a uniform environment for programming, and for proving properties of programs in an MLlike setting. The language is Currystyle and callbyvalue, it provides a control operator (interpreted in terms of classical logic), it supports general recursion and a very general form of (implicit, noncoercive) subtyping. In the system, equational properties of programs are expressed using two new type formers, and they are proved by constructing terminating programs. Although proofs rely heavily on equational reasoning, equalities are exclusively managed by the typechecker. This means that the user only has to choose which equality to use, and not where to use it, as is usually done in mathematical proofs. In the system, writing proofs mostly amounts to applying lemmas (possibly recursive function calls), and to perform case analyses (pattern matchings).
@inproceedings{Lepigre2018,
author = {Rodolphe Lepigre},
title = {{PML$_2$:} Integrated Program Verification in ML},
booktitle = {Postproceedings of TYPES, Budapest, Hungary, 29th May to 1st
June 2018.},
series = {{LIPIcs}},
year = {2018}
}
Abstract. The Bindlib library for OCaml provides a set of tools for the manipulation of data structures with variable binding. It is very well suited for the representation of abstract syntax trees, and has already been used for the implementation of half a dozen languages and proof assistants (including a new version of the logical framework Dedukti). Bindlib is optimised for fast substitution, and it supports variable renaming. Since the representation of binders is based on higherorder abstract syntax, variable capture cannot arise during substitution. As a consequence, variable names are not updated at substitution time. They can however be explicitly recomputed to avoid “visual capture” (i.e., distinct variables with the same apparent name) when a data structure is displayed.
@inproceedings{LepRaf2018b,
author = {Rodolphe Lepigre and
Christophe Raffalli},
editor = {Fr{\'{e}}d{\'{e}}ric Blanqui and
Giselle Reis},
title = {Abstract Representation of Binders in OCaml using the Bindlib Library},
booktitle = {Proceedings of the 13th International Workshop on Logical Frameworks
and MetaLanguages: Theory and Practice, LFMTP@FSCD 2018, Oxford,
UK, 7th July 2018.},
series = {{EPTCS}},
volume = {274},
pages = {4256},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.274.4},
doi = {10.4204/EPTCS.274.4}
}
Abstract. In recent years, proof assistant have reached an
impressive level of maturity. They have led to the certification of
complex programs such as compilers and operating systems. Yet, using
a proof assistant requires highly specialised skills and it remains
very different from standard programming. To bridge this gap, we aim
at designing an MLstyle programming language with support for
proofs of programs, combining in a single tool the flexibility of ML
and the fine specification features of a proof assistant. In other
words, the system should be suitable both for programming (in the
stronglytyped, functional sense) and for gradually increasing the
level of guarantees met by programs, on a byneed basis.
We thus define and study a callbyvalue language whose type system
extends higherorder logic with an equality type over untyped
programs, a dependent function type, classical logic and subtyping.
The combination of callbyvalue evaluation, dependent functions and
classical logic is known to raise consistency issues. To ensure the
correctness of the system (logical consistency and runtime safety),
we design a theoretical framework based on Krivine's classical
realizability. The construction of the model relies on an essential
property linking the different levels of interpretation of types in
a novel way.
We finally demonstrate the expressive power of our system using our
prototype implementation, by proving properties of standard programs
like the map function on lists or the insertion sort.
@phdthesis{Lepigre2017PhD,
author = {Rodolphe Lepigre},
title = {Semantics and Implementation of an Extension of {ML} for Proving Programs.
(S{\'{e}}mantique et Implantation d'une Extension de {ML} pour
la Preuve de Programmes)},
school = {Grenoble Alpes University, France},
year = {2017},
url = {https://tel.archivesouvertes.fr/tel01590363}
}
Abstract. We present a new type system with support for proofs of programs in a callbyvalue language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which are used for specifying program properties and for encoding dependent products. The main challenge arises from the lack of expressiveness of dependent products due to the value restriction. To circumvent this limitation we relax the syntactic restriction and only require equivalence to a value. The consistency of the system is obtained semantically by constructing a classical realizability model in three layers (values, stacks and terms).
@inproceedings{Lepigre2016,
author = {Rodolphe Lepigre},
editor = {Peter Thiemann},
title = {A Classical Realizability Model for a Semantical Value Restriction},
booktitle = {Programming Languages and Systems  25th European Symposium on Programming,
{ESOP} 2016, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2016, Eindhoven, The Netherlands,
April 28, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9632},
pages = {476502},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/9783662494981\_19},
doi = {10.1007/9783662494981\_19}
}
Abstract. Le cœur de DeCaP, objet de cet article, est une
bibliothèque de combinateurs d'analyseurs syntaxiques. Ils sont la cible
de la traduction d'une syntaxe EBNF, sans récursion à gauche, que l'on
a ajoutée à OCaml. Les parseurs ainsi définis sont des expressions de
première classe.
Pour plus d'efficacité, nos combinateurs
utilisent des continuations et inspectent l'ensemble des premiers
caractères acceptés par une grammaire afin d'élaguer l'arbre des
possibilités. Les continuations donnent naturellement la sémantique
complète d'EBNF et DeCaP peut donc gérer les grammaires ambigues. De
plus, des combinateurs inspirés de la notion de continuation délimitée
permettent d'optimiser certaines grammaires en restreignant la
sémantique. Notre parseur d’OCaml est en moyenne deux fois plus rapide
que celui de Camlp4 et cinq fois plus lent que l'original.
DeCaP fournit également un système de
quotation et d'antiquotation similaire à celui de Camlp4 et permet
ainsi d'étendre la syntaxe d'OCaml. Notre outil se veut plus simple et
moins contraignant que ce dernier et n'impose, par exemple, aucune
analyse lexicale.
@inproceedings{LepRaf2015,
author = {Rodolphe Lepigre and Christophe Raffalli},
title = {{Mêler combinateurs, continuations et EBNF pour une analyse
syntaxique efficace en OCaml}},
year = {2015},
booktitle = {Journées Francophones dans Langages Applicatifs (short paper only)}
}
Abstract. A notion of test for intuitionistic type theory has
recently been introduced by Peter Dybjer and his collaborators. It is
meant to be the foundation for automatic testing tools that could be
implemented in proof assistants such as Coq or Agda. Such tools would
provide a way to test, at any time during the construction of a proof,
if the current goal can be completed in the context. The failure of such
a test would mean that the goal is impossible to prove, and its success
would corroborate the partial result.
In this report, we investigate the
possibility of extending the testing procedure to classical systems. We
propose an interpretation of the testing procedure in terms of Krivine's
classical realizability. Finally we show that the notion of test is
correct, in the sense that a judgement is valid if and only if it passes
every possible test.
@MastersThesis{Lepigre2013M2,
author = {Rodolphe Lepigre},
title = {A Classical Realizability Interpretation of Judgement Testing},
school = {Grenoble INP and Université Joseph Fourrier, Grenoble, France},
year = {2013}
}
Abstract.We investigate a testing framework for type theory. We first describe the Krivine Abstract Machine (KAM), and the Testing KAM (TKAM) which is a modified version of the KAM that allows the testing of terms of the PCF language. This follows notes by Pierre Clairambault. We use two versions of the TKAM. The first one is restricted to the Finite System T language and the second one has lazy natural numbers. We then use the virtual machines as the central part of a testing procedure for the typing of terms. This work is an implementation of certain aspects of the testing manual for intuitionistic type theory described in Peter Dybjer's paper “Program Testing and Constructive Validity”.
@MastersThesis{Lepigre2012M1,
author = {Rodolphe Lepigre},
title = {Testing judgments of type theory},
school = {Chalmers Tekniska H\"ogskola, G\"oteborg, Sweden},
year = {2012}
}
Software
My work on the design of type systems for programming languages and proof assistants has resulted in a relatively large amount of implementation work. The most important projects are listed in the following section, and include PML₂ (which is described in [Lepigre2018] and [Lepigre2017PhD]), SubML (which is described in [LepRaf2018a]) but also a more recent work on a new implementation and extension of the Dedukti logical framework. The implementation of such systems has also directed me toward the development of specific tools and software libraries providing convenient abstractions. For instance, I take part in the development of the Bindlib library [LepRaf2018b], that was initiated by Christophe Raffalli, and that provides an abstract representation for binders (which are very common in languages and proofs systems). We also developed (with Christophe Raffalli) a system for writing parsers called Earley, that is integrated to OCaml using a BNFlike syntax extension.
The SubML language implements the type system presented in [LepRaf2018a]. Its many features include subtyping, inductive and coinductive types, polymorphism, existential types, sized types and a termination checker. This is joint work with Christophe Raffalli.
The PML₂ language implements the system presented in [Lepigre2017PhD]. It can be seen as an extension of SubML with proof of programs, classical logic and higherorder. Examples of programs and proofs of programs are given in [Lepigre2017PhD] and [Lepigre2018]. I was the only author of PML₂ (up to minor fixes and examples) until the PhD thesis version (see below). Christophe Raffalli contributes to the development of the language since September 2017.
Lambdapi is an implementation of the λΠcalculus modulo rewriting similar to Dedukti (Dowek et al.), but based on the Bindlib library (see below). It is intended to become the new implementation of Dedukti in the near future. The code is shorter by half, well documented, and first experiments indicate a small gain in terms of performances.
Bindlib is an OCaml library providing tools for the manipulation of data structures with bound variables (e.g., λcalculus, quantified formulas). It allows for efficient substitution and supports variable renaming. The project was initiated by Christophe Raffalli. I contributed several simplifications, improvements, new features, and most of the current documentation.
Earley is a parser combinator library for the OCaml language. It relies on Earley's parsing algorithm and it is intended to be used in conjunction with a proprocessor, which provides an OCaml syntax extension for allowing the definition of parsers inside the OCaml source code. This is joint work with Christophe Raffalli, following [LepRaf2015] in which a different parsing technology was used.
The Timed library allows the encapsulation of reference updates in an abstract notion of state. It can be used to emulate a pure interface while working with (imperative) references. This is joint work with Christophe Raffalli.
The Imagelib library implements image formats without relying on any C library, which makes it suitable for compilation using js_of_ocaml
. Supported image formats are PNG (RCF 2083), PPM, PGM, and PBM. The formats JPG, GIF and XCF are only partially supported.
Patoline aims at providing an alternative to TeXbased systems by relying on a highlevel programming language: OCaml. The project was initiated by PierreÉtienne Meunier, Christophe Raffalli and Tom Hirschowitz. I joined the project in 2013 and became one of its main contributors. I notably used Patoline to produce my thesis [Lepigre2017PhD].
Invited talks and seminars
Date and location  Title and kind of talk  Slides 

11/12/2018 Nantes, France 
The PML₂ Language: Integrated Program Verification in ML Gallinette seminar (Inria) 

03/12/2018 Paris, France 
The PML₂ Language: Integrated Program Verification in ML Prosecco seminar (Inria Paris) 

29/11/2018 Saarbrücken, Germany 
The PML₂ Language: Integrated Program Verification in ML Talk at the Max Planck Institute for Software Systems 

27/11/2018 Saclay, Orsay 
An Overview of the PML₂ Language: Realizability, Subtyping and Cyclic Proofs Invited speaker at the journées inaugurales du GT Scalp (LRI) 

01/10/2018 Paris, France 
Abstract Representation of Binders using the Bindlib Library Gallium seminar (Inria Paris) 

20/09/2018 Cachan, France 
Termination checking using wellfounded typing derivations Deducteam seminar (ENS de Cachan) 
UTF8 
07/07/2018 Oxford, UK 
Representation of Binders Using the Bindlib (OCaml) Library Paper presentation at the LFMTP Workshop 

13/06/2018 Marseille, France 
The PML Language: Realizability at the Service of Program Proofs Invited speaker at the Realizability Workshop (CIRM) 

08/03/2018 Paris, France 
The PML₂ Language: Proving Programs in ML Gallium seminar (Inria Paris) 

17/01/2018 Paris, France 
Practical CurryStyle using Choice Operators and Local Subtyping Type theory and realizability seminar (IRIF) 

22/09/2017 Villetaneuse, France 
Circular Proofs for Subtyping and Termination Seminar of the LCR team (LIPN) 

01/06/2017 Budapest, Hungary 
Theory and Demo of PML2: Proving Programs in ML Contributed talk at the TYPES conference 

22/02/2017 Saclay, France 
PML2, Semantical Value Restriction & Pointed Subtyping Visit to the Parsifal Team (Inria Saclay) 

16/02/2017 Marseille, France 
Proofs of programs and subtyping in PML2 Séminaire Logique et Interactions (I2M) 

07/04/2016 Eindhoven, Netherlands 
A Classical Realizability Model for a Semantical Value Restriction Paper presentation at the ESOP conference 

26/02/2016 Cambridge, UK 
A callbyvalue realizability model for PML Logic and Semantics Seminar (Computer Laboratory) 

03/12/2015 Lyon, France 
A callbyvalue realizability model for PML Séminaire CHoCoLa (ENS de Lyon) 

08/01/2015 Val d'Ajol, France 
Mêler combinateurs et BNF pour l'analyse syntaxique en OCaml Short paper presentation at the JFLA workshop 

03/12/2014 Montevideo, Uruguay 
Toward an Adequation Lemma for PML2 Visit to the Equipo de Lógica, Facultad de Ingeniería, Udelar 

13/04/2014 Grenoble, France 
Realizability, Testing and Game Semantics Talk at the GaLoP workshop 