[Prev][Next][Index][Thread]
A Typed Operational Semantics for Type Theory
I would like to announce that my thesis, entitled ``A Typed
Operational Semantics for Type Theory,'' is available
electronically and will be available soon as an LFCS report.
The addresses for accessing it are enclosed at the end of
this message.
Healfdene Goguen
-------------------------------------------------------------
A Typed Operational Semantics for Type Theory
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-Lof'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 thesis is available by anonymous ftp at
ftp.dcs.ed.ac.uk
in the directory
pub/lfcsreps/94/ECS-LFCS-94-304
as either ECS-LFCS-94-304.ps or ECS-LFCS-94-304.dvi.
Alternatively, it is available by WWW at
http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/94/ECS-LFCS-94-304/index.html
Paper copies will be available from the following address by
requesting report ECS-LFCS-94-304, although the price has not
yet been determined:
Laboratory for Foundations of Computer Science
University of Edinburgh
The King's Buildings
Edinburgh, EH9 3JZ
United Kingdom