1 citations · 1 across the 3 of their papers we have counts for
4 papers
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…
Parametricity in an Impredicative Sort
Chantal Keller, Marc Lasson
Reynold's abstraction theorem is now a well-established result for a large class of type systems. We propose here a definition of relational parametricity and a proof of the abstra…
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…
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…