Skip to Main content Skip to Navigation
Conference papers

The Refined Calculus of Inductive Construction: Parametricity and Abstraction

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [7 references]  Display  Hide  Download

https://hal.inria.fr/hal-00757620
Contributor : Chantal Keller <>
Submitted on : Tuesday, November 27, 2012 - 2:52:31 PM
Last modification on : Friday, June 25, 2021 - 3:40:04 PM
Long-term archiving on: : Thursday, February 28, 2013 - 3:43:39 AM

Files

paramath.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00757620, version 1
  • ARXIV : 1211.6341

Collections

Citation

Chantal Keller, Marc Lasson. The Refined Calculus of Inductive Construction: Parametricity and Abstraction. LICS - 27th Annual IEEE Symposium on Logic in Computer Science - 2012, Jun 2012, Dubrovnik, Croatia. ⟨hal-00757620⟩

Share

Metrics

Record views

669

Files downloads

279