Tools

Type theory based tools for programming and verification

Proof management systems

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

• 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

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.

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.

Dedukti

Dedukti is a logical framework based on the λΠ-calculus modulo in which many theories and logics can be expressed. For instance, it provides means to define theories such as Predicate logic, Simple type theory, the Calculus of constructions, the Calculus of Inductive Constructions... and to express proofs in these theories.

Logipedia is a library of proofs expressed in Dedukti.

Programming languages

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

Idris is a general purpose pure functional programming language with dependent types. Dependent types make it possible to express aspects of a program’s behaviour precisely in the type, which describes expected additional properties of the inputs and more precise guarantees for outputs. It is compiled, with eager evaluation and its features are influenced by Haskell and ML.

It is interesting that

• The name Idris is derived from a name of a dragon that appears in an animated series Ivor the Engine (here, at the end of the 3rd minute).
• Idris is a PacMan-complete language, that means a language in which one can develop the PacMan game.
• It compiles to C and JavaScript (both browser- and Node.js-based). There are also a number of unofficial code generators for other platforms, such as Java, JVM, CIL, OCaml, and a partial LLVM backend.

HaHa

HaHa is a small software verification integrated development environment (IDE) that makes it possible to verify small programs in a simple while-language. As the backend it uses Z3, CVC4 and Coq as proving engines. It is also possible to compile HaHa procedures to Unix object files to be linked with C code.

Iris

Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed in a wide variety of verification projects. These projects include but are not limited to: verification of fine-grained concurrent data structures, logical-relations for relational reasoning, program logics for relaxed memory models, program logics for object capabilities, and a safety proof for a realistic subset of the Rust programming language. The Iris framework is language independent and comes with the MoSeL proofmode, which offers a rich set of tactics for making separation-logic proofs look and feel like ordinary Coq proofs.