X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fmatita.shtml;h=5da934cdc8aa6661c76a4af35997b6fd49401713;hb=d2545ffd201b1aa49887313791386add78fa8603;hp=a68b488302a0d40c85534cfa594e9798211f0722;hpb=0692f9fb99211c02a93c72d58c9177f9f994e4d9;p=helm.git

diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index a68b48830..5da934cdc 100644
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -11,6 +11,13 @@
     <!--#include virtual="news.shtml" -->
     <div class="main">
 
+      <div class="topimage">
+	<img src="images/matita-text-big.png" alt="Matita" />
+	<a href="matita_it.shtml">
+         <img src="flags/wit.gif" alt="italian flag" />
+        </a>
+      </div>
+
       <p class="spaced">
       Matita (that means <em>pencil</em> in italian) is an experimental, 
 	interactive theorem prover under development at the 
@@ -18,8 +25,40 @@
       <a href="http://www.unibo.it">University of Bologna</a>.
       </p>
 
+      <p>
+      </p>
 <!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
+      
+      <p>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.
+      </p>
+
+      <p>
+      Matita is based on a <a href="http://en.wikipedia.org/wiki/Dependent_type">Dependent Type System</a> known as the Calculus of Inductive Constructions.</p>
 
+      <p>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.</p>
+
+      <p>At the same time, proofs are an integrated part of the formalism, allowing, via the 
+      <a href="http://en.wikipedia.org/wiki/Curry-Howard_correspondence">Curry Howard 
+      isomorphism</a>, 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 <a href="http://en.wikipedia.org/wiki/Proof-carrying_code">proof-carrying-code</a>, 
+      where chunks of software 
+      come equipped with proofs of (some of) their properties.</p>
+
+      <p>Matita is currently adopted in the European Union "Certified Complexity" Project
+      <a href="http://cerco.cs.unibo.it/">CerCo</a> 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.
+      </p>
+      
+      <!--#include virtual="bottombar.shtml" -->
 
     </div>
   </body>