{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:14:13Z","timestamp":1725664453638},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540587156"},{"type":"electronic","value":"9783540490548"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58715-2_114","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:42:32Z","timestamp":1330274552000},"page":"60-76","source":"Crossref","is-referenced-by-count":6,"title":["Inductive definitions and type theory an introduction (preliminary version)"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"Peter","family":"Dybjer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"P. Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739\u2013782. North-Holland, 1977.","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"6_CR2","unstructured":"S. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Department of Computer Science, Cornell University, 1987."},{"key":"6_CR3","unstructured":"H. P. Barendregt. The Lambda Calculus. North-Holland, 1984. Revised edition."},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"M. Beeson. Foundations of Constructive Mathematics. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-68952-9"},{"key":"6_CR5","volume-title":"Iterated Inductive Definitions and Subsystems of Analysis","author":"F. S. P. W. Buchholz","year":"1981","unstructured":"F. S. P. W. Buchholz, W. and S. W. Iterated Inductive Definitions and Subsystems of Analysis. Springer, Berlin, 1981."},{"key":"6_CR6","first-page":"135","volume":"39","author":"R. M. Burstall","year":"1985","unstructured":"R. M. Burstall. Proving properties of programs by structural induction. Computer Journal, (39): 135\u2013154, 1985.","journal-title":"Computer Journal"},{"key":"6_CR7","unstructured":"T. Coquand. Infinite objects in type theory. In Proceedings of the 1993 TYPES Workshop, Nijmegen, LNCS 806, 1993."},{"key":"6_CR8","unstructured":"J. Despeyroux. Proof of translation in natural semantics. In Proceedings of the First ACM Conference on Logic in Computer Science, pages 193\u2013205, 1986."},{"key":"6_CR9","unstructured":"E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"P. Dybjer. Inductive families. Formal Aspects of Computing. To appear.","DOI":"10.1007\/BF01211308"},{"key":"6_CR11","unstructured":"K. G\u00f6del. Collected Works, Volumes I and II. Oxford University Press, 1986."},{"key":"6_CR12","unstructured":"J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types. Prentice Hall, 1978."},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"D. Gries. The Science of Programming. Springer Texts and Monographs in Computer Science, 1981.","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"6_CR14","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/BF03037052","volume":"2","author":"M. Hagiya","year":"1984","unstructured":"M. Hagiya and T. Sakurai. Foundation of logic programming based on inductive definition. New Generation Computing, 2: 59\u201377, 1984.","journal-title":"New Generation Computing"},{"key":"6_CR15","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1016\/0304-3975(87)90073-9","volume":"53","author":"L. Halln\u00e4s","year":"1991","unstructured":"L. Halln\u00e4s. Partial inductive definitions. Theoretical Computer Science, 53: 335\u2013343, 1991.","journal-title":"Theoretical Computer Science"},{"key":"6_CR16","unstructured":"J. Herbrand. On the consistency of arithmetic. In J. van Heijenoort, editor, From Frege to G\u00f6del, pages 618\u2013628. Harvard University Press."},{"key":"6_CR17","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BF00976239","volume":"4","author":"C. Hoare","year":"1975","unstructured":"C. Hoare. Recursive data structures. International Journal of Computer and Information Sciences, 4: 105\u2013124, 1975.","journal-title":"International Journal of Computer and Information Sciences"},{"key":"6_CR18","unstructured":"W. Howard. Functional interpretation of bar induction by bar recursion. Compositio Mathematica, 20:107\u2013124."},{"key":"6_CR19","unstructured":"G. Kahn. Natural semantics. Technical Report 601, 1987."},{"key":"6_CR20","doi-asserted-by":"crossref","first-page":"109","DOI":"10.2307\/2269016","volume":"10","author":"S. Kleene","year":"1945","unstructured":"S. Kleene. On the interpretation of intuitionistic number theory. Journal of Symbolic Logic, 10: 109\u2013124, 1945.","journal-title":"Journal of Symbolic Logic"},{"key":"6_CR21","unstructured":"G. Kreisel. Interpretation of analysis by mean of constructive functionals of finite type. In Heyting, editor, Constructivity in Mathematics, pages 101\u2013128. North-Holland, 1959."},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"F. W. Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. In A. Heller, editor, Applications of Categorical Algebra, Proceedings of Symposia in Pure Mathematics. AMS, 1970.","DOI":"10.1090\/pspum\/017\/0257175"},{"key":"6_CR23","unstructured":"K. Lorenzen. M\u00e9tamath\u00e9matique. Edition Gauthier-Villars, 1962."},{"key":"6_CR24","volume-title":"Notes on Constructive Mathematics","author":"P. Martin-L\u00f6f","year":"1968","unstructured":"P. Martin-L\u00f6f. Notes on Constructive Mathematics. Almqvist & Wiksell, Stockholm, 1968."},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 179\u2013216. North-Holland, 1971.","DOI":"10.1016\/S0049-237X(08)70847-4"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f. An intuitionistic theory of types: Predicative part. In Logic Colloquium'73, pages 73\u2013118. North-Holland, 1975.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"6_CR27","unstructured":"P. Martin-L\u00f6f. The domain interpretation of type theory, lecture notes. In K. Karlsson and K. Petersson, editors, Workshop on Semantics of Programming Languages, Abstracts and Notes, Chalmers University of Technology and University of G\u00f6teborg, August 1983. Programming Methodology Group."},{"key":"6_CR28","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984."},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"J. McCarthy and J. A. Painter. Correctness of a compiler for arithmetic expressions. In Mathematical Aspects of Computer Science, pages 33\u201341. AMS, 1967.","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"D. R. Musser. On proving inductive properties of abstract data types. POPL, pages 154\u2013162, 1980.","DOI":"10.1145\/567446.567461"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Extracting f\u03c9 programs from proofs in the calculus of constructions. In Sixteenth Annual ACM Symposium on Principles of Programing Languages. ACM, 1989.","DOI":"10.1145\/75277.75285"},{"key":"6_CR32","series-title":"Technical Report DAIMI FN-19","volume-title":"A structural approach to operational semantics","author":"G. D. Plotkin","year":"1981","unstructured":"G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Depratment, Aarhus University, Aarhus, Denmark, 1981."},{"key":"6_CR33","volume-title":"The undecidable","author":"E. Post","year":"1965","unstructured":"E. Post. Absolutely unsolvable problems and relatively undecidable propositions. account of an anticipation. In M. Davis, editor, The undecidable. Raven Press, Hewlett, NY, 1965."},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"M. Sato. Adding proof objects and inductive definition mechanisms to frege structure. In D. H. Pitt, A. Poign\u00e9, and D. E. Rydeheard, editors, Proceeding of International Conference on Theoretical Aspects of Computer Software, pages 53\u201387. Springer-Verlag, LNCS 526, 1991.","DOI":"10.1007\/3-540-54415-1_41"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"D. S. Scott. Constructive validity. In Symposium on Automatic Demonstration, pages 237\u2013275. Springer Lecture Notes in Mathematics 125, 1970.","DOI":"10.1007\/BFb0060636"},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"W. W. Tait. Normal Derivability in Classical Logic. Springer, 1968.","DOI":"10.1007\/BFb0079691"},{"key":"6_CR37","unstructured":"M. Tatsuta. Realiability interpretation of coinductive definitions and program synthesis with streams. Proceedings of International Conference on Fifth Generation Computer Systems, pages 666\u2013673, 1992."},{"key":"6_CR38","unstructured":"A. S. Troelstra and D. van Dalen. Constructivism in Mathematics, an introduction. North-Holland, 1988."},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"J. Webb. Mechanism, Mentalism and Metamathematics. D. Reidel Publishing Company, 1980.","DOI":"10.1007\/978-94-015-7653-6"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"G. Winskel. The Formal Semantics of Programming Languages, an Introduction. MIT Press, 1993.","DOI":"10.7551\/mitpress\/3054.001.0001"}],"container-title":["Lecture Notes in Computer Science","Foundation of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58715-2_114.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:20:01Z","timestamp":1619572801000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58715-2_114"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540587156","9783540490548"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/3-540-58715-2_114","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}