{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T22:00:25Z","timestamp":1775944825800,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540523352","type":"print"},{"value":"9783540469636","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52335-9_47","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:31:29Z","timestamp":1330205489000},"page":"50-66","source":"Crossref","is-referenced-by-count":121,"title":["Inductively defined types"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"Christine","family":"Paulin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"5_CR1","unstructured":"P. Aczel. \u201cThe strength of Martin-L\u00f6f's intuitionistic type theory with one universe.\u201d In the Proceedings of the Symposium on Mathematical Logic, Helsinki, 1977."},{"key":"5_CR2","unstructured":"R. Backhouse. \u201cOn the meaning and construction of the rules in Martin-L\u00f6f's theory of types.\u201d Technical Report CS 8606, University of Groningen, 1986."},{"key":"5_CR3","volume-title":"Foundations of Constructive Analysis","author":"E. Bishop","year":"1967","unstructured":"E. Bishop. \u201cFoundations of Constructive Analysis.\u201d McGraw-Hill, New-York, 1967."},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"C. B\u00f6hm and A. Berarducci. \u201cAutomatic synthesis of typed A-programs on term algebras.\u201d Theoretical Computer Science, 39, 1985.","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"A. Church. \u201cA formulation of the simple theory of types.\u201d Journal of Symbolic Logic 5, 1940.","DOI":"10.2307\/2266170"},{"key":"5_CR6","unstructured":"Th. Coquand. \u201cAn introduction to type theory.\u201d Course notes, Albi, 1989."},{"key":"5_CR7","unstructured":"Th. Coquand. \u201cAn Analysis of Girard's Paradox.\u201d Proceedings of the first Logic in Computer Science, Boston, 1986."},{"key":"5_CR8","unstructured":"P. Dybjer. \u201cInductively Defined Types in Martin-L\u00f6f's Set Theory.\u201d Unpublished manuscript, 1987."},{"key":"5_CR9","unstructured":"P. Dybjer. \u201cAn inversion principle for Martin-L\u00f6f's type theory.\u201d To appear in the proceedings of Bastad, 1989."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"K. G\u00f6del. \u201cOn a hitherto unexploited extension of the finitist viewpoint.\u201d Translation by W. Hodge, appeared in Journal of Philosophical Logic 9 (1980).","DOI":"10.1007\/BF00247744"},{"key":"5_CR11","unstructured":"D. Hilbert. \u201cOn the Infinite.\u201d Published in Van Heijenoort."},{"key":"5_CR12","unstructured":"P. Martin-L\u00f6f. \u201cNotes on Constructive Mathematics.\u201d Almqvist & Wiksell, Stockholm."},{"key":"5_CR13","unstructured":"P. Martin-L\u00f6f. \u201cIntuitionistic Type Theory.\u201d Bibliopolis, 1980."},{"key":"5_CR14","unstructured":"P. F. Mendler. \u201cInductive Definition in Type Theory.\u201d Ph. D. Thesis, Cornell, 1987."},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"P.J. Landin. \u201cThe mechanical evaluation of expressions.\u201d Comput. J. 6, 1964.","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"5_CR16","unstructured":"Z. Luo. \u201cCC and its meta Theory.\u201d LFCS report ECS-LFCS-88-57, Dept. of Computer Science, University of Edinburgh."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Z. Luo. \u201cECC, an Extended calculus of Constructions.\u201d Proc. of the Fourth IEEE Symposium on Logics in Computer Science, June 1989, Asilomar, California, U.S.A.","DOI":"10.1109\/LICS.1989.39193"},{"key":"5_CR18","unstructured":"Ch. Paulin-Mohring. \u201cExtraction de programmes dans le Calcul des Constructions.\u201d Th\u00e8se, Universit\u00e9 Paris 7, 1989."},{"key":"5_CR19","unstructured":"D. Normann. \u201cInductively and recursively defined types.\u201d A seminar report, Department of Mathematics, University of Oslo, 1987."},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. \u201cA formulation of the Simple Theory of Types (for Isabelle).\u201d Unpublished manuscript, Cambridge, 1989.","DOI":"10.1007\/3-540-52335-9_58"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"F. Pfenning and Ch. Paulin-Mohring. \u201cInductively Defined Types in the Calculus of Constructions.\u201d To appear in the proceedings of MFPLS'89, 1989.","DOI":"10.1007\/BFb0040259"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"J.C. Reynolds. \u201cPolymorphism is not Set-Theoretic.\u201d Lecture Notes in Computer Science 173, Springer-Verlag, 1984.","DOI":"10.1007\/3-540-13346-1_7"},{"key":"5_CR23","unstructured":"B. Russell and A.N. Whitehead. \u201cPrincipia Mathematica.\u201d Volume 1,2,3 Cambridge University Press, 1912."},{"key":"5_CR24","unstructured":"J.R. Shoenfield. \u201cMathematical Logic.\u201d Addison-Wesley, 1967."},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"S.S. Wainer. \u201cSlow Growing Versus Fast Growing.\u201d Journal of Symbolic Logic, Volume 54, 1989.","DOI":"10.2307\/2274873"}],"container-title":["Lecture Notes in Computer Science","COLOG-88"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52335-9_47.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T21:00:39Z","timestamp":1742590839000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52335-9_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540523352","9783540469636"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-52335-9_47","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990]]}}}