{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:11:06Z","timestamp":1725664266039},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540580850"},{"type":"electronic","value":"9783540484400"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58085-9_73","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:11:32Z","timestamp":1330269092000},"page":"79-107","source":"Crossref","is-referenced-by-count":6,"title":["Conservativity between logics and typed \u03bb calculi"],"prefix":"10.1007","author":[{"given":"Herman","family":"Geuvers","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"5_CR1","unstructured":"[Barendregt 1992]H.P. Barendregt, Typed lambda calculi. In Handbook of Logic in Computer Science, eds. Abramski et al., Oxford Univ. Press."},{"key":"5_CR2","volume-title":"\u03bbP is conservative over first order predicate logic, Manuscript","author":"E. Barendsen","year":"1989","unstructured":"[Barendsen and Geuvers 1989]E. Barendsen and H. Geuvers, \u03bbP is conservative over first order predicate logic, Manuscript, Faculty of Mathematics and Computer Science, University of Nijmegen, Netherlands."},{"key":"5_CR3","volume-title":"Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt's cube","author":"S. Berardi","year":"1988","unstructured":"[Berardi 1988]S. Berardi, Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt's cube. Dept. Computer Science, Carnegie-Mellon University and Dipartimento Matematica, Universita di Torino, Italy."},{"key":"5_CR4","unstructured":"[Berardi 1989]S. Berardi, Talk given at the \u2018Jumelage meeting on typed lambda calculus', Edinburgh, September 1989."},{"key":"5_CR5","volume-title":"Ph.D. thesis","author":"S. Berardi","year":"1990","unstructured":"[Berardi 1990]S. Berardi, Type dependence and constructive mathematics, Ph.D. thesis, Universita di Torino, Italy."},{"key":"5_CR6","first-page":"580","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"N.G. Bruijn de","year":"1980","unstructured":"[De Bruijn 1980]N.G. de Bruijn, A survey of the project Automath, InTo H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, eds. J.P. Seldin, J.R. Hindley, Academic Press, New York, pp 580\u2013606."},{"key":"5_CR7","volume-title":"Th\u00e8se de troisi\u00e8me cycle","author":"T. Coquand","year":"1985","unstructured":"[Coquand 1985]Th. Coquand, Une th\u00e9orie des constructions, Th\u00e8se de troisi\u00e8me cycle, Universit\u00e9 Paris VII, France, January 1985."},{"key":"5_CR8","unstructured":"[Coquand 1990]Th. Coquand, Metamathematical investigations of a calculus of constructions. In Logic and Computer Science, ed. P.G. Odifreddi, APIC series, vol. 31, Academic Press, pp 91\u2013122."},{"key":"5_CR9","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"[Coquand and Huet 1988]Th. Coquand and G. Huet, The calculus of constructions, Information and Computation, 76, pp 95\u2013120.","journal-title":"Information and Computation"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"[Coquand and Huet 1985]Th. Coquand and G. Huet, Constructions: a higher order proof system for mechanizing mathematics. Proceedings of EUROCAL '85, Linz, LNCS 203.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"5_CR11","volume-title":"Synthese Library, vol 148","author":"D.M. Gabbay","year":"1981","unstructured":"[Gabbay 1981]D.M. Gabbay, Semantical investigations in Heyting's intuitionistic logic, Synthese Library, vol 148, Reidel, Dordrecht."},{"key":"5_CR12","unstructured":"[Geuvers 1989]J.H. Geuvers, Talk given at the \u2018Jumelage meeting on typed lambda calculus\u201d, Edinburgh, September 1989."},{"issue":"2","key":"5_CR13","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"J.H. Geuvers","year":"1991","unstructured":"[Geuvers and Nederhof] 1991J.H. Geuvers and M.J. Nederhof, A modular proof of strong normalisation for the calculus of constructions. Journal of Functional Programming, vol 1 (2), pp 155\u2013189.","journal-title":"Journal of Functional Programming"},{"key":"5_CR14","volume-title":"PhD. Thesis","author":"J.H. Geuvers","year":"1993","unstructured":"[Geuvers 1993]J.H. Geuvers, Logics and Type systems, PhD. Thesis, University of Nijmegen, Netherlands."},{"key":"5_CR15","volume-title":"Ph.D. thesis","author":"J.-Y. Girard","year":"1972","unstructured":"[Girard 1972]J.-Y. Girard, Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieur. Ph.D. thesis, Universit\u00e9 Paris VII, France."},{"key":"5_CR16","unstructured":"[Girard et al. 1989]J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and types, Camb. Tracts in Theoretical Computer Science 7, Cambridge University Press."},{"key":"5_CR17","first-page":"194","volume-title":"A framework for defining logics","author":"R. Harper","year":"1987","unstructured":"[Harper et al. 1987]R. Harper, F. Honsell and G. Plotkin, A framework for defining logics. Proceedings Second Symposium on Logic in Computer Science, (Ithaca, N.Y.), IEEE, Washington DC, pp 194\u2013204."},{"key":"5_CR18","first-page":"479","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"W.A. Howard","year":"1980","unstructured":"[Howard 1980]W.A. Howard, The formulas-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, eds. J.P. Seldin, J.R. Hindley, Academic Press, New York, pp 479\u2013490."},{"issue":"4","key":"5_CR19","doi-asserted-by":"crossref","first-page":"705","DOI":"10.2307\/2272390","volume":"41","author":"M. L\u00f6b","year":"1976","unstructured":"[L\u00f6b 1976]M. L\u00f6b, Embedding first order predicate logic in fragments of intuitionistic logic, J. Symbolic Logic vol 41, 4, pp. 705\u2013719.","journal-title":"J. Symbolic Logic"},{"key":"5_CR20","unstructured":"[Longo and Moggi 1988]G. Longo and E. Moggi, Constructive Natural Deduction and its \u2018Modest\u2019 Interpretation. Report CMU-CS-88-131."},{"key":"5_CR21","unstructured":"[Paulin 1989]Ch. Paulin-Mohring, Extraction des programmes dans le calcul des constructions, Th\u00e8se, Universit\u00e9 Paris VII, France."},{"issue":"1","key":"5_CR22","doi-asserted-by":"crossref","first-page":"33","DOI":"10.2307\/2275175","volume":"57","author":"A.M. Pitts","year":"1992","unstructured":"[Pitts 1992]A.M. Pitts, On an interpretation of second order quantification in first order intuitionistic propositional logic. J. Symbolic Logic vol 57, 1, pp.33\u201352.","journal-title":"J. Symbolic Logic"},{"key":"5_CR23","volume-title":"Master's thesis","author":"M. Ruys","year":"1991","unstructured":"[Ruys 1991]M. Ruys, \u03bbP\u03c9 is not conservative over \u03bbP2, Master's thesis, University of Nijmegen, Netherlands, November 1991."},{"key":"5_CR24","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/0168-0072(92)90044-Z","volume":"57","author":"H. Tonino","year":"1992","unstructured":"[Tonino and Fujita 1992]H. Tonino and K.-E. Fujita, On the adequacy of representing higher order intuitionistic logic as a pure type system, Annals of Pure and Applied Logic vol 57, pp 251\u2013276.","journal-title":"Annals of Pure and Applied Logic"},{"key":"5_CR25","unstructured":"[Troelstra and Van Dalen 1988]A. Troelstra and D. van Dalen, Constructivism in mathematics, an introduction, Volume I\/II, Studies in logic and the foundations of mathematics, vol 121 and volume 123, North-Holland."},{"key":"5_CR26","volume-title":"Master's thesis","author":"E. Verschuren","year":"1990","unstructured":"[Verschuren 1990]E. Verschuren, Conservativity in Barendregt's cube, Master's thesis, University of Nijmegen, Netherlands, December 1990."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58085-9_73.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:16:48Z","timestamp":1605647808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58085-9_73"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540580850","9783540484400"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-58085-9_73","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}