The Refined Calculus of Inductive Construction: Parametricity and Abstraction

Chantal Keller 1, 2 Marc Lasson 3
1 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
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.
Type de document :
Communication dans un congrès
LICS - 27th Annual IEEE Symposium on Logic in Computer Science - 2012, Jun 2012, Dubrovnik, Croatia. 2012
Liste complète des métadonnées

Littérature citée [7 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00757620
Contributeur : Chantal Keller <>
Soumis le : mardi 27 novembre 2012 - 14:52:31
Dernière modification le : jeudi 10 mai 2018 - 02:06:56
Document(s) archivé(s) le : jeudi 28 février 2013 - 03:43:39

Fichiers

paramath.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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

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. 2012. 〈hal-00757620〉

Partager

Métriques

Consultations de la notice

401

Téléchargements de fichiers

183