We advocate the use of de Bruijn’s universal abstraction \lambda {\mathord \infty }{}{}{} for the quantification of schematic variables in the predicative setting, and we present a typed \lambda {}{}{}{} -calculus featuring the quantifier \lambda {\mathord \infty }{}{}{} accompanied by other practically useful constructions like explicit substitutions and expected type annotations. Our calculus stands just on two notions, i.e., bound rt-reduction and parametric validity, and has the expressive power of \lambda \mathord \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 \lambda \delta 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, our calculus includes and evolves two earlier systems of this family. Moreover, a machine-checked specification of its theory is available.

In this paper, we are interested in high-level programming languages to implement the core components of an interactive theorem prover for a dependently typed language: the kernel – responsible for type-checking closed terms – and the elaborator – that manipulates open terms, that is terms containing unresolved unification variables. In this paper, we confirm that λProlog, the language developed by Miller and Nadathur since the 80s, is extremely suitable for implementing the kernel. Indeed, we easily obtain a type checker for the Calculus of Inductive Constructions (CIC). Even more, we do so in an incremental way by escalating a checker for a pure type system to the full CIC. We then turn our attention to the elaborator with the objective to obtain a simple implementation thanks to the features of the programming language. In particular, we want to use λProlog’s unification variables to model the object language ones. In this way, scope checking, carrying of assignments and occur checking are handled by the programming language. We observe that the eager generative semantics inherited from Prolog clashes with this plan. We propose an extension to λProlog that allows to control the generative semantics, suspend goals over flexible terms turning them into constraints, and finally manipulate these constraints at the meta-meta level via constraint handling rules. We implement the proposed language extension in the Embedded Lambda Prolog Interpreter system and we discuss how it can be used to extend the kernel into an elaborator for CIC.

The formal system λδ is a typed λ-calculus that pursues the unification of terms, types, environments, and contexts as the main goal. λδ takes some features from the Automath-related λ-calculi and some from the pure type systems, but differs from both in that it does not include the Π construction while it provides for an abbreviation mechanism at the level of terms. λδ enjoys some important desirable properties such as the confluence of reduction, the correctness of types, the uniqueness of types up to conversion, the subject reduction of the type assignment, the strong normalization of the typed terms, and, as a corollary, the decidability of type inference problem.