Abstract
Typed operational semantics [4],[5] is a technique for describing the operational behavior of the terms of type theory. The combination of operational information and types provides a strong induction principle that allows an elegant and uniform treatment of the metatheory of type theory. In this paper, we adapt the new proof of strong normalization by Joachimski and Matthes [6] for the simply-typed λ-calculus to prove soundness of the Logical Framework for its typed operational semantics. This allows an elegant treatment of strong normalization, Church-Rosser, and subject reduction for βη-reduction for the Logical Framework. Along the way, we also give a cleaner presentation of typed operational semantics than has appeared elsewhere.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
H. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbai, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1991.
A. Compagnoni and H. Goguen. Typed operational semantics for higher order subtyping. Technical Report ECS-LFCS-97-361, Edinburgh Univ., July 1997. Submitted to Information and Computation.
H. Geuvers. Logics and Type Systems. PhD thesis, Katholieke Universiteit Nijmegen, Sept. 1993.
H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, Edinburgh Univ., Aug. 1994.
H. Goguen. Typed operational semantics. In Proceedings of TLCA, volume 902 of Lecture Notes in Computer Science, pages 186–200. Springer-Verlag, Apr. 1995.
F. Joachimski and R. Matthes. Short proofs of strong normalization, 1998. Draft, submitted for publication.
A. Jones, Z. Luo, and S. Soloviev. Some algorithmic and proof-theoretical aspects of coercive subtyping. In Proceedings of TYPES’96, 1996. To appear.
P. Leleu. Metatheoretic results for a modal lambda calculus. Technical Report RR-3361, INRIA, 1998.
R. Loader. Normalisation by translation. Note distributed on TYPES list, Apr. 1995. 177
Z. Luo. An Extended Calculus of Constructions. PhD thesis, Edinburgh Univ., Nov. 1990.
Z. Luo. Computation and Reasoning. Oxford University Press, 1994.
J. McKinna and R. Pollack. Pure type systems formalized. In M. Bezem and J. F. Groote, editors, Proceedings of TLCA, pages 289–305. Springer-Verlag, LNCS 664, Mar. 1993.
B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press, 1990.
G. Pottinger. Strong normalization for the terms of the theory of constructions. Technical Report TR 11-7, Odyssey Research Associates, Inc., 1987.
A. Salvesen. The Church-Rosser property for pure type systems with βη-reduction, Nov. 1991. Unpublished manuscript.
M. Takahashi. Parallel reductions in λ-calculus. Information and Computation, 118:120–127, 1995.
L. van Benthem Jutting, J. McKinna, and R. Pollack. Typechecking in pure type systems. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programming. Springer-Verlag, 1993.
F. van Raamsdonk and P. Severi. On normalisation. Technical Report CS-R9545, CWI Amsterdam, 1995.
B. Werner. Une Théorie des Constructions Inductives. PhD thesis, Université Paris 7, 1994.
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
Goguen, H. (1999). Soundness of the Logical Framework for Its Typed Operational Semantic. In: Girard, JY. (eds) Typed Lambda Calculi and Applications. TLCA 1999. Lecture Notes in Computer Science, vol 1581. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48959-2_14
Download citation
DOI: https://doi.org/10.1007/3-540-48959-2_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65763-7
Online ISBN: 978-3-540-48959-7
eBook Packages: Springer Book Archive