Matita is a programming language created in 1999.

#2913on PLDB | 25Years Old |

Matita is an experimental proof assistant under development at the Computer Science Department of the University of Bologna. It is a tool aiding the development of formal proofs by man-machine collaboration, providing a programming environment where formal specifications, executable algorithms and automatically verifiable correctness certificates naturally coexist. Matita is based on a dependent type System known as the Calculus of (Co)Inductive Constructions (a derivative of Calculus of Constructions), and is compatible, to some extent, with Coq. Read more on Wikipedia...

- Tags: programming language
- Early development of Matita happened in University of Bologna