14 citations · 27 across the 4 of their papers we have counts for
5 papers
PML 2 : Integrated Program Verification in ML
Rodolphe Lepigre
We present the PML 2 language, which provides a uniform environment for programming, and for proving properties of programs in an ML-like setting. The language is Curry-style and c…
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…
Abstract Representation of Binders in OCaml using the Bindlib Library
Rodolphe Lepigre, Christophe Raffalli
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 synta…
A Classical Realizability Model for a Semantical Value Restriction
Rodolphe Lepigre
We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (unt…
Practical Subtyping for System F with Sized (Co-)Induction
Rodolphe Lepigre, Christophe Raffalli
We present a rich type system with subtyping for an extension of System F. Our type constructors include sum and product types, universal and existential quantifiers, inductive and…