Complete Bidirectional Typing for the Calculus of Inductive Constructions - Ecole Centrale de Nantes Accéder directement au contenu
Pré-Publication, Document De Travail 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 novel judgement intermediate between the usual inference and checking, dubbed constrained inference, to handle the presence of computation in types. The key property is the completeness of the system with respect to the usual undirected one, which has been formally proven in Coq as a part of the MetaCoq project. Although it plays a central role in an ongoing completeness proof for a realistic typing algorithm, the interest of bidirectionality is much wider, as it clarifies previous works in the area and gives strong insights and structure when trying to prove properties on CIC or design variations and extensions.
Fichier principal
Vignette du fichier
main.pdf (871.13 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

  • HAL Id : hal-03139924 , version 1

Citer

Meven Lennon-Bertrand. Complete Bidirectional Typing for the Calculus of Inductive Constructions. 2021. ⟨hal-03139924v1⟩
153 Consultations
211 Téléchargements

Partager

Gmail Facebook X LinkedIn More