X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Fmatita%2Fmatita.shtml;h=5da934cdc8aa6661c76a4af35997b6fd49401713;hb=74c7035b4dd6933bda4479816e51f5771ee1f572;hp=845367ad1efebcd8482bcc3b79ffa24d30232e9f;hpb=4c042b286cd7d2559738569b96769dd0263a9f6d;p=helm.git diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml index 845367ad1..5da934cdc 100644 --- a/helm/www/matita/matita.shtml +++ b/helm/www/matita/matita.shtml @@ -1,6 +1,6 @@ - - + +
+
- -
-
-
-
-
-
- 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.
Matita is partially supported by the following Projects: -
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. +
+ +