{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:21Z","timestamp":1761611061723},"reference-count":40,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2002,2,1]],"date-time":"2002-02-01T00:00:00Z","timestamp":1012521600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4184,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2002,2]]},"DOI":"10.1016\/s0304-3975(00)00355-8","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T06:11:15Z","timestamp":1027577475000},"page":"315-339","source":"Crossref","is-referenced-by-count":9,"title":["Least and greatest fixed points in intuitionistic natural deduction"],"prefix":"10.1016","volume":"272","author":[{"given":"Tarmo","family":"Uustalu","sequence":"first","affiliation":[]},{"given":"Varmo","family":"Vene","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(00)00355-8_BIB1","first-page":"3","article-title":"An introduction to the theory of lists","volume":"vol. 36","author":"Bird","year":"1987"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB2","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","article-title":"Automatic synthesis of typed \u039b-programs on term algebras","volume":"39","author":"B\u00f6hm","year":"1985","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB3","unstructured":"R. Cockett, T. Fukushima, About charity, Yellow Series Report 92\/480\/18, Dept. of Computer Science, University of Calgary, 1992."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB4","first-page":"50","article-title":"Inductively defined types (preliminary version)","volume":"vol. 417","author":"Coquand","year":"1990"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB5","series-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","first-page":"579","article-title":"A survey of the project AUTOMATH","author":"de Bruijn","year":"1980"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB6","unstructured":"M.M. Fokkinga, Law and order in algorithmics, Ph.D. Thesis, Dept. of Informatics, University of Twente, 1992."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB7","unstructured":"H. Geuvers, Inductive and coinductive types with iteration and recursion, in: B. Nordstr\u00f6m, K. Pettersson, G. Plotkin (Eds.), Informal Proc. Workshop on Types for Proofs and Programs B\u00e5stad, Sweden, June 1992, Dept. of Computing Science, Chalmers Univ. of Technology and G\u00f6teborg University, 1992, pp. 193\u2013217. ftp:\/\/ftp.cs.chalmers.se\/pub\/cs-reports\/baastad.92\/proc.ps.Z."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB8","first-page":"39","article-title":"Codifying guarded definitions with recursion schemes","volume":"vol. 996","author":"Gim\u00e9nez","year":"1995"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB9","first-page":"397","article-title":"Structural recursive definitions in type theory","volume":"vol. 1443","author":"Gim\u00e9nez","year":"1998"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB10","doi-asserted-by":"crossref","unstructured":"J. Greiner, Programming with inductive and co-inductive types, Tech. Report CMU-CS-92-109, School of Computer Science, Carnegie-Mellon Univ., Pittsburgh, PA, USA, 1992.","DOI":"10.21236\/ADA249562"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB11","unstructured":"T. Hagino, A categorical programming language, Ph.D. Thesis CST-47-87, Lab. for Foundations of Computer Science, Dept. of Computer Science, Univ. of Edinburgh, 1987."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB12","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A framework for defining logics","volume":"40","author":"Harper","year":"1993","journal-title":"J. ACM"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB13","unstructured":"B. Howard, Fixed points and extensionality in typed functional programming languages, Ph.D. Thesis, Tech. Report STAN-CS-92-1455, Computer Science Dept., Stanford Univ., CA, 1992."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB14","series-title":"Proc. 24th Annual IEEE Symp. on Foundations of Computer Science, FOCS\u201983, Tucson, AZ, USA, November 1983","first-page":"460","article-title":"Reasoning about functional programs and complexity classes associated with type disciplines","author":"Leivant","year":"1983"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB15","first-page":"279","article-title":"Contracting proofs to programs","volume":"vol. 31","author":"Leivant","year":"1990"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB16","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0167-6423(90)90023-7","article-title":"Data structures and program transformation","volume":"14","author":"Malcolm","year":"1990","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB17","first-page":"179","article-title":"Hauptsatz for the intuitionistic theory of iterated inductive definitions","volume":"vol. 63","author":"Martin-L\u00f6f","year":"1971"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB18","unstructured":"R. Matthes, Extensions of system F by iteration and primitive recursion on monotone inductive types, Ph.D. Thesis, Fachbereich Mathematik, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, 1998."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB19","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/BF01211391","volume":"4","author":"Meertens","year":"1992","journal-title":"Paramorphisms Formal Aspects Comput."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB20","unstructured":"N.P. Mendler, Recursive types and type constraints in second-order lambda-calculus, Proc. 2nd Annual IEEE Symp. on Logic in Computer Science, LICS\u201987, Ithaca, NY, USA, June 1987, IEEE CS Press, Los Alamitos, CA, 1987, pp. 30\u201336."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB21","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0168-0072(91)90069-X","article-title":"Inductive types and type constraints in the second-order lambda-calculus","volume":"51","author":"Mendler","year":"1991","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB22","volume":"vol. 7","author":"Nordstr\u00f6m","year":"1990"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB23","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0890-5401(92)90031-A","article-title":"The extended calculus of constructions (ECC) with inductive types","volume":"89","author":"Ore","year":"1992","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB24","first-page":"145","article-title":"Programming with proofs: a second order type theory","volume":"vol. 300","author":"Parigot","year":"1988"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB25","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1016\/0304-3975(92)90042-E","article-title":"Recursive programming with proofs","volume":"94","author":"Parigot","year":"1992","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB26","series-title":"Conf. Record 16th Annual ACM Symp. on Principles of Programming Languages, POPL\u201989, Austin, TX, USA, January 1989","first-page":"89","article-title":"Extracting F\u03c9's programs from proofs in the calculus of constructions","author":"Paulin-Mohring","year":"1989"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB27","first-page":"328","article-title":"Inductive definitions in the system Coq: rules and properties","volume":"vol. 664","author":"Paulin-Mohring","year":"1993"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB28","first-page":"209","article-title":"Inductively defined types in the calculus of constructions","volume":"vol. 442","author":"Pfenning","year":"1990"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB29","doi-asserted-by":"crossref","first-page":"1284","DOI":"10.2307\/2274279","article-title":"A natural extension of natural deduction","volume":"49","author":"Schroeder-Heister","year":"1984","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB30","first-page":"399","article-title":"Generalized rules for quantifiers and the completeness of the intuitionistic operators &, \u2228, \u2283, \u22a5, \u2200, \u2203","volume":"vol. 1104","author":"Schroeder-Heister","year":"1984"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB31","series-title":"Proc. 6th ACM SIGPLAN\/SIGARCH Internat. Conf. on Functional Programming Languages and Computer Architecture, FPCA\u201993, Copenhagen, Denmark, June 1993","first-page":"233","article-title":"A fold for all seasons","author":"Sheard","year":"1993"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB32","series-title":"Proc. 4th ACM SIGPLAN Internat. Conf. on Functional Programming, ICFP\u201999, Paris, France, September 1999","first-page":"102","article-title":"Type fixpoints","author":"Sp\u0142awski","year":"1999"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB33","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","article-title":"A lattice-theoretical fixpoint theorem and its applications","volume":"5","author":"Tarski","year":"1955","journal-title":"Pacific J. Math."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB34","first-page":"382","article-title":"Positive recursive type assignment","volume":"vol. 969","author":"Urzyczyn","year":"1995"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB35","unstructured":"T. Uustalu, Natural deduction for intuitionistic least and greatest fixedpoint logics, with an application to program construction, Ph.D. Thesis, Dissertation TRITA-IT AVH 98:03, Dept. of Teleinformatics, Royal Inst. of Technology, Stockholm, 1998."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB36","unstructured":"T. Uustalu, Multi-(co)iteration, categorically, in: J. Penjam (Ed.), Proc. 6th Fenno-Ugric Symp. on Software Technology, FUSST\u201999, Sagadi, Estonia, August 1999, Report CS 104\/99, Inst. of Cybernetics, Tallinn, 1999, pp. 259\u2013267."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB37","unstructured":"T. Uustalu, V. Vene, A cube of proof systems for the intuitionistic predicate \u03bc,\u03bd-logic, in: M. Haveraaen, O. Owe (Eds.), Selected Papers 8th Nordic Workshop on Programming Theory, NWPT\u201996, Oslo, Norway, December 1996, Research Report 248, Dept. of Informatics, University of Oslo, 1997, pp. 237\u2013246."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB38","first-page":"5","article-title":"Primitive (co)recursion and course-of-value (co)iteration, categorically","volume":"10","author":"Uustalu","year":"1999","journal-title":"INFORMATICA"},{"key":"10.1016\/S0304-3975(00)00355-8_BIB39","first-page":"343","article-title":"Mendler-style inductive types, categorically","volume":"6","author":"Uustalu","year":"1999","journal-title":"Nordic J. Comput."},{"key":"10.1016\/S0304-3975(00)00355-8_BIB40","unstructured":"T. Uustalu, V. Vene, Coding recursion \u00e0 la Mendler, in: J. Jeuring (Ed.), Proc. 2nd Workshop on Generic Programming, WGP\u201900, Ponte de Lima, Portugal, July 2000, Tech. Report UU-CS.2000-19, Computer Science Dept., Utrecht Univ., 2000, pp. 69\u201385."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500003558?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500003558?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,7]],"date-time":"2020-01-07T21:02:59Z","timestamp":1578430979000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397500003558"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,2]]},"references-count":40,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2002,2]]}},"alternative-id":["S0304397500003558"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00355-8","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2002,2]]}}}