{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:02:05Z","timestamp":1767927725795,"version":"3.49.0"},"reference-count":115,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T00:00:00Z","timestamp":1415577600000},"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":[[2016,1]]},"abstract":"<jats:p>The use of interactive theorem provers to establish the correctness of critical parts of a software development or for formalizing mathematics is becoming more common and feasible in practice. However, most mature theorem provers lack a direct treatment of partial and general recursive functions; overcoming this weakness has been the objective of intensive research during the last decades. In this article, we review several techniques that have been proposed in the literature to simplify the formalization of partial and general recursive functions in interactive theorem provers. Moreover, we classify the techniques according to their theoretical basis and their practical use. This uniform presentation of the different techniques facilitates the comparison and highlights their commonalities and differences, as well as their relative advantages and limitations. We focus on theorem provers based on constructive type theory (in particular, Agda and Coq) and higher-order logic (in particular Isabelle\/HOL). Other systems and logics are covered to a certain extent, but not exhaustively. In addition to the description of the techniques, we also demonstrate tools which facilitate working with the problematic functions in particular theorem provers.<\/jats:p>","DOI":"10.1017\/s0960129514000115","type":"journal-article","created":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T17:59:54Z","timestamp":1415642394000},"page":"38-88","source":"Crossref","is-referenced-by-count":10,"title":["Partiality and recursion in interactive theorem provers \u2013 an overview"],"prefix":"10.1017","volume":"26","author":[{"given":"ANA","family":"BOVE","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ALEXANDER","family":"KRAUSS","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MATTHIEU","family":"SOZEAU","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,11,10]]},"reference":[{"key":"S0960129514000115_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_11"},{"key":"S0960129514000115_ref13","unstructured":"Balaa A. and Bertot Y. (2002) Fonctions r\u00e9cursives g\u00e9n\u00e9rales par it\u00e9ration en th\u00e9orie des types. Journ\u00e9es Francophones des Langages Applicatifs - JFLA02, INRIA."},{"key":"S0960129514000115_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25979-4_2"},{"key":"S0960129514000115_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_9"},{"key":"S0960129514000115_ref41","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"S0960129514000115_ref22","unstructured":"Berghofer S. and Wenzel M. (1999) Inductive datatypes in HOL \u2013 lessons learned in formal-logic engineering. In: Bertot et al. (1999) 19\u201336."},{"key":"S0960129514000115_ref46","unstructured":"development team (2010) Coq 8.3 Reference Manual, INRIA. http:\/\/coq.inria.fr\/refman\/."},{"key":"S0960129514000115_ref97","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-008-9038-0"},{"key":"S0960129514000115_ref89","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0960129514000115_ref75","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9157-2"},{"key":"S0960129514000115_ref45","first-page":"183","volume-title":"Logic in Computer Science (LICS 1987)","author":"Constable","year":"1987"},{"key":"S0960129514000115_ref37","volume-title":"A Computational Logic","author":"Boyer","year":"1979"},{"key":"S0960129514000115_ref79","doi-asserted-by":"publisher","DOI":"10.1137\/0205033"},{"key":"S0960129514000115_ref10","first-page":"319","article-title":"Theorem Proving in Higher Order Logics (TPHOLs 2008)","volume":"5170","author":"Ait Mohamed","year":"2008","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129514000115_ref92","first-page":"215","article-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic","volume":"2283","author":"Nipkow","year":"2002","journal-title":"Springer Verlag Lecture Notes in Computer Science"},{"key":"S0960129514000115_ref78","first-page":"42","volume-title":"Principles of Programming Languages (POPL 2006)","author":"Leroy","year":"2006"},{"key":"S0960129514000115_ref47","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"S0960129514000115_ref6","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"Abramsky","year":"1994"},{"key":"S0960129514000115_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_10"},{"key":"S0960129514000115_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004191"},{"key":"S0960129514000115_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45685-6_7"},{"key":"S0960129514000115_ref52","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569807.012"},{"key":"S0960129514000115_ref87","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292601"},{"key":"S0960129514000115_ref66","unstructured":"Harrison J. (1995) Inductive definitions: Automation and application. In: Schubert et al. (1995) 200\u2013213."},{"key":"S0960129514000115_ref11","first-page":"86","volume-title":"Logic in Computer Science (LICS 1991)","author":"Audebaud","year":"1991"},{"key":"S0960129514000115_ref38","volume-title":"Automated Reasoning and Its Applications: Essays in Honor of Larry Wos","author":"Boyer","year":"1996"},{"key":"S0960129514000115_ref62","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"Gordon","year":"1993"},{"key":"S0960129514000115_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004822"},{"key":"S0960129514000115_ref100","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80002-5"},{"key":"S0960129514000115_ref21","unstructured":"Berghofer S. and Nipkow T. (2000) Executing higher order logic. In: Callaghan et al. (2002) 24\u201340."},{"key":"S0960129514000115_ref105","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90095-B"},{"key":"S0960129514000115_ref102","volume-title":"Haskell 98 Language and Libraries The Revised Report","author":"Peyton Jones","year":"2003"},{"key":"S0960129514000115_ref88","doi-asserted-by":"crossref","unstructured":"Milner R. (1972) Logic for computable functions: Description of a machine implementation, Technical report, Stanford, CA, USA.","DOI":"10.21236\/AD0785072"},{"key":"S0960129514000115_ref81","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0960129514000115_ref77","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_17"},{"key":"S0960129514000115_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.07.084"},{"key":"S0960129514000115_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15975-4_46"},{"key":"S0960129514000115_ref64","doi-asserted-by":"crossref","unstructured":"Greve D. (2009) Assuming termination. ACL2 Workshop Proceedings.","DOI":"10.1145\/1637837.1637856"},{"key":"S0960129514000115_ref72","first-page":"497","article-title":"Interactive Theorem Proving, Proceedings of 1st International Conference, ITP 2010, Edinburgh, UK, 11\u201314 July, 2010","volume":"6172","author":"Kaufmann","year":"2010","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129514000115_ref9","unstructured":"Agda (2008) Agda wiki. Available at http:\/\/wiki.portal.chalmers.se\/agda\/agda.php."},{"key":"S0960129514000115_ref82","doi-asserted-by":"crossref","unstructured":"Matthews J. (1999) Recursive function definition over coinductive types. In: Bertot et al. (1999) 73\u201390.","DOI":"10.1007\/3-540-48256-3_6"},{"key":"S0960129514000115_ref3","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(2:3)2008"},{"key":"S0960129514000115_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44659-1_1"},{"key":"S0960129514000115_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_47"},{"key":"S0960129514000115_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_18"},{"key":"S0960129514000115_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73228-0_7"},{"key":"S0960129514000115_ref74","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_34"},{"key":"S0960129514000115_ref76","doi-asserted-by":"crossref","unstructured":"Krauss A. (2010b) Recursive definitions of monadic functions. In: Bove et al. (2010) 1\u201313.","DOI":"10.4204\/EPTCS.43.1"},{"key":"S0960129514000115_ref70","first-page":"410","volume-title":"Principles of Programming Languages (POPL 1996)","author":"Hughes","year":"1996"},{"key":"S0960129514000115_ref84","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004957"},{"key":"S0960129514000115_ref110","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_16"},{"key":"S0960129514000115_ref36","first-page":"93","article-title":"Workshop on Partiality and Recursion in Interative Theorem Provers (PAR 2010), Satellite Workshop of ITP'10 at FLoC 2010","volume":"43","author":"Bove","year":"2010","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"S0960129514000115_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_5"},{"key":"S0960129514000115_ref90","doi-asserted-by":"publisher","DOI":"10.1017\/S095679689900341X"},{"key":"S0960129514000115_ref53","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"S0960129514000115_ref68","unstructured":"Huffman B. (2008) Reasoning with powerdomains in Isabelle\/HOLCF. In: Ait Mohamed O. , Mu\u00f1oz C. and Tahar S. (eds.) TPHOLs 2008: Emerging Trends Proceedings, Department of Electrical and Computer Engineering, Concordia University 45\u201356."},{"key":"S0960129514000115_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"S0960129514000115_ref98","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116"},{"key":"S0960129514000115_ref33","doi-asserted-by":"crossref","unstructured":"Bove A. and Capretta V. (2008) A type of partial recursive functions. In: Ait Mohamed et al. (2008) 102\u2013117.","DOI":"10.1007\/978-3-540-71067-7_12"},{"key":"S0960129514000115_ref55","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881906"},{"key":"S0960129514000115_ref60","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7_3"},{"key":"S0960129514000115_ref86","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"S0960129514000115_ref73","doi-asserted-by":"crossref","unstructured":"Krauss A. (2006) Partial recursive functions in higher-order logic. In: Furbach and Shankar (2006) 589\u2013603.","DOI":"10.1007\/11814771_48"},{"key":"S0960129514000115_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S0960129514000115_ref108","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0105417"},{"key":"S0960129514000115_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_9"},{"key":"S0960129514000115_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45685-6_4"},{"key":"S0960129514000115_ref67","first-page":"479","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Howard","year":"1980"},{"key":"S0960129514000115_ref25","first-page":"358","volume":"1690","author":"Bertot","year":"1999","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129514000115_ref58","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005797629953"},{"key":"S0960129514000115_ref59","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006408829523"},{"key":"S0960129514000115_ref34","doi-asserted-by":"crossref","unstructured":"Bove A. , Dybjer P. and Sicard-Ram\u00edrez A. (2009) Embedding a logical theory of constructions in Agda, Programming Languages meets Program Verification (PLPV) 2009, ACM Digital Library.","DOI":"10.1145\/1481848.1481857"},{"key":"S0960129514000115_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03153-3_3"},{"key":"S0960129514000115_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15648-8_5"},{"key":"S0960129514000115_ref69","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_19"},{"key":"S0960129514000115_ref43","first-page":"51","volume-title":"3rd Refinement Workshop","author":"Cheng","year":"1991"},{"key":"S0960129514000115_ref2","unstructured":"Abel A. (2006) A Polymorphic Lambda-Calculus with Sized Higher-Order Types, Ph.D. thesis, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen."},{"key":"S0960129514000115_ref42","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud A. (2010) The optimal fixed point combinator. In: Kaufmann and Paulson (2010) 195\u2013210.","DOI":"10.1007\/978-3-642-14052-5_15"},{"key":"S0960129514000115_ref101","doi-asserted-by":"publisher","DOI":"10.1007\/BF00248324"},{"key":"S0960129514000115_ref96","unstructured":"OCaml (1996) Ocaml web page. Available at http:\/\/caml.inria.fr\/ocaml\/."},{"key":"S0960129514000115_ref54","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(93)90144-3"},{"key":"S0960129514000115_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28729-9_7"},{"key":"S0960129514000115_ref57","first-page":"680","volume":"4130","author":"Furbach","year":"2006","journal-title":"Springer Verlag Lecture Notes in Artificial Intelligence"},{"key":"S0960129514000115_ref80","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000009505.07087.34"},{"key":"S0960129514000115_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"S0960129514000115_ref8","first-page":"1","volume-title":"Proceedings of the Symposium on Mathematical Logic (Oulu, 1974)","author":"Aczel","year":"1977"},{"key":"S0960129514000115_ref26","first-page":"89","volume-title":"Principles and Practice of Declarative Programming (PPDP '08)","author":"Bertot","year":"2008"},{"key":"S0960129514000115_ref85","doi-asserted-by":"publisher","DOI":"10.1007\/11546382_3"},{"key":"S0960129514000115_ref109","unstructured":"Slind K. (1999) Reasoning About Terminating Functional Programs, Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen."},{"key":"S0960129514000115_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_35"},{"key":"S0960129514000115_ref107","doi-asserted-by":"crossref","unstructured":"Setzer A. (2007) A data type of partial recursive functions in Martin-L\u00f6f type theory. 35 pp, submitted.","DOI":"10.1007\/11780342_51"},{"key":"S0960129514000115_ref1","unstructured":"Abel A. (1998) Foetus \u2013 termination checker for simple functional programs. Programming Lab Report. Available at http:\/\/www.tcs.informatik.uni-muenchen.de\/abel\/foetus\/."},{"key":"S0960129514000115_ref63","first-page":"162","article-title":"Edinburgh LCF: A Mechanised Logic of Computation","volume":"78","author":"Gordon","year":"1979","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129514000115_ref65","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"S0960129514000115_ref83","doi-asserted-by":"crossref","unstructured":"McBride C. (2002) Elimination with a motive. In: Callaghan et al. (2002) 197\u2013216.","DOI":"10.1007\/3-540-45842-5_13"},{"key":"S0960129514000115_ref114","doi-asserted-by":"crossref","unstructured":"Wenzel M. , Paulson L. C. and Nipkow T. (2008) The Isabelle framework. In: Ait Mohamed et al. (2008) 33\u201338.","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"S0960129514000115_ref113","unstructured":"Wahlstedt D. (2007) Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion, Ph.D. thesis, Chalmers University of Technology."},{"key":"S0960129514000115_ref106","doi-asserted-by":"publisher","DOI":"10.1007\/11780342_51"},{"key":"S0960129514000115_ref112","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9143-8"},{"key":"S0960129514000115_ref111","doi-asserted-by":"crossref","unstructured":"Sozeau M. (2010) Equations: A dependent pattern matching compiler. In: Kaufmann and Paulson (2010) 419\u2013434.","DOI":"10.1007\/978-3-642-14052-5_29"},{"key":"S0960129514000115_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264250"},{"key":"S0960129514000115_ref115","first-page":"231","volume-title":"Logic in Computer Science (LICS 2001)","author":"Xi","year":"2001"},{"key":"S0960129514000115_ref95","unstructured":"Norell U. (2007) Towards a Practical Programming Language Based on Dependent Type Theory, Ph.D. thesis, Chalmers University of Technology."},{"key":"S0960129514000115_ref56","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005702928286"},{"key":"S0960129514000115_ref103","unstructured":"Regensburger F. (1995) HOLCF: Higher order logic of computable functions. In: Schubert et al. (1995) 293\u2013307."},{"key":"S0960129514000115_ref99","volume-title":"From Semantics and Computer Science: Essays in Honor of Gilles Kahn","author":"Paulin-Mohring","year":"2009"},{"key":"S0960129514000115_ref104","first-page":"400","article-title":"Higher Order Logic Theorem Proving and its Applications, Proceedings of 8th International Workshop, Aspen Grove, UT, USA, 11\u201314 September, 1995","volume":"971","author":"Schubert","year":"1995","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129514000115_ref71","volume-title":"Systematic Software Development using VDM","author":"Jones","year":"1990"},{"key":"S0960129514000115_ref50","unstructured":"Dubois C. and Donzeau-Gouge V. V. (1998) A step towards the mechanization of partial functions: domains as inductive predicates. CADE-15 Workshop on Mechanization of Partial Functions."},{"key":"S0960129514000115_ref93","doi-asserted-by":"publisher","DOI":"10.1007\/BF01941137"},{"key":"S0960129514000115_ref61","doi-asserted-by":"publisher","DOI":"10.1007\/11780274_27"},{"key":"S0960129514000115_ref91","unstructured":"Nipkow T. , Bauer G. and Schultz P. (2006) Flyspeck I: Tame graphs. In: Furbach and Shankar (2006) 21\u201335."},{"key":"S0960129514000115_ref40","first-page":"245","volume":"2277","author":"Callaghan","year":"2002","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129514000115_ref94","volume-title":"Programming in Martin-L\u00f6f's Type Theory. An Introduction","author":"Nordstr\u00f6m","year":"1990"},{"key":"S0960129514000115_ref4","unstructured":"Abel A. (2010) MiniAgda: Integrating sized and dependent types. In: Bove et al. (2010) 14\u201328."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000115","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T05:46:13Z","timestamp":1566020773000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000115\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,10]]},"references-count":115,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,1]]}},"alternative-id":["S0960129514000115"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000115","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,10]]}}}