{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:24:52Z","timestamp":1761596692107,"version":"3.44.0"},"reference-count":20,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[2002,4,1]],"date-time":"2002-04-01T00:00:00Z","timestamp":1017619200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,4,1]],"date-time":"2002-04-01T00:00:00Z","timestamp":1017619200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4125,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-0105651","DMS-9870320"],"award-info":[{"award-number":["CCR-0105651","DMS-9870320"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[2002,4]]},"DOI":"10.1016\/s0168-0072(01)00078-1","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T10:20:24Z","timestamp":1027592424000},"page":"117-153","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":20,"title":["Intrinsic reasoning about functional programs I: first order theories"],"prefix":"10.1016","volume":"114","author":[{"given":"Daniel","family":"Leivant","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0168-0072(01)00078-1_BIB1","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1017\/S0305004100013463","article-title":"On the structure of abstract algebras","volume":"31","author":"Birkhoff","year":"1935","journal-title":"Proc. Cambridge Phil. Soc."},{"key":"10.1016\/S0168-0072(01)00078-1_BIB2","unstructured":"L. Colson, About primitive recursive algorithms, in: G. Ausiello, M. Dezani-Ciancaglini, S. Ronchi Della Rocca (Eds.), Proc. 16th Int. Coll. on Automata, Languages and Programming, Stresa, Italy, Lecture Notes in Computer Science, Vol. 372, Springer, Berlin, July 1989, pp. 194\u2013206."},{"key":"10.1016\/S0168-0072(01)00078-1_BIB3","series-title":"Higher Set Theory","first-page":"21","article-title":"Classically and intuitionistically provable recursive functions","author":"Friedman","year":"1978"},{"key":"10.1016\/S0168-0072(01)00078-1_BIB4","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","article-title":"\u00dcber eine bisher noch nicht benutzte erweiterung des finiten standpunktes","volume":"12","author":"G\u00f6del","year":"1958","journal-title":"Dialectica"},{"year":"1967","series-title":"From Frege to G\u00f6del, A Source Book in Mathematical Logic, 1879\u20131931","author":"van Heijenoort","key":"10.1016\/S0168-0072(01)00078-1_BIB5"},{"key":"10.1016\/S0168-0072(01)00078-1_BIB6","unstructured":"W. A. Howard, The formulae-as-types notion of construction, in: J.P. Seldin, J.R. Hindley (Eds.), To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, New York, 1980. Preliminary manuscript: 1969, pp. 479\u2013490."},{"year":"1952","series-title":"Introduction to Metamathematics","author":"Kleene","key":"10.1016\/S0168-0072(01)00078-1_BIB7"},{"key":"10.1016\/S0168-0072(01)00078-1_BIB8","first-page":"95","article-title":"Mathematical logic","volume":"Vol. III","author":"Kreisel","year":"1965"},{"key":"10.1016\/S0168-0072(01)00078-1_BIB9","first-page":"182","article-title":"Strong normalization for arithmetic","volume":"Vol. 500","author":"Leivant","year":"1975"},{"key":"10.1016\/S0168-0072(01)00078-1_BIB10","series-title":"Proc. 24th Ann. Symp. on the Foundations of Computer Science, Washington","first-page":"460","article-title":"Reasoning about functional programs and complexity classes associated with type disciplines","author":"Leivant","year":"1983"},{"key":"10.1016\/S0168-0072(01)00078-1_BIB11","series-title":"Logic and Computer Science","first-page":"279","article-title":"Contracting proofs to programs","author":"Leivant","year":"1990"},{"key":"10.1016\/S0168-0072(01)00078-1_BIB12","series-title":"Feasible Mathematics II","first-page":"320","article-title":"Ramified recurrence and computational complexity I: world recurrence and poly-time","author":"Leivant","year":"1994"},{"key":"10.1016\/S0168-0072(01)00078-1_BIB13","series-title":"Logic and Computational Complexity","first-page":"177","article-title":"Intrinsic theories and computational complexity","volume":"Vol. 960","author":"Leivant","year":"1995"},{"key":"10.1016\/S0168-0072(01)00078-1_BIB14","series-title":"Handbook of Logic in Computer Science","first-page":"189","article-title":"Universal algebra","author":"Meinke","year":"1992"},{"year":"1994","series-title":"Universal Algebra, Algebraic Logic, and Databases","author":"Plotkin","key":"10.1016\/S0168-0072(01)00078-1_BIB15"},{"year":"1965","series-title":"Natural Deduction","author":"Prawitz","key":"10.1016\/S0168-0072(01)00078-1_BIB16"},{"key":"10.1016\/S0168-0072(01)00078-1_BIB17","series-title":"Proc. 2nd Scandinavian Logic Symp.","first-page":"235","article-title":"Ideas and results in proof theory","author":"Prawitz","year":"1971"},{"key":"10.1016\/S0168-0072(01)00078-1_BIB18","doi-asserted-by":"crossref","unstructured":"M. Sch\u00f6nfinkel, \u00dcber die Bausteine der mathematischen Logik, Mathematische Annalen 92 (1924) 305\u2013316. (English translation: On the building blocks of mathematical logic, in [5, pp. 355\u2013366]).","DOI":"10.1007\/BF01448013"},{"year":"1973","series-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Vol. 344","author":"Troelstra","key":"10.1016\/S0168-0072(01)00078-1_BIB19"},{"year":"1992","series-title":"Universal Algebra for Computer Scientists","author":"Wechler","key":"10.1016\/S0168-0072(01)00078-1_BIB20"}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007201000781?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007201000781?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T10:03:05Z","timestamp":1759140185000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0168007201000781"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,4]]},"references-count":20,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2002,4]]}},"alternative-id":["S0168007201000781"],"URL":"https:\/\/doi.org\/10.1016\/s0168-0072(01)00078-1","relation":{},"ISSN":["0168-0072"],"issn-type":[{"type":"print","value":"0168-0072"}],"subject":[],"published":{"date-parts":[[2002,4]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Intrinsic reasoning about functional programs I: first order theories","name":"articletitle","label":"Article Title"},{"value":"Annals of Pure and Applied Logic","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S0168-0072(01)00078-1","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}