14 citations · 27 across the 4 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2019★ 7 cited
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…
cs.LO2016★ 14 cited
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…
cs.LO2016
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…