[an error occurred while processing this directive] An error occured whilst processing this directive

LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
4pm, Tuesday 21st October 1997

Typed Operational Semantics Revisited

In my thesis [1], I introduced typed operational semantics, a new approach to studying metatheory for type theory. Typed operational semantics presents type theory from an operational rather than declarative perspective, leading to simpler proofs of properties about reduction and typing such as Church-Rosser, Strong Normalization and Subject Reduction. The technique is especially fruitful when studying systems with dependent types and eta-equality.

I and other people have continued to think about this technique, which has led to clarifications and simplifications of the original idea. In this talk I shall build up a modular development of the concepts involved in typed operational semantics, including:

A simple characterization of the strongly normalizing terms using weak-head normal forms.
Extending this to Church-Rosser and normal forms.
Adding type information for simple types.
Adding type information for dependent types.

The latter two points will also involve discussion of soundness and completeness of the usual typing systems, and a novel treatment of structural properties such as substitution.

[1] H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, Aug. 1994. LFCS Report ECS-LFCS-94-304.

Healfdene Goguen

Last modified: Thu Oct 9 17:35:25 BST 1997 An error occured whilst processing this directive