{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:12:30Z","timestamp":1776888750312,"version":"3.51.2"},"reference-count":25,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1991,9,1]],"date-time":"1991-09-01T00:00:00Z","timestamp":683683200000},"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":7990,"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":[[1991,9]]},"DOI":"10.1016\/s0304-3975(06)80007-1","type":"journal-article","created":{"date-parts":[[2007,9,16]],"date-time":"2007-09-16T07:02:58Z","timestamp":1189926178000},"page":"115-142","source":"Crossref","is-referenced-by-count":65,"title":["Partial inductive definitions"],"prefix":"10.1016","volume":"87","author":[{"given":"Lars","family":"Halln\u00e4s","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(06)80007-1_bib1","series-title":"Handbook of Mathematical Logic","article-title":"An introduction to inductive definitions","author":"Aczel","year":"1977"},{"key":"10.1016\/S0304-3975(06)80007-1_bib2","series-title":"The Kleene Symposium","article-title":"Frege structures and the notions of proposition, truth and set","author":"Aczel","year":"1980"},{"key":"10.1016\/S0304-3975(06)80007-1_bib3","series-title":"The Lambda Calculus","author":"Barendregt","year":"1984"},{"key":"10.1016\/S0304-3975(06)80007-1_bib4","author":"Cardelli","year":"1986","journal-title":"A. polymorphic \u03bb-calculus with Type: Type"},{"key":"10.1016\/S0304-3975(06)80007-1_bib5","article-title":"An analysis of Girards paradox","author":"Coquand","year":"1986","journal-title":"Proc. 2nd Symp. in Logic in Computer Science, IEEE"},{"key":"10.1016\/S0304-3975(06)80007-1_bib6","article-title":"A programming calculus based on partial inductive definitions","author":"Eriksson","year":"1988","journal-title":"SICS research report R88013"},{"key":"10.1016\/S0304-3975(06)80007-1_bib7","series-title":"Partial inductive definitions as type systems","author":"Fredholm","year":"1988"},{"key":"10.1016\/S0304-3975(06)80007-1_bib8","article-title":"A proof theoretic approach to logic programming. I Generalized Horn clauses","author":"Halln\u00e4s","year":"1988","journal-title":"J. Logic and Computation"},{"key":"10.1016\/S0304-3975(06)80007-1_bib9","article-title":"A Framework for defining logis","author":"Harper","year":"1986","journal-title":"Proc. 2nd Symp. in Logic in Computer Science, IEEE"},{"key":"10.1016\/S0304-3975(06)80007-1_bib10","doi-asserted-by":"crossref","DOI":"10.2307\/2024634","article-title":"An outline of a theory of truth","volume":"72","author":"Kripke","year":"1975","journal-title":"J. Philos."},{"key":"10.1016\/S0304-3975(06)80007-1_bib11","series-title":"Einf\u00fchrung in die Operativen Logik und Mathematik","author":"Lorenzen","year":"1969"},{"key":"10.1016\/S0304-3975(06)80007-1_bib12","series-title":"Proc. 2nd Scandinavian Logic Symposium","article-title":"Hauptsatz for the intuitionistic theory of iterated inductive definitions","author":"Martin-L\u00f6f","year":"1971"},{"key":"10.1016\/S0304-3975(06)80007-1_bib13","series-title":"Constructive mathematics and computer programming","author":"Martin-L\u00f6f","year":"1982"},{"key":"10.1016\/S0304-3975(06)80007-1_bib14","series-title":"On the meanings of the logical constants and the justifications of the logical laws","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/S0304-3975(06)80007-1_bib15","article-title":"Amendments to intuitionistic type theory","author":"Martin-L\u00f6f","year":"1986","journal-title":"Notes from a lecture given at Chalmers"},{"key":"10.1016\/S0304-3975(06)80007-1_bib16","article-title":"\u201cType\u201d is not a type","author":"Meyer","year":"1986","journal-title":"Proc. Conf. Record 13th Ann. Symp. on Principles of Programming Languages, ACM"},{"issue":"3","key":"10.1016\/S0304-3975(06)80007-1_bib17","doi-asserted-by":"crossref","DOI":"10.1007\/BF00248324","article-title":"The foundation of a generic theorem prover","volume":"5","author":"Paulson","year":"1988","journal-title":"J. Automat. Reason"},{"key":"10.1016\/S0304-3975(06)80007-1_bib18","series-title":"Proc. 2nd Scandinavian Symposium","article-title":"Ideas and results in proof theory","author":"Prawitz","year":"1971"},{"key":"10.1016\/S0304-3975(06)80007-1_bib19","series-title":"Logic, Methodology and the Philosophy of Sciences IV","article-title":"Towards a foundation of a general proof theory","author":"Prawitz","year":"1973"},{"key":"10.1016\/S0304-3975(06)80007-1_bib20","doi-asserted-by":"crossref","DOI":"10.1007\/BF00660889","article-title":"On the idea of a general proof theory","volume":"27","author":"Prawitz","year":"1974","journal-title":"Synthese"},{"key":"10.1016\/S0304-3975(06)80007-1_bib21","doi-asserted-by":"crossref","DOI":"10.1007\/BF00486044","article-title":"Remarks on some approaches to the concept of logical consequences","volume":"62","author":"Prawitz","year":"1985","journal-title":"Synthese"},{"key":"10.1016\/S0304-3975(06)80007-1_bib22","article-title":"Untersuchungen zur Regellogischen deutung von Aussagenverkn\u00fcpfungen","author":"Schroeder-Heister","year":"1981","journal-title":"Dissertation"},{"key":"10.1016\/S0304-3975(06)80007-1_bib23","doi-asserted-by":"crossref","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(06)80007-1_bib24","author":"Schroeder-Heister","year":"1985","journal-title":"Judgements of higher level and standardized rules for logical constants in Martin-L\u00f6fs theory of logic"},{"key":"10.1016\/S0304-3975(06)80007-1_bib25","doi-asserted-by":"crossref","DOI":"10.2307\/2271658","article-title":"Intensional interpretation of functionals of finite type","volume":"32","author":"Tait","year":"1967","journal-title":"J. Symbolic Logic"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397506800071?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397506800071?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T22:25:38Z","timestamp":1556835938000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397506800071"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,9]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1991,9]]}},"alternative-id":["S0304397506800071"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(06)80007-1","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1991,9]]}}}