Department of Computer Science
University of Durham
4pm Tuesday 8 April 2003
Room 2511, JCMB, King's Buildings
Logical frameworks such as that developed by Per Martin-Lof may be viewed as foundations for type theory and the associated proof systems. I shall give a (non-technical) introduction to PAL+, a lambda-free logical framework, and explain that it is an adequate calculus for specifying type theories and a useful foundation for designing proof development systems based on type theory. An implementation of a generic proof system based on PAL+ is in progress.
The talk will begin with an introduction to dependent type theory and its applications.