The applications that currently engage us are in four fields: Formal Methods; Secure Software Systems; Education; and Problem Solving Environments for science and engineering. We distinguish these applications from purely experimental work that engages us when we evaluate the theorem prover or the type theory. This experimental work is particularly relevant in Artificial Intelligence (AI), especially in Cognitive Studies.
Leibniz dreamed of applying a symbolic calculus to the solution of practical problems, and the Greeks even devised machines to help with geometric argument, but the sustained use of computers to aid in practical reasoning is a very new subject. The main applications have been in checking and verifying computer software and computer hardware, and in computer aids for education.
The key to successful applications has been the choice of problems to match the available technology. Like Leibniz, we can imagine a plethora of useful applications to accounting, commerce, education, engineering, entertainment, science and so forth; but only some of these applications are tractable with existing tools. Selecting the right targets is the most important strategic decision. There have been several excellent choices, and the results from these have sustained interest in the field.
The most successful applications are those that can be integrated into tools that are already widely used. (Some mistakenly characterize these as the fully automatic uses of the technology, but that misses a key point.) For example, Milner's polymorphic type checker, a small automatic theorem prover, extends the type checkers of mainstream programming languages. Likewise the work at DEC on extended static type checking incorporates theorem proving technology into compilers. The model checkers pioneered by Edmund Clarke on hardware and finite state protocols are incorporated into CAD tools. The verifications in Ensemble done by Nuprl are part of the Ensemble code optimizer. The theorem provers and verifiers used in proof carrying code are part of the security system for mobile code.
In the area of Problem Solving Environments, the biggest opportunities have been in integrating theorem provers with computer algebra systems. We have been able to provide a semantic foundation for the domain and type structure of systems like Axiom and the local system, Weyl.
Technical ContributionsThe Ensemble work is described under Projects. The idea can be seen from a key paper [PS, PDF] by Kreitz, Hayden and Hickey.
The Bell Labs work is described in articles by Howe and Felty that can be found at their home pages.