<!--#include virtual="xhtml-header.shtml" -->
-<html>
- <head>
- <title>Matita home page</title>
- </head>
- <style>
- a {text-decoration:none}
- img.image{ display: none; }
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <meta name="keywords" content="Matita, prover, assistant" />
+ <title>Matita - Home Page</title>
+ <!--#include virtual="xhtml-meta.shtml" -->
+ </head>
+ <body>
+ <!--#include virtual="menubar.shtml" -->
+ <!--#include virtual="news.shtml" -->
+ <div class="main">
- dl#matitaMap {
- margin-left:auto;
- margin-right:auto;
- margin-top:50px;
- padding: 0;
- background: url(matita.png) top left no-repeat;
- height: 590px;
- width: 485px;
- position: relative;
- }
-
- dt{ margin: 0; padding: 0; position: absolute; font-size: 85%; display: none; }
- dd{ margin: 0; padding: 0; position: absolute; font-size: 85%; }
-
- dd#developersDef{ top: 206px; left: 30px; }
- dd#developersDef a{ position: absolute; width: 426px; height: 70px; text-decoration: none; }
- dd#developersDef a span{ display: none; }
- dd#developersDef a:hover{ position: absolute; background: transparent url(bg0.png) ; top: 0px}
-
- dd#documentationDef{ top: 277px; left: 30px; }
- dd#documentationDef a{ position: absolute; width: 426px; height: 70px; text-decoration: none; }
- dd#documentationDef a span{ display: none; }
- dd#documentationDef a:hover{ position: absolute; background: transparent url(bg1.png) ; top: 0px}
-
- dd#communityDef{ top: 348px; left: 30px; }
- dd#communityDef a{ position: absolute; width: 426px; height: 70px; text-decoration: none; }
- dd#communityDef a span{ display: none; }
- dd#communityDef a:hover{ position: absolute; background: transparent url(bg2.png) ; top: 0px}
-
- dd#downloadDef{ top: 419px; left: 30px; }
- dd#downloadDef a{ position: absolute; width: 426px; height: 70px; text-decoration: none; }
- dd#downloadDef a span{ display: none; }
- dd#downloadDef a:hover{ position: absolute; background: transparent url(bg3.png) ; top: 0px}
+ <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>
- div#ex {margin-left:auto; margin-right:auto}
- </style>
+ <p class="spaced">
+ Matita (that means <em>pencil</em> in italian) is an experimental,
+ interactive theorem prover under development at the
+ <a href="http://www.cs.unibo.it">Computer Science Department</a> of the
+ <a href="http://www.unibo.it">University of Bologna</a>.
+ </p>
- <body>
+ <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>
-<div id="ex" >
-<img src="matita.png" width="485" height="590" border="0" class="image" />
+ <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>
- <dl id="matitaMap">
- <dt id="developers">1. Developers</dt>
- <dd id="developersDef"><a href="developers.shtml"></a></dd>
- <dt id="documentation">2. Documentation</dt>
- <dd id="documentationDef"><a href="documentation.shtml"></a></dd>
- <dt id="community">3. Community</dt>
- <dd id="communityDef"><a href="community.shtml"></a></dd>
- <dt id="download">4. Download</dt>
- <dd id="downloadDef"><a href="download.shtml"></a></dd>
- </dl>
- <div>
-
-<!--#include virtual="bottombar.shtml" -->
+ <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>
</html>
-
-<!-- $Id$ -->
projects / helm.git / blobdiff