Complete Bidirectional Typing for the Calculus of Inductive Constructions - l'unam - université nantes angers le mans Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

Complete Bidirectional Typing for the Calculus of Inductive Constructions

Résumé

This article presents a bidirectional type system for the Calculus of Inductive Constructions (CIC). It introduces a new judgement intermediate between the usual inference and checking, dubbed constrained inference, to handle the presence of computation in types. The key property of the system is its completeness with respect to the usual undirected one, which has been formally proven in Coq as a part of the MetaCoq project. Although it plays an important role in an ongoing completeness proof for a realistic typing algorithm, the interest of bidirectionality is wider, as it gives insights and structure when trying to prove properties on CIC or design variations and extensions. In particular, we put forward constrained inference, an intermediate between the usual inference and checking judgements, to handle the presence of computation in types.
Fichier principal
Vignette du fichier
main.pdf (868.71 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03139924 , version 1 (12-02-2021)
hal-03139924 , version 2 (19-04-2021)

Identifiants

Citer

Meven Lennon-Bertrand. Complete Bidirectional Typing for the Calculus of Inductive Constructions. ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome, Italy. pp.1-19, ⟨10.4230/LIPIcs.ITP.2021.24⟩. ⟨hal-03139924v2⟩
153 Consultations
208 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More