Type theory and its applications

Zhaohui Luo

(Royal Holloway, University of London)

Dependent type theory provides a powerful logical calculus for formalisation of mathematics and verification of programs. I shall present two applications of type theory based proof assistants, one on the formalisation of Weyl's predicative mathematics and the other on the modelling and verification of object-oriented programs.
Thursday 13th March 2008, 14:00
Robert Recorde Room
Department of Computer Science