This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
[Barendregt 1992]H.P. Barendregt, Typed lambda calculi. In Handbook of Logic in Computer Science, eds. Abramski et al., Oxford Univ. Press.
[Barendsen and Geuvers 1989]E. Barendsen and H. Geuvers, λP is conservative over first order predicate logic, Manuscript, Faculty of Mathematics and Computer Science, University of Nijmegen, Netherlands.
[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.
[Berardi 1989]S. Berardi, Talk given at the ‘Jumelage meeting on typed lambda calculus', Edinburgh, September 1989.
[Berardi 1990]S. Berardi, Type dependence and constructive mathematics, Ph.D. thesis, Universita di Torino, Italy.
[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–606.
[Coquand 1985]Th. Coquand, Une théorie des constructions, Thèse de troisième cycle, Université Paris VII, France, January 1985.
[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–122.
[Coquand and Huet 1988]Th. Coquand and G. Huet, The calculus of constructions, Information and Computation, 76, pp 95–120.
[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.
[Gabbay 1981]D.M. Gabbay, Semantical investigations in Heyting's intuitionistic logic, Synthese Library, vol 148, Reidel, Dordrecht.
[Geuvers 1989]J.H. Geuvers, Talk given at the ‘Jumelage meeting on typed lambda calculus”, Edinburgh, September 1989.
[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–189.
[Geuvers 1993]J.H. Geuvers, Logics and Type systems, PhD. Thesis, University of Nijmegen, Netherlands.
[Girard 1972]J.-Y. Girard, Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur. Ph.D. thesis, Université Paris VII, France.
[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.
[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–204.
[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–490.
[Löb 1976]M. Löb, Embedding first order predicate logic in fragments of intuitionistic logic, J. Symbolic Logic vol 41, 4, pp. 705–719.
[Longo and Moggi 1988]G. Longo and E. Moggi, Constructive Natural Deduction and its ‘Modest’ Interpretation. Report CMU-CS-88-131.
[Paulin 1989]Ch. Paulin-Mohring, Extraction des programmes dans le calcul des constructions, Thèse, Université Paris VII, France.
[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–52.
[Ruys 1991]M. Ruys, λPω is not conservative over λP2, Master's thesis, University of Nijmegen, Netherlands, November 1991.
[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–276.
[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.
[Verschuren 1990]E. Verschuren, Conservativity in Barendregt's cube, Master's thesis, University of Nijmegen, Netherlands, December 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Geuvers, H. (1994). Conservativity between logics and typed λ calculi. In: Barendregt, H., Nipkow, T. (eds) Types for Proofs and Programs. TYPES 1993. Lecture Notes in Computer Science, vol 806. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58085-9_73
Download citation
DOI: https://doi.org/10.1007/3-540-58085-9_73
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58085-0
Online ISBN: 978-3-540-48440-0
eBook Packages: Springer Book Archive