
VOLUME 8, ISSUE 1, PAPER 18
A BiDirectional Refinement Algorithm for the Calculus of (Co)Inductive Constructions

©Andrea Asperti, University of Bologna ©Wilmer Ricciotti, University of Bologna ©Claudio Sacerdoti Coen, University of Bologna ©Enrico Tassi, INRIA  Microsoft Research 
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
subtyping. 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 bidirectional: 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 monodirectional
algorithms, instead, proceed in a bottomup way by inferring the type of a
subterm and comparing (unifying) it with the type expected by its context only
at the end. We propose some novel bidirectional rules for CIC that are
particularly effective. Among the benefits of bidirectionality we have better
error message reporting and better inference of dependent types. Moreover,
thanks to bidirectionality, the coercion system for subtyping 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.

Publication date: March 2, 2012
Full Text: PDF  PostScript DOI: 10.2168/LMCS8(1:18)2012
Hit Counts: 4792 
Creative Commons  