{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:08:47Z","timestamp":1763467727792},"publisher-location":"Berlin\/Heidelberg","reference-count":11,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354051662X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0018349","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T07:50:09Z","timestamp":1132645809000},"page":"128-140","source":"Crossref","is-referenced-by-count":14,"title":["A set constructor for inductive sets in Martin-L\u00f6f's type theory"],"prefix":"10.1007","author":[{"given":"Kent","family":"Petersson","sequence":"first","affiliation":[]},{"given":"Dan","family":"Synek","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Roland Backhouse. On the meaning and construction of the rules in Martin-L\u00f6f's theory of types. In Proceedings of the Workshop on General Logic, Edinburgh, Laboratory for the Foundations of Computer Science, University of Edinburgh, February 1987."},{"key":"9_CR2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0167-6423(87)90002-5","volume":"8","author":"P. Chisholm","year":"1987","unstructured":"P. Chisholm. Derivation of a Parsing Algorithm in Martin-L\u00f6f's theory of types. Science of Computer Programming, 8:1\u201342, 1987.","journal-title":"Science of Computer Programming"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Robert L. Constable and Nax P. Mendler. Recursive Definitions in Type Theory. In Proceedings of the LICS-Conference, Brooklyn, N. Y., Lecture Notes in Computer Science, Springer-Verlag, June 1985.","DOI":"10.1007\/3-540-15648-8_5"},{"key":"9_CR4","volume-title":"Inductively Defined Sets in Martin-L\u00f6f's Type Theory","author":"P. Dybjer","year":"1987","unstructured":"Peter Dybjer. Inductively Defined Sets in Martin-L\u00f6f's Type Theory. 1987. Presented at the Workshop on General Logic, Edinburgh."},{"issue":"2","key":"9_CR5","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BF00976239","volume":"4","author":"C. A. R. Hoare","year":"1975","unstructured":"C. A. R. Hoare. Recursive Data Structures. International Journal of Computer and Information Sciences, 4(2):105\u2013132, 1975.","journal-title":"International Journal of Computer and Information Sciences"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. Constructive Mathematics and Computer Programming. In Logic, Methodology and Philosophy of Science, VI, 1979, pages 153\u2013175, North-Holland, 1982.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"9_CR7","volume-title":"Intuitionistic Type Theory","author":"P. Martin-L\u00f6f","year":"1984","unstructured":"Per Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984."},{"key":"9_CR8","unstructured":"R. Milner. Standard ML Proposal. Polymorphism: The ML\/LCF\/Hope Newsletter, 1(3), January 1984."},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Dana Scott. Domains for Denotational Semantics. In Automata, Languages and Programming, 9th Colloquium, pages 577\u2013613, Springer-Verlag, LNCS 140, July 1982.","DOI":"10.1007\/BFb0012801"},{"key":"9_CR10","unstructured":"Dan Synek. Deriving Rules for Inductive Sets in Martin-L\u00f6f's Type Theory. Technical Report, Programming Methodology Group, Dept. of Computer Science, Chalmers University of Technology, S-412 96 G\u00f6teborg, 1989. In preparation."},{"key":"9_CR11","first-page":"1","volume":"5","author":"A. Wijngarden van","year":"1974","unstructured":"A. van Wijngarden et al. Revised report on the Algorithmic Language, ALGOL 68. Acta Informatica, 5:1\u2013236, 1974.","journal-title":"Acta Informatica"}],"container-title":["Lecture Notes in Computer Science","Category Theory and Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0018349.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:41:09Z","timestamp":1607550069000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0018349"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354051662X"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/bfb0018349","relation":{},"subject":[]}}