A bi-directional refinement algorithm for the calculus of (co)inductive constructions

DOI10.2168/LMCS-8(1:18)2012MaRDI QIDQ2881085zbMATH OpenFDO

Authors Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi

Publication date 3 April 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1202.4905

zbMATH Keywords

type inferencecalculus of inductive constructionsinteractive theorem prover\texttt{Matita}refiner

Mathematics Subject Classification ID

Abstract: The paper describes the refinement algorithm for the Calculus of (Co)Inductive Constructions (CIC) implemented in the interactive theorem prover Matita. The refinement algorithm is in charge of giving a meaning to the terms, types and proof terms directly written by the user or generated by using tactics, decision procedures or general automation. The terms are written in an "external syntax" meant to be user friendly that allows omission of information, untyped binders and a certain liberal use of user defined sub-typing. The refiner modifies the terms to obtain related well typed terms in the internal syntax understood by the kernel of the ITP. In particular, it acts as a type inference algorithm when all the binders are untyped. The proposed algorithm is bi-directional: given a term in external syntax and a type expected for the term, it propagates as much typing information as possible towards the leaves of the term. Traditional mono-directional algorithms, instead, proceed in a bottom-up way by inferring the type of a sub-term and comparing (unifying) it with the type expected by its context only at the end. We propose some novel bi-directional rules for CIC that are particularly effective. Among the benefits of bi-directionality we have better error message reporting and better inference of dependent types. Moreover, thanks to bi-directionality, the coercion system for sub-typing is more effective and type inference generates simpler unification problems that are more likely to be solved by the inherently incomplete higher order unification algorithms implemented. Finally we introduce in the external syntax the notion of vector of placeholders that enables to omit at once an arbitrary number of arguments. Vectors of placeholders allow a trivial implementation of implicit arguments and greatly simplify the implementation of primitive and simple tactics.

Recommendations

• scientific article; zbMATH DE number 7699441
• scientific article; zbMATH DE number 2185723
• A compact kernel for the calculus of inductive constructions
• Reduction and conversion strategies for the calculus of (co)inductive constructions. I
• A refinement-based approach to computational algebra in Coq
• scientific article; zbMATH DE number 2061701
• scientific article; zbMATH DE number 2182487
• Inductive consequences in the calculus of constructions
• A calculus of refinements for program derivations

Cited in

(6)

• scientific article; zbMATH DE number 7561342 (Why is no real title available?)
• Reduction and conversion strategies for the calculus of (co)inductive constructions. I
• I got plenty o' nuttin'
• A formalization of multi-tape Turing machines
• A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
• Implementing type theory in higher order constraint logic programming

Describes a project that uses

Uses Software

• Agda
• Automath
• Matita
• Coq

This page was built for publication: A bi-directional refinement algorithm for the calculus of (co)inductive constructions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2881085)