The Refined Calculus of Inductive Construction: Parametricity and Abstraction - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

The Refined Calculus of Inductive Construction: Parametricity and Abstraction

Résumé

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.

Domaines

Logique en informatique [cs.LO]
Fichier principal
Vignette du fichier
paramath.pdf (75.61 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Chantal Keller  : Connectez-vous pour contacter le contributeur

https://inria.hal.science/hal-00757620

Soumis le : mardi 27 novembre 2012-14:52:31

Dernière modification le : jeudi 11 mai 2023-11:56:10

Archivage à long terme le : jeudi 28 février 2013-03:43:39

Télécharger pour visualiser

Dates et versions

hal-00757620 , version 1 (27-11-2012)

Identifiants

Citer

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⟩

Exporter

BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

ENS-LYON X CNRS INRIA UNIV-LYON1 LIX LIP X-LIX X-DEP-INFO LIP_PLUME INRIA2 UDL
424 Consultations
161 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More