Research Project

An Open Proof Checker Based on Type Theory

Zhaohui Luo and Randy Pollack
Dept of Computer Science, University of Durham

Funded by EPSRC, grant ref. GR/M75518 (August 1999 - December 2002, 268K)

This project is to develop a new type theory (of dependent types) and a prototype implementation, that are simple and well-understood and that support openness for modification. Our approach has two parts: (1) make the type theory simpler so it can be implemented directly from its formal definition, and (2) build the proof checker on software engineering principles. The new type theory will also address issues not well-handled by present implemented type theories, such as subtyping, modularity of proofs and existential variables.