License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.24
URN: urn:nbn:de:0030-drops-139194
URL: https://drops.dagstuhl.de/opus/volltexte/2021/13919/
Go to the corresponding LIPIcs Volume Portal


Lennon-Bertrand, Meven

Complete Bidirectional Typing for the Calculus of Inductive Constructions

pdf-format:
LIPIcs-ITP-2021-24.pdf (0.8 MB)


Abstract

This article presents a bidirectional type system for the Calculus of Inductive Constructions (CIC). 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.

BibTeX - Entry

@InProceedings{lennonbertrand:LIPIcs.ITP.2021.24,
  author =	{Lennon-Bertrand, Meven},
  title =	{{Complete Bidirectional Typing for the Calculus of Inductive Constructions}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13919},
  URN =		{urn:nbn:de:0030-drops-139194},
  doi =		{10.4230/LIPIcs.ITP.2021.24},
  annote =	{Keywords: Bidirectional Typing, Calculus of Inductive Constructions, Coq, Proof Assistants}
}

Keywords: Bidirectional Typing, Calculus of Inductive Constructions, Coq, Proof Assistants
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: Software (Formalization): https://github.com/MevenBertrand/metacoq/tree/itp-artefact archived at: https://archive.softwareheritage.org/swh:1:dir:d5e5b711b7c45fdfb18f02bf91684f771e0c8b65


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI