print · source · login   

Tools

Type theory based tools for programming and verification

Coq (in three short paragraphs)

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

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

Twelf

NuPRL

Agda

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.

Idris

Lean

Andromeda

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.