{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:27:07Z","timestamp":1725460027921},"publisher-location":"Berlin\/Heidelberg","reference-count":18,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540582770"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0049337","type":"book-chapter","created":{"date-parts":[[2006,3,6]],"date-time":"2006-03-06T18:58:16Z","timestamp":1141671496000},"page":"280-294","source":"Crossref","is-referenced-by-count":6,"title":["Data types, infinity and equality in system AF 2"],"prefix":"10.1007","author":[{"given":"Christophe","family":"Raffalli","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, revised edition, 1984."},{"key":"18_CR2","volume-title":"Pubblicazioni 696","author":"C. B\u00f6hm","year":"1968","unstructured":"C. B\u00f6hm. Alcune proprieta delle forme \u03b2\u03b7-normali nel \u03bb\u03ba-calculus. Pubblicazioni 696, Instituto per le Applicazioni del Calcolo, Roma, 1968."},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"T. Coquand and G. Huet. The calculus of construction. In Information and Computation, pages 241\u2013262, 1988.","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"N. de Bruijn. The mathematical language automath, its usage and some of its extensions. In Symp. on automatic demonstration, pages 29\u201361. Springer Verlag, 1970. Lecture Notes in Mathematics Vol. 125.","DOI":"10.1007\/BFb0060623"},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","volume":"45","author":"J.-Y. Girard","year":"1986","unstructured":"J.-Y. Girard. The system F of variable types: fifteen years later. Theoretical Computer Science, 45:159\u2013192, 1986.","journal-title":"Theoretical Computer Science"},{"key":"18_CR6","unstructured":"W. Howard. The formulae-as-types notion of construction. To H.B. Curry: Essays on combinatory logic, \u03bb-calculus and formalism, pages 479\u2013490, 1980."},{"key":"18_CR7","unstructured":"Jean-Louis Krivine. Lambda-Calcul: Types et Mod\u00e8les, Etudes et Recherches en Informatique. Masson, 1990."},{"issue":"3","key":"18_CR8","first-page":"149","volume":"26","author":"J. Krivine","year":"1990","unstructured":"Jean-Louis Krivine and Michel Parigot. Programming with proofs. Inf. Process. Cybern., EIK 26(3):149\u2013167, 1990.","journal-title":"EIK"},{"key":"18_CR9","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(86)90109-X","volume":"44","author":"D. Leivant","year":"1986","unstructured":"Daniel Leivant. Typing and computational properties of lambda expressions. Theoretical Computer Science, 44:51\u201368, 1986.","journal-title":"Theoretical Computer Science"},{"key":"18_CR10","unstructured":"Daniel Leivant. Contracting proofs to programs. Logic and Computer Science, pages 279\u2013327, 1990."},{"key":"18_CR11","unstructured":"P. Martin-L\u00f6f. Lecture notes on the domain interpretation of type theory. In Programming Methodology Group, editor, Workshop on the Semantics of Programming Languages, G\u00f6teborg, Sweden, 1983. Chalmers University of Technology."},{"key":"18_CR12","unstructured":"Paul Francis Meadler. Inductive definition in type theory. PhD thesis, Cornell University, 1988."},{"key":"18_CR13","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/3-540-52753-2_47","volume":"440","author":"M. Parigot","year":"1989","unstructured":"Michel Parigot. On the representation of data in lambda-calculus. Lecture Notes in Computer Science, 440:309\u2013321, 1989.","journal-title":"Lecture Notes in Computer Science"},{"key":"18_CR14","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1016\/0304-3975(92)90042-E","volume":"94","author":"M. Parigot","year":"1992","unstructured":"Michel Parigot. Recursive programming with proofs. Theoritical Computer Science, 94:335\u2013356, 1992.","journal-title":"Theoritical Computer Science"},{"key":"18_CR15","doi-asserted-by":"crossref","first-page":"608","DOI":"10.1007\/3-540-57182-5_52","volume":"711","author":"M. Parigot","year":"1993","unstructured":"Michel Parigot and Paul Rozi\u00e8re. Constant time reduction in \u03bb-calculus. Lecture Note in Computer Science, 711:608\u2013617, 1993.","journal-title":"Lecture Note in Computer Science"},{"key":"18_CR16","unstructured":"C. Paulin-Mohring. Inductive definitions in the calculus of constructions. Technical report, INRIA, 1989. Technical Report Number 110."},{"key":"18_CR17","unstructured":"Christophe Raffalli. L'arithm\u00e9tique fonctionnelle du second ordre avec points fixes. PhD thesis, Universit\u00e9 Paris 7, F\u00e9vrier 1994."},{"key":"18_CR18","unstructured":"M. Tatsuta. Realizability interpretation of coinductive definitions and program synthesis using streams. In Proceedings of the fifth generation computer systems, pages 666\u2013673. ICOT, 1992."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0049337.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:55:45Z","timestamp":1607550945000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0049337"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540582770"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0049337","relation":{},"subject":[]}}