The metatheory of UTT

Abstract

This paper outlines the development of the metatheory for Luo's type theory UTT, the type theory implemented in the proof assistant LEao and containing as subsystems Martin-LSf's type theory and the Calculus of Constructions. The approach used is to define a typed operational semantics for the system and to establish the important metatheoretic properties, such as Church-Rosser, strong normalization and subject reduction, for this operational presentation of the theory. These properties are then transferred to the usual presentation by soundness and completeness results. This technique gives a new and simpler development of the metatheory for systems with dependent types and n-equality.