Personal tools
You are here: Home Events Abstract Archives 1997 Typed Operational Semantics Revisited

Typed Operational Semantics Revisited

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

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.

Document Actions