Abstract
Pure Type Systems ( PTS β s) provide a parametric framework for typed λ-calculi à la Church [1,2,10,11]. One important aspect of PTS β s is to feature a definitional equality based on β-conversion. In some instances however, one desires a stronger definitional equality based on βη-conversion. The need for such a strengthened definitional equality arises for example when using type theory as a logical framework or in categorical type theory.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barendregt, H.: Introduction to Generalised Type Systems. Journal of Functional Programming 1(2), 125–154 (1991)
Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 117–309. Oxford Science Publications (1992)
Barras, B., et al.: The Coq Proof Assistant User’s Guide. Version 6.2 (May 1998)
Barthe, G.: Expanding the cube. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 90–104. Springer, Heidelberg (1999)
Barthe, G., Hatcliff, J., Sφrensen, M.H.B.: An induction principle for Pure Type Systems. Manuscript (1998)
Cornes, C.: Conception d’un langage de haut niveau de representation de preuves: Récurrence par filtrage de motifs; Unification en présence de types inductifs primitifs; Synthése de lemmes d’inversion. PhD thesis, Université de Paris 7 (1997)
Di Cosmo, R.: A brief history of rewriting with extensionality. Presented at the International Summer School on Type Theory and Term Rewriting, Glasgow (September 1996)
Dowek, G., Huet, G., Werner, B.: On the existence of long βη-normal forms in the cube. In: Geuvers, H. (ed.) TYPES 1993. LNCS, vol. 806, pp. 115–130. Springer, Heidelberg (1994)
Geuvers, H.: The Church-Rosser property for βη-reduction in typed λ-calculi. In: Proceedings of LICS 1992, pp. 453–460. IEEE Computer Society Press, Los Alamitos (1992)
Geuvers, H.: Logics and type systems. PhD thesis, University of Nijmegen (1993)
Geuvers, H., Nederhof, M.J.: A modular proof of strong normalisation for the Calculus of Constructions. Journal of Functional Programming 1(2), 155–189 (1991)
Geuvers, H., Werner, B.: On the Church-Rosser property for expressive type systems and its consequence for their metatheoretic study. In: Proceedings of LICS 1994, pp. 320–329. IEEE Computer Society Press, Los Alamitos (1994)
Ghani, N.: Eta-expansions in dependent type theory–the calculus of constructions. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 164–180. Springer, Heidelberg (1997)
Klop, J.W.: Term-rewriting systems. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 1–116. Oxford Science Publications (1992)
Luo, Z., Pollack, R.: LEGO proof development system: User’s manual. In: Nerode, A., Taitslin, M.A. (eds.) LFCS 1992. LNCS, vol. 620. Springer, Heidelberg (1992)
Nederpelt, R.: Strong normalisation in a typed lambda calculus with lambda structured types. PhD thesis, Technical University of Eindhoven (1973)
Salvesen, A.: The Church-Rosser property for βη-reduction. Manuscript (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barthe, G. (1999). Existence and Uniqueness of Normal Forms in Pure Type Systems with βη-conversion. In: Gottlob, G., Grandjean, E., Seyr, K. (eds) Computer Science Logic. CSL 1998. Lecture Notes in Computer Science, vol 1584. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10703163_17
Download citation
DOI: https://doi.org/10.1007/10703163_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65922-8
Online ISBN: 978-3-540-48855-2
eBook Packages: Springer Book Archive