Research Project
Type-theoretic foundation of mathematical pluralism
Zhaohui Luo
Dept of Computer Science,
Royal Holloway, Univ of London
Funded by Leverhulme Trust, Grant ref: F/07 537/AA (Nov 2006 -- Oct 2009).
Dependent type theory, or type theory for short,
provides a solid foundation of mathematics and
a powerful calculus for reasoning.
Proof development systems based on type theories (so-called proof assistants)
have been used successfully in formalisation of
mathematics and reasoning about programs.
The current type theories as found in various proof assistants are all
based on intuitionistic systems and only adequate for formalisation of
constructive mathematics.
The type theory based theorem proving technology is not (and should not be)
limited to applications to such special branches of mathematics.
It should have wider applications in formalisation of other kinds of
mathematics, including the ordinary classical mathematics and the classical
predicative mathematics. What is missing is a uniform type-theoretic
foundation so that the theorem provers based on type theory can be applied --
this is the research topic of this project.