The Refined Calculus of Inductive Construction: Parametricity and Abstraction
Chantal Keller (INRIA Saclay - Ile de France, LIX), Marc Lasson (LIP)
TL;DR
This paper introduces a refined version of the Calculus of Inductive Constructions that facilitates defining relational parametricity, enhancing proof automation in theorem provers like Coq.
Contribution
It presents a new refinement enabling easier definition of relational parametricity within the Calculus of Inductive Constructions.
Findings
Enhanced proof automation in Coq
Simplified definition of relational parametricity
Improved expressiveness of the calculus
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Semantic Web and Ontologies · Logic, Reasoning, and Knowledge