2021/02/12 by Meven Lennon-Bertrand, Lennon-Bertrand, Meven
Computer Science · #F.3 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Numerical Methods and Algorithms #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2102.06513
openalex publication_date 2021/02/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.