{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,6]],"date-time":"2022-12-06T07:23:14Z","timestamp":1670311394094},"publisher-location":"New York, NY","reference-count":27,"publisher":"Springer-Verlag","isbn-type":[{"value":"9780387973753","type":"print"},{"value":"9780387348087","type":"electronic"}],"license":[{"start":{"date-parts":[[1990,1,1]],"date-time":"1990-01-01T00:00:00Z","timestamp":631152000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/bfb0040259","type":"book-chapter","created":{"date-parts":[[2006,8,17]],"date-time":"2006-08-17T17:01:43Z","timestamp":1155834103000},"page":"209-228","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":33,"title":["Inductively defined types in the Calculus of Constructions"],"prefix":"10.1007","author":[{"given":"Frank","family":"Pfenning","sequence":"first","affiliation":[]},{"given":"Christine","family":"Paulin-Mohring","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"8_CR1","series-title":"Technical Report","volume-title":"Using typed lambda calculus to implement formal systems on a machine","author":"A. Avron","year":"1987","unstructured":"Arnon Avron, Furio A. Honsell, and Ian A. Mason. Using typed lambda calculus to implement formal systems on a machine. Technical Report ECS-LFCS-87-31, Laboratory for Foundations of Computer Science, University of Edinburgh, Edinburgh, Scotland, June 1987."},{"key":"8_CR2","unstructured":"Henk Barendregt. The forest of lambda calculi with types. Talk given at the Workshop on Semantics of Lambda Calculus and Category Theory, Carnegie Mellon University, April 1988."},{"key":"8_CR3","first-page":"137","volume":"372","author":"V. Breazu-Tannen","year":"1989","unstructured":"Val Breazu-Tannen and Jean Gallier. Polymorphic rewriting conserves algebraic strong normalization and confluence. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, Stresa, Italy, pages 137\u2013150. Springer-Verlag LNCS 372, July 1989.","journal-title":"LNCS"},{"key":"8_CR4","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","volume":"39","author":"C. B\u00f6hm","year":"1985","unstructured":"Corrado B\u00f6hm and Alessandro Berarducci. Automatic synthesis of typed \u2227-programs on term algebras. Theoretical Computer Science, 39:135\u2013154, 1985.","journal-title":"Theoretical Computer Science"},{"key":"8_CR5","first-page":"194","volume":"372","author":"L. Colson","year":"1989","unstructured":"Lo\u00efc Colson. About primitive recursive algorithms. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, Stresa, Italy, pages 194\u2013206. Springer-Verlag LNCS 372, July 1989.","journal-title":"LNCS"},{"key":"8_CR6","unstructured":"Thierry Coquand. Une Th\u00e9orie des Constructions. PhD thesis, University Paris VII, January 1985."},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Thierry Coquand and G\u00e9rard Huet. Constructions: A higher order proof system for mechanizing mathematics. In EUROCAL85. Springer-Verlag LNCS 203, 1985.","DOI":"10.1007\/3-540-15983-5_13"},{"issue":"2\/3","key":"8_CR8","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Thierry Coquand and G\u00e9rard Huet. The Calculus of Constructions. Information and Computation, 76(2\/3):95\u2013120, February\/March 1988.","journal-title":"Information and Computation"},{"key":"8_CR9","unstructured":"Thierry Coquand and Christine Paulin-Mohring. Inductively defined types. Talk presented at the Workshop on Programming Logic, University of G\u00f6teborg and Chalmers University of Technology, May 1989."},{"issue":"5","key":"8_CR10","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. G. Bruijn de","year":"1972","unstructured":"N. G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math., 34(5):381\u2013392, 1972.","journal-title":"Indag. Math."},{"key":"8_CR11","unstructured":"Peter Dybjer. An inversion principle for Martin-L\u00f6f's type theory. Talk presented at the Workshop on Programming Logic, University of G\u00f6teborg and Chalmers University of Technology, May 1989."},{"key":"8_CR12","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/322358.322370","volume":"30","author":"S. Fortune","year":"1983","unstructured":"Steven Fortune, Daniel Leivant, and Michael O'Donnell. The expressiveness of simple and second-order type structures. Journal of the ACM, 30:151\u2013185, 1983.","journal-title":"Journal of the ACM"},{"key":"8_CR13","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0049-237X(08)70843-7","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"J. Girard","year":"1971","unstructured":"Jean-Yves Girard. Une extension de l'interpr\u00e9tation de G\u00f6del \u00e0 l'analyse, et son application a l'\u00e9limination des coupures dans l'analyse et la th\u00e9orie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 63\u201392, Amsterdam, London, 1971. North-Holland Publishing Co."},{"key":"8_CR14","unstructured":"Jean-Yves Girard. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII, 1972."},{"key":"8_CR15","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. In Symposium on Logic in Computer Science, pages 194\u2013204. IEEE, June 1987."},{"key":"8_CR16","unstructured":"G\u00e9rard Huet. Formal structures for computation and deduction. Lecture notes for a graduate course at Carnegie Mellon University, May 1986."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Daniel Leivant. Reasoning about functional programs and complexity classes associated with type disciplines. In Proceedings of the Twenty Fourth Annual Symposium on the Foundations of Computer Science, pages 160\u2013169. IEEE, 1983.","DOI":"10.1109\/SFCS.1983.50"},{"key":"8_CR18","unstructured":"Daniel Leivant. Contracting proofs to programs. In P. Odifreddi, editor, Logic and Computer Science. Academic Press, 1990. To appear."},{"key":"8_CR19","series-title":"Technical Report","volume-title":"First-and second-order lambda calculi with recursive types","author":"N. P. Mendler","year":"1986","unstructured":"N. P. Mendler. First-and second-order lambda calculi with recursive types. Technical Report TR 86-764, Department of Computer Science, Cornell University, Ithaca, New York, July 1986."},{"key":"8_CR20","unstructured":"Paul Francis Mendler. Inductive Definition in Type Theory. PhD thesis, Department of Computer Science, Cornell University, September 1987."},{"key":"8_CR21","first-page":"225","volume":"193","author":"J. C. Mitchell","year":"1985","unstructured":"John C. Mitchell and Albert Meyer. Second-order logical relations. In Rohit Parikh, editor, Logics of Programs, pages 225\u2013236. Springer-Verlag LNCS 193, June 1985.","journal-title":"LNCS"},{"key":"8_CR22","unstructured":"Michel Parigot. On the representation of data in lambda-calculus. Draft, 1988."},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Christine Paulin-Mohring. Extracting F\n \u03c9 programs from proofs in the calculus of constructions. In Sixteenth Annual Symposium on Principles of Programming Languages, pages 89\u2013104. ACM Press, January 1989.","DOI":"10.1145\/75277.75285"},{"key":"8_CR24","unstructured":"Christine Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. PhD thesis, Universit\u00e9 Paris VII, January 1989."},{"key":"8_CR25","first-page":"345","volume":"352","author":"F. Pfenning","year":"1989","unstructured":"Frank Pfenning and Peter Lee. Metacircularity in the polymorphic lambda-calculus. Theoretical Computer Science, 1990. To appear. A preliminary version appeared in TAPSOFT '89, Proceedings of the International Joint Conference on Theory and Practice in Software Development, Barcelona, Spain, pages 345\u2013359, Springer-Verlag LNCS 352, March 1989.","journal-title":"LNCS"},{"key":"8_CR26","unstructured":"John Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513\u2013523. Elsevier Science Publishers B. V., 1983."},{"key":"8_CR27","first-page":"97","volume":"185","author":"J. Reynolds","year":"1985","unstructured":"John Reynolds. Three approaches to type structure. In Hartmut Ehrig, Christiane Floyd, Maurice Nivat, and James Thatcher, editors, Mathematical Foundations of Software Development, pages 97\u2013138. Springer-Verlag LNCS 185, March 1985.","journal-title":"LNCS"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Programming Semantics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0040259","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:21:54Z","timestamp":1558272114000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0040259"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9780387973753","9780387348087"],"references-count":27,"URL":"http:\/\/dx.doi.org\/10.1007\/bfb0040259","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1990]]},"assertion":[{"value":"9 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}