The Refined Calculus of Inductive Construction: Parametricity and Abstraction
Logic in Computer Science
2012-11-28 v1
Abstract
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 an interactive theorem prover like Coq.
Cite
@article{arxiv.1211.6341,
title = {The Refined Calculus of Inductive Construction: Parametricity and Abstraction},
author = {Chantal Keller and Marc Lasson},
journal= {arXiv preprint arXiv:1211.6341},
year = {2012}
}