{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T20:33:26Z","timestamp":1768163606499,"version":"3.49.0"},"reference-count":43,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2019,3,1]],"date-time":"2019-03-01T00:00:00Z","timestamp":1551398400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2019,9]]},"abstract":"<jats:p>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 \u2013 responsible for type-checking closed terms \u2013 and the elaborator \u2013 that manipulates open terms, that is terms containing unresolved unification variables.<\/jats:p><jats:p>In this paper, we confirm that \u03bbProlog, 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.<\/jats:p><jats:p>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 \u03bbProlog\u2019s 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.<\/jats:p><jats:p>We observe that the eager generative semantics inherited from Prolog clashes with this plan. We propose an extension to \u03bbProlog 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.<\/jats:p><jats:p>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.<\/jats:p>","DOI":"10.1017\/s0960129518000427","type":"journal-article","created":{"date-parts":[[2019,3,1]],"date-time":"2019-03-01T05:28:21Z","timestamp":1551418101000},"page":"1125-1150","source":"Crossref","is-referenced-by-count":5,"title":["Implementing type theory in higher order constraint logic programming"],"prefix":"10.1017","volume":"29","author":[{"given":"FERRUCCIO","family":"GUIDI","sequence":"first","affiliation":[]},{"given":"CLAUDIO","family":"SACERDOTI COEN","sequence":"additional","affiliation":[]},{"given":"ENRICO","family":"TASSI","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2019,3,1]]},"reference":[{"key":"S0960129518000427_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"S0960129518000427_ref10","unstructured":"Boespflug M. , Carbonneaux Q. and Hermant O. (2012). The lambda-pi-calculus modulo as a universal proof language. In: Proceedings of the 2nd International Workshop on Proof Exchange for Theorem Proving, CEUR Workshop Proceedings, vol. 878, 28\u201343."},{"key":"S0960129518000427_ref15","unstructured":"Dunchev C. , Guidi F. , Sacerdoti Coen C. and Tassi E. (2015). ELPI: Fast, embeddable, \u03bbProlog interpreter. In: Proceedings of Logic for Programming, Artificial Intelligence and Reasoning."},{"key":"S0960129518000427_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_8"},{"key":"S0960129518000427_ref25","unstructured":"Luo Z. (1996). Coercive subtyping in type theory. In: Proceedings of the 10th International Workshop on Computer Science Logic, Annual Conference of the European Association for Computer Science Logic, Utrecht, the Netherlands, September 21\u201327, Selected Papers, 276\u2013296."},{"key":"S0960129518000427_ref11","unstructured":"Coq development team. (2017). The Coq Proof Assistant Reference Manual, Inria."},{"key":"S0960129518000427_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.09.026"},{"key":"S0960129518000427_ref24","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39193"},{"key":"S0960129518000427_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_11"},{"key":"S0960129518000427_ref28","unstructured":"Mazzoli F. and Abel A. (2016). Type checking through unification. CoRR, abs\/1609.09709."},{"key":"S0960129518000427_ref1","unstructured":"Andersson J. , Andersson S. , Boortz K. , Carlsson M. , Nilsson H. , Sj\u00f6land T. and Widen J. (1993). SICStus Prolog User's Manual. Technical report."},{"key":"S0960129518000427_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.10.020"},{"key":"S0960129518000427_ref42","unstructured":"Werner B. (1994). Une Th\u00e9orie des Constructions Inductives. PhD thesis, Universit\u00e9 Paris VII."},{"key":"S0960129518000427_ref5","first-page":"91","article-title":"Matita tutorial","volume":"7","author":"Asperti","year":"2014","journal-title":"Journal of Formalized Reasoning"},{"key":"S0960129518000427_ref6","first-page":"1","article-title":"Abella: A system for reasoning about relational specifications","volume":"7","author":"Baelde","year":"2014","journal-title":"Journal of Formalized Reasoning"},{"key":"S0960129518000427_ref7","first-page":"7","volume-title":"Auto-Validation d'un syst\u00e8me de preuves avec familles inductives","author":"Barras","year":"1999"},{"key":"S0960129518000427_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10038-9"},{"key":"S0960129518000427_ref12","unstructured":"de Moura L. , Avigad J. , Kong S. and Roux C. (2015a). Elaboration in dependent type theory. CoRR, abs\/1505.04324."},{"key":"S0960129518000427_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27775-0_7"},{"key":"S0960129518000427_ref16","unstructured":"Dunchev C. , Sacerdoti Coen C. and Tassi E. (2016). Implementing HOL in an higher order logic programming language. In: Proceedings of the 11th Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, ACM, 4:1\u20134:10. ISBN 978-1-4503-4777-8."},{"key":"S0960129518000427_ref17","unstructured":"Ebner G. , Ullrich S. , Roesch J. , Avigad J. and de Moura L. (Aug. 2017). A metaprogramming framework for formal verification. In: Proceedings of the ACM Programming Languages, vol. 1, 34:1\u201334:29. ISSN 2475-1421."},{"key":"S0960129518000427_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012823"},{"key":"S0960129518000427_ref19","doi-asserted-by":"crossref","unstructured":"Felty A.P. and Miller D. (1990). Encoding a dependent-type lambda-calculus in a logic programming language. In: Proceedings of the 10th International Conference on Automated Deduction, London, UK: Springer-Verlag, 221\u2013235. ISBN 3-540-52885-7.","DOI":"10.1007\/3-540-52885-7_90"},{"key":"S0960129518000427_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"S0960129518000427_ref22","unstructured":"Herbelin H. (2005). Type inference with algebraic universes in the calculus of inductive constructions. Unpublished. Available at: pauillac.inria.fr\/~herbelin\/publis\/univalgcci.pdf"},{"key":"S0960129518000427_ref23","unstructured":"Libal T. and Miller D. (2016). Functions-as-constructors higher-order unification. In: Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, Porto, Portugal, Delia Kesner and Brigitte Pientka, 1\u201317."},{"key":"S0960129518000427_ref27","unstructured":"Mahboubi A. and Tassi E. (July 2013). Canonical structures for the working Coq user. In: Blazy S. , Paulin C. and Pichardie D. (eds.) 4th Conference on Interactive Theorem Proving, Lecture Notes in Computer Science, vol. 7998, Rennes, France: Springer, 19\u201334."},{"key":"S0960129518000427_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90068-W"},{"key":"S0960129518000427_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"S0960129518000427_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16492-8_94"},{"key":"S0960129518000427_ref31","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326"},{"key":"S0960129518000427_ref34","volume-title":"D\u00e9finitions Inductives en Th\u00e9orie des Types d'Ordre Sup\u00e9rieur","author":"Paulin-Mohring","year":"1996"},{"key":"S0960129518000427_ref4","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:18)2012"},{"key":"S0960129518000427_ref35","unstructured":"Qi X. , Gacek A. , Holte S. , Nadathur G. and Snow Z. (2015). The Teyjus System \u2013 Version 2. Available at: http:\/\/teyjus.cs.umn.edu\/"},{"key":"S0960129518000427_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39320-4_25"},{"key":"S0960129518000427_ref37","unstructured":"Roberto Blanco D.M. and Chihani Z. (2017). Translating between implicit and explicit versions of proof. In: Conference on Automated Deduction 26."},{"key":"S0960129518000427_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68103-8_11"},{"key":"S0960129518000427_ref39","unstructured":"Sacerdoti Coen C. and Tassi E. (2009). Nonuniform coercions via unification hints. In: Proceedings TYPES, 16\u201329."},{"key":"S0960129518000427_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/1836089.1836113"},{"key":"S0960129518000427_ref43","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000494"},{"key":"S0960129518000427_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45793-3_36"},{"key":"S0960129518000427_ref3","first-page":"64","volume-title":"The Matita Interactive Theorem Prover","author":"Asperti","year":"2011"},{"key":"S0960129518000427_ref13","first-page":"378","volume-title":"The Lean Theorem Prover (System Description)","author":"de Moura","year":"2015"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129518000427","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,15]],"date-time":"2024-07-15T08:06:06Z","timestamp":1721030766000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129518000427\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,3,1]]},"references-count":43,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["S0960129518000427"],"URL":"https:\/\/doi.org\/10.1017\/s0960129518000427","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,3,1]]}}}