1 citations · 1 across the 3 of their papers we have counts for
3 papers
cs.LO2012
The Refined Calculus of Inductive Construction: Parametricity and Abstraction
Chantal Keller, Marc Lasson
We present a refinement of the Calculus of Inductive Constructions in which one can easily define a notion of relational parametricity. It provides a new way to automate proofs in…
cs.LO2010★ 1 cited
Controlling program extraction in Elementary Linear Logic
Marc Lasson
We present an adaptation, based on program extraction in elementary linear logic, of Krivine & Leivant's system FA_2. This system allows to write higher-order equations in order to…
cs.LO2010
Internalized realizability in pure type systems
Marc Lasson
Let P be any pure type system, we are going to show how we can extend P into a PTS P' which will be used as a proof system whose formulas express properties about sets of terms of…