A Formal System for the Universal Quantification of Schematic Variables

Abstract

We advocate the use of de Bruijn's universal abstraction $λ^\infty$ for the quantification of schematic variables in the predicative setting and we present a typed $λ$-calculus featuring the quantifier $λ^\infty$ accompanied by other practically useful constructions like explicit substitutions and expected type annotations. The calculus stands just on two notions, i.e., bound rt-reduction and parametric validity, and has the expressive power of $λ\rightarrow$. Thus, while not aiming at being a logical framework by itself, it does enjoy many desired invariants of logical frameworks including confluence of reduction, strong normalization, preservation of type by reduction, decidability, correctness of types and uniqueness of types up to conversion. This calculus belongs to the $λδ$ family of formal systems, which borrow some features from the pure type systems and some from the languages of the Automath tradition, but stand outside both families. In particular, the calculus includes and evolves two earlier systems of this family. Moreover, a machine-checked specification of its theory is available.