14 citations · 27 across the 4 of their papers we have counts for
Showing 2016Show all
2 papers · 1 filter
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…