Classical Dependent Type Theories

The job of a mathematician is to prove theorems - that is, to provide a rigorous, logical argument that establishes that a mathematical statement is true. If the proof is correct, then we can be certain that the theorem is true. But how can we be certain that a proof is correct?

Proof assistants are computer programs that help the user to formalise a mathematical proof, and check that the proof is correct.

They are slowly becoming important for research mathematicians. They have also become very important in the computing industries, for software verification and hardware verification: a formal proof that a product has the properties it is supposed to have, checked by a proof assistant, allows a high degree of confidence in the product.

When designing a proof assistant, one must first choose a system of logic. A system of logic consists of a symbolic language in which theorems and proofs may be written, together with a set of rules for deciding which proofs are correct. The systems of logic known as type theories have proven very successful for use in proof assistants.

Given a system of logic, we may ask: which proofs can be formalised in this system? Proofs are divided into "constructive proofs" and "classical proofs". Most computer scientists, and the vast majority of mathematicians, accept classical proofs. But proof assistants based on type theory have, so far, only been able to formalise constructive proofs; and this is quite a large constraint on their usefulness.

Certain objects, called control operators, may be added to a type theory. When these are added to some simple type theories, the theories now accept classical proofs; this is a very surprising fact, and still not well understood. However, when control operators are added in the same way to more complex type theories (dependent type theories), the theories become inconsistent; that is, it is now possible to "prove" statements that are false.

The problem is that there are several different ways in which control operators may be added to a complex type theory; we have several choices as to where we allow a control operator to appear, and how control operators interact with the other features of a type theory. The naive choice - allow them everywhere, and allow all possible forms of interaction - leads to inconsistency. Of the many other possibilities, it is not at all obvious which will be most likely to be fruitful; and investigating their properties one by one would be very time consuming.

Systems of logic known as logic-enriched type theories, or LTTs, have also been developed. These are closely related to type theories. They differ in being divided rigidly into two parts: one part - the type-theoretic component - for defining mathematical objects and programs, and one part - the logical component - for stating and proving theorems about the object. We can change the logical part to make it accept classical proofs, without changing the type-theoretic part.

However, LTTs are still quite new, and their theoretical properties and suitability for use in a proof assistant is not yet well understood.

I believe that work on control operators and work on LTTs can help each other. If we investigate the properties of type theories and classical LTTs, and translations between the two, then we should be able to reuse results and use the insights from one to shed light on the other. In particular, we should find the best way to add control operators to a complex type theory, by choosing the way that makes translation to and from LTTs easiest.

I therefore propose to construct several type theories with control operators and several classical LTTs, investigate their theoretical properties and translations between them, and experiment with their use in practice. My aim is to produce one or more systems of logic that keeps all the advantages of type theories; accepts classical proofs; and is practicable for use in a proof assistan

1. Software and hardware developers, in both the public and private sectors, who use and develop theorem provers for the purposes of software and hardware verification.

As software and hardware become increasingly complex, there is a need for greater certainty that a given piece of software or hardware satisfies its specification and has the properties that it is claimed to have. This is especially true in safety-critical applications. This has led to a lot of interest in both the public and private sectors into the use of proof checkers for software verification and hardware verification.

Type theories have proven extremely successful for these purposes. However, the current restriction of type theory to constructive logic has hampered such efforts; a classical proof of a program's properties is often satisfactory, and the extra effort needed to discover a constructive proof is a disadvantage. A better theoretical understanding of classical type theory would help in the development of such proof checkers.

For example, the US National Security Agency is currently developing a new theorem prover, HOL omega, that is intended to use both dependent types and classical logic, for use in software verification. A better theoretical understanding of how classical logic and dependent types interact would greatly help developers to understand their design space.

As another example, both Microsoft and Google conduct research into type theory and the formalisation of mathematics.

This research would immediately benefit the designers of proof checkers intended for use in software and hardware verification. In turn, the end users would benefit, by being provided with more reliable software and hardware.

2. Developers of dependently typed programming languages

Non-dependently typed functional programming languages such as Haskell and Ruby are becoming increasingly important for software development. There is growing interest from financial institutions in Haskell programming, for example. Dependently typed programming languages are just starting to appear; the systems Coq and Agda, originally designed as proof checkers, are starting to be used as programming languages, and other dependently typed languages such as Cayenne and Epigram have recently been developed.

In such languages, no very satisfactory way has yet been found to handle side effects, such as exceptions and input/output. This could be provided if a consistent way to add control operators to such a language were discovered.

If so, this research would therefore immediately benefit the designers of dependently typed languages. In turn, programmers using such languages would benefit, as it would become easier to write software in such languages. The end users of the software would also benefit, as the software will be better written and more reliable.

3. Mathematics teachers and computer science teachers who wish to teach logic or the notion of mathematical proof.

There have been a few attempts to use proof checkers based on type theory to teach constructive logic to undergraduates. The anecdotal reports from such attempts have been positive. If, as a consequence of this research, a proof checker based on classical type theory were to be developed in the future, it might well prove to be an equally effective tool for teaching classical logic.

Teachers who wish to teach classical logic would therefore benefit by having an effective tool for teaching classical logic. Their students would in turn benefit by learning classical logic more easily.