Implementing type theory in higher order constraint logic programming

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 lambda 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 lambda 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 lambda 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.