Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Implementing Type Theory in Higher Order Constraint Logic Programming

Abstract : 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 terms with holes or, equivalently, partial proof terms. In the first part of the paper we confirm that λProlog, the language developed by Miller and Nadathur since the 80s, is extremely suitable for implementing the kernel, even when efficient techniques like reduction machines are employed. In the second part of the paper we turn our attention to the elaborator and we observe that the eager generative semantics inherited by Prolog makes it impossible to reason by induction over terms containing metavariables. We also conclude that the minimal extension to λProlog that allows to do so is the possibility to delay inductive predicates over flexible terms, turning them into (set of) constraints to be propagated according to user provided constraint propagation rules. Therefore we propose extensions to λProlog to declare and manipulate higher order constraints, and we implement the proposed extensions in the ELPI system. Our test case is the implementation of an elaborator for a type theory as a CLP extension to a kernel written in plain λProlog.
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download
Contributor : Enrico Tassi Connect in order to contact the contributor
Submitted on : Friday, November 17, 2017 - 11:31:06 AM
Last modification on : Thursday, January 7, 2021 - 3:40:10 PM
Long-term archiving on: : Sunday, February 18, 2018 - 2:00:23 PM


Files produced by the author(s)


  • HAL Id : hal-01410567, version 2



Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi. Implementing Type Theory in Higher Order Constraint Logic Programming. 2017. ⟨hal-01410567v2⟩



Les métriques sont temporairement indisponibles