7 citations · 14 across the 6 of their papers we have counts for
Showing 2012Show all
2 papers · 1 filter
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.LO2012
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…