# PAL+: a lambda-free logical framework

Zhaohui Luo 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.