{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:39:30Z","timestamp":1767926370970,"version":"3.49.0"},"reference-count":12,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1988,9,1]],"date-time":"1988-09-01T00:00:00Z","timestamp":589075200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["BIT"],"published-print":{"date-parts":[[1988,9]]},"DOI":"10.1007\/bf01941137","type":"journal-article","created":{"date-parts":[[2005,7,31]],"date-time":"2005-07-31T10:23:42Z","timestamp":1122805422000},"page":"605-619","source":"Crossref","is-referenced-by-count":37,"title":["Terminating general recursion"],"prefix":"10.1007","volume":"28","author":[{"given":"Bengt","family":"Nordstr\u00f6m","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF01941137_CR1","doi-asserted-by":"crossref","unstructured":"Peter Aczel. An introduction to inductive definitions. In J. Barwise, editor,Handbook of Mathematical Logic, pages 739-, North-Holland Publishing Company, 1977.","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"BF01941137_CR2","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"R. L. Constable and et. al.Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986."},{"key":"BF01941137_CR3","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. InLogic, Methodology and Philosophy of Science, VI, 1979, pages 153\u2013175, North-Holland, 1982.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"BF01941137_CR4","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f Per","year":"1984","unstructured":"Per Martin-L\u00f6f.Intuitionistic Type Theory. Bibliopolis, Napoli, 1984."},{"key":"BF01941137_CR5","unstructured":"Bengt Nordstr\u00f6m and Kent Petersson.The Semantics of Module Specifications in Martin-L\u00f6f's Type Theory. PMG Report 36, Chalmers University of Technology, S-412 96 G\u00f6teborg, 1987."},{"key":"BF01941137_CR6","first-page":"915","volume-title":"Proceedings of IFIP 83","author":"Bengt Nordstr\u00f6m","year":"1983","unstructured":"Bengt Nordstr\u00f6m and Kent Petersson. Types and specifications. In R. E. A. Mason, editor,Proceedings of IFIP 83, pages 915\u2013920, Elsevier Science Publishers, Amsterdam, October 1983."},{"issue":"3","key":"BF01941137_CR7","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1007\/BF02136027","volume":"24","author":"Bengt Nordstr\u00f6m","year":"1984","unstructured":"Bengt Nordstr\u00f6m and Jan Smith. Propositions, types and specifications in Martin-L\u00f6f's type theory.BIT, 24(3):288\u2013301, October 1984.","journal-title":"BIT"},{"key":"BF01941137_CR8","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Constructing recursion operators in intuitionistic type theory.Journal of Symbolic Computation, (2):325\u2013355, 1986.","DOI":"10.1016\/S0747-7171(86)80002-5"},{"key":"BF01941137_CR9","series-title":"Technical report","volume-title":"Natural Deduction Proof as Higher-Order Resolution","author":"Lawrence C. Paulson","year":"1985","unstructured":"Lawrence C. Paulson.Natural Deduction Proof as Higher-Order Resolution. Technical report 82, University of Cambridge Computer Laboratory, Cambridge, 1985."},{"key":"BF01941137_CR10","unstructured":"Kent Petersson.A Programming System for Type Theory. PMG report 9, Chalmers University of Technology, S-412 96 G\u00f6teborg, 1982, 1984."},{"key":"BF01941137_CR11","volume-title":"Well-founded Recursion in Type theory","author":"E. Saaman","year":"1987","unstructured":"E. Saaman and G. Malcolm.Well-founded Recursion in Type theory. Technical Report, Subfaculteit Wiskunde en Informatica, Rijksuniversiteit Groningen, Netherlands, 1987."},{"key":"BF01941137_CR12","doi-asserted-by":"crossref","unstructured":"Jan M. Smith. The identification of propositions and types in Martin-L\u00f6f's type theory. InFoundations of Computation Theory, Proceedings of the Conference, pages 445\u2013456, 1983.","DOI":"10.1007\/3-540-12689-9_125"}],"container-title":["BIT"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01941137.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01941137\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01941137","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T13:26:46Z","timestamp":1586352406000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01941137"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988,9]]},"references-count":12,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1988,9]]}},"alternative-id":["BF01941137"],"URL":"https:\/\/doi.org\/10.1007\/bf01941137","relation":{},"ISSN":["0006-3835","1572-9125"],"issn-type":[{"value":"0006-3835","type":"print"},{"value":"1572-9125","type":"electronic"}],"subject":[],"published":{"date-parts":[[1988,9]]}}}