+ 
+ @@ -21,73 +25,41 @@ University of Bologna.
++
- -
-
-
- 
-
-
- Matita is based on the
- Calculus of (Co)Inductive Constructions, and is compatible, at some
- extent, with Coq.
- 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; (XML-encoded) proof objects
- are produced for storage and exchange.
+
An interactive prover is a software tool aiding the development of + formal proofs by man-machine collaboration. It provides a formal language + where mathematical definitions, executable algorithms and theorems cohexist, + and an interactive environment keeping the current status of the proof, + and updating it according to commands (usually called tactics) issued by the user.
- -
-
-
- 
-
-
- 
-
-
- The graphical interface has been inspired by CtCoq and
- Proof General.
- It supports high quality bidimensional rendering of
- proofs and formulae transformed on-the-fly to
- MathML markup
-
-
- 
-
-
- 
-
-
-
-
- The knowledge base can be
- browsed as an hypertext
- (locally or on the World Wide Web) and
- searched by means of
- content-based queries;
+ Matita is based on a Dependent Type System known as the Calculus of Inductive Constructions.
-
-
-
- 
-
-
- The tactical language, part of the proof language, has
- step-by-step semantics, enabling inspection and replaying of deeply
- structured proof scripts.
It embeds key computational constructs of functional programming languages: + functions can be defined by (well-founded) recursion, and are live entities that can be + tested and executed.
+ +At the same time, proofs are an integrated part of the formalism, allowing, via the + Curry Howard + isomorphism, a smooth interplay between + specification, implementation and verification: proofs are objects of the language, and + can be treated as normal data, naturally leading to a programming style + akin to proof-carrying-code, + where chunks of software + come equipped with proofs of (some of) their properties.
+Matita is currently adopted in the European Union "Certified Complexity" Project + CerCo for the formal verification of a + complexity-preserving compiler from a large subset of C to a microcontroller + assembly of the kind traditionally used in embedded systems. +
+ +