Type theory based tools for programming and verification

Coq is a proof management system in which one can describe items subject to study (e.g. numbers, computer programs etc.), state their properties, and prove them. It makes it possible to do do various proof management activities to facilitate the proof creation process. The tool was used to successfully

- To develop a verfied compiler
*CompCert*for a considerably big fragment of C programming language. - To develop a proof of the Feit-Thompson theorem.
- To develop a constructive library for real mathematics, including Fundametal Theorem of Algebra, Fundamental Theorem of Calculus etc.

It is interesting that

- There was still some shadow of doubt that Four color theorem is proved after the argument of Kenneth Appel and Wolfgang Haken. This was dispelled by the proof of the theorem done by Georges Gonthier and Benjamin Werner.
- You can use a JavaScript interpreter written in Coq!

Maybe it is not so obvious that Coq was used in the following projects.

- Tools such as Why, Krakatoa, Frama-C make it possible to prove annotated programs written in other languages (e.g. C, Java).
- Gemalto used Coq to achieve EAL7 certification for their Java Card platform.
- One can try Coq on-line here.

For more projects that use Coq you can look to this page and also to that one.

Matita is an experimental, interactive theorem prover under development at the Computer Science Department of the University of Bologna.

It is interesting that

- Matita means pencil in Italian.
- Matita has a kernel with a remarkably compact implementation of around 2300 lines of OCaml code.
- Matita is used for the formal verification of a complexity-preserving compiler from a large subset of C to a microcontroller assembly used in embedded systems.

Maybe it is not so obvious that Matita was used in the following projects.

- The Lebesgue’s dominated convergence theorem is proved using Matita.
- Executable models of microprocessors for the Freescale (formerly Motorola) 8-bit family are written in Matita. The formalization captures not only the functional behaviour of the processors, but also computes their exact execution times.

Agda is a dependently-typed programming language and proof assistant based on Martin-Löf Type Theory. The syntax is inspired by Haskell, and it comes with a powerful totality checker to ensure coverage and termination. Sized types and copattern matching make Agda the tool of choice for programming and reasoning with coinductive structures.

Agda features instance arguments which are similar to Scala's implicits and generalize Haskell's type classes. Agda's parametrized modules allow for structured programming at the large. An Agda's reflective features enable meta-programming and proving by decision procedures.

Currently Agda is very popular to assist researchers in computer science. Around 200 papers have been written with the help of Agda.

Andromeda is an implementation of dependent type theory with equality reflection. The type theory is very expressive, as it allows one to postulate new judgmental equalities. The design of Andromeda follows the tradition of LCF-style theorem provers:

- there is an abstract datatype of judgments,
- all constructions of judgments are done by a trusted
*nucleus*and directly correspond to the inference rules of type theory (or derivations thereof), - the user interacts with the nucleus by writing programs in a high-level, statically
typed meta-language
*Andromeda ML (AML)*.

The nucleus does not perform any normalization (it cannot as the underlying type theory has no normal forms), unification, or perform proof search. These techniques can all be implemented on top of the nucleus in AML, and therefore cannot compute underivable judgments by design. Of course, they could fail or run forever because AML is a general-purpose programming language.

Equality checking is delegated to the meta-level by a mechanism of operations and handlers akin to those of the Eff programming language. Whenever the nucleus needs to check a non-trivial equation, it triggers an operation (question) which propagates to the meta-level. There it is intercepted by a user-defined handler which handles (answers) the equation by providing a witness for it.