Matita


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 Inductive Constructions, and is compatible, to some extent, with Coq.
The word "matita" means "pencil" in Italian. It is a reasonably small and simple application, whose architectural and software complexity is meant to be mastered by students, providing a tool particularly suited for testing innovative ideas and solutions. Matita adopts a tactic-based editing mode; proof objects are produced for storage and exchange.

Main features

Existential variables are native in Matita, allowing a simpler management of dependent goals.
Matita implements a bidirectional type inference algorithm exploiting both inferred and expected types.
The power of the type inference system is further augmented by a mechanism of
hints
that helps in synthetizing unifiers in particular situations specified by the user.
Matita supports a sophisticated disambiguation strategy
based on a dialog between the parser and the typechecker.
At the interactive level, the system implements a small step execution of structured tactics
allowing a much better management of the proof development, and naturally leading
to more structured and readable scripts.

Applications

Matita has been employed in : a
European Project
focused on the development of a formally verified, complexity preserving compiler from a large subset of C to the assembler of a MCS-51 microprocessor.

Documentation

The Matita tutorial provides a pragmatic introduction to the main functionalities of the Matita interactive theorem prover, offering a guided tour through a set of not trivial examples in the field of software specification and verification.