Personal tools
You are here: Home Events Abstract Archives 2000 Soundness of the Logical Framework for its Typed Operational Semantics

Soundness of the Logical Framework for its Typed Operational Semantics

Healfdene Goguen AT+T 2:30pm Thursday 23 March 2000 Room 2511, JCMB, King's Buildings

Typed operational semantics 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 for the simply-typed lambda-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 beta-eta-reduction for the Logical Framework. Along the way, we also give a cleaner presentation of typed operational semantics than has appeared elsewhere.

Document Actions