Use semantics to show properties of syntax

Thorsten Altenkirch

(University of Nottingham)

To illustrate the idea of using semantics to show syntactical properties I will derive normalisation for minimal propositional logic from completeness of Kripke models. This simple construction motivates the work on categorical normalisation proofs and also shows how to use Type Theory and Categories in Theoretical Computer Science.
The talk is self contained - no previous knowledge of Kripke models or any other of the buzzwords used above is required.
Thursday 22nd February 2001, 14:00
Robert Recorde Room
Department of Computer Science