## A Typed Operational Semantics for Type Theory

**Healfdene Goguen**
*Abstract:* Untyped reduction provides a natural
operational semantics for type theory. Normalization results say
that such a semantics is sound. However, this reduction does not
take type information into account and gives no information about
canonical forms for terms. We introduce a new operational
semantics, which we call typed operational semantics, which defines
a reduction to normal form for terms which are well-typed in the
type theory.

The central result of the thesis is soundness of the typed
operational semantics for the original system. Completeness of the
semantics is straightforward. We demonstrate that this equivalence
between the declarative and operational presentations of type
theory has important metatheoretic consequences: results such as
strengthening, subject reduction and strong normalization follow by
straightforward induction on derivations in the new system.

We introduce these ideas in the setting of the simply typed
lambda calculus. We then extend the techniques to Luo's system UTT,
which is Martin-Löf's Logical Framework extended by a general
mechanism for inductive types, a predicative universe and an
impredicative universe of propositions. We also give a
proof-irrelevant set-theoretic semantics for UTT.

*This report is a 220-page PhD thesis. It is available in
DVI (683Kb) and Postscript (1.2Mb) format.*

Previous |

Index |

Next