Soundness of the logical framework for its typed operational semantics

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.