X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Fmatita%2Fmatita.shtml;h=5da934cdc8aa6661c76a4af35997b6fd49401713;hb=045c74915022181e288d9a950cc485437b08d002;hp=2bf6a2119984b97d5ed56ecf36d25fe60edae50a;hpb=727fa1f56c2e47203da5d232ad48b2fe02e63282;p=helm.git diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml index 2bf6a2119..5da934cdc 100644 --- a/helm/www/matita/matita.shtml +++ b/helm/www/matita/matita.shtml @@ -1,68 +1,65 @@ - -
-+ Matita (that means pencil in italian) is an experimental, + interactive theorem prover under development at the + Computer Science Department of the + University of Bologna. +
- ++
+ + +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. +
+ ++ Matita is based on a Dependent Type System known as the Calculus of Inductive Constructions.
-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. +
+ + + +