Sciweavers

Share
CORR
2012
Springer

A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions

7 years 5 months ago
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
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, procee...
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdot
Added 20 Apr 2012
Updated 20 Apr 2012
Type Journal
Year 2012
Where CORR
Authors Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
Comments (0)
books