helm/www/matita/matita.shtml

   1 <!--#include virtual="xhtml-header.shtml" -->
   2 <!-- $Id$ -->
   3 <html xmlns="http://www.w3.org/1999/xhtml">
   4   <head>
   5     <meta name="keywords" content="Matita, prover, assistant" />
   6     <title>Matita - Home Page</title>
   7     <!--#include virtual="xhtml-meta.shtml" -->
   8   </head>
   9   <body>
  10     <!--#include virtual="menubar.shtml" -->
  11     <!--#include virtual="news.shtml" -->
  12     <div class="main">
  13
  14       <div class="topimage">
  15         <img src="images/matita-text-big.png" alt="Matita" />
  16         <a href="matita_it.shtml">
  17          <img src="flags/wit.gif" alt="italian flag" />
  18         </a>
  19       </div>
  20
  21       <p class="spaced">
  22       Matita (that means <em>pencil</em> in italian) is an experimental,
  23         interactive theorem prover under development at the
  24       <a href="http://www.cs.unibo.it">Computer Science Department</a> of the
  25       <a href="http://www.unibo.it">University of Bologna</a>.
  26       </p>
  27
  28 <!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
  29
  30       <p class="spaced">
  31       <span class="screenshots">
  32         <a class="quiet" href="images/screenshot-matita.png">
  33           <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
  34         </a>
  35       </span>
  36
  37       <p>An interactive prover is a software tool aiding the development of
  38       formal proofs by man-machine collaboration. It provides a formal language
  39       where mathematical definitions, executable algorithms and theorems cohexist,
  40       and an interactive environment keeping the current status of the proof,
  41       and updating it according to commands (usually called tactics) issued by the user.
  42       </p>
  43
  44       <p>
  45       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>
  46
  47       <p>It embeds key computational constructs of functional programming languages:
  48       functions can be defined by (well-founded) recursion, and are live entities that can be
  49       tested and executed.</p>
  50
  51       <p>At the same time, proofs are an integrated part of the formalism, allowing, via the
  52       <a href="http://en.wikipedia.org/wiki/Curry-Howard_correspondence">Curry Howard
  53       isomorphism</a>, a smooth interplay between
  54       specification and reasoning: proofs are objects of the language, and
  55       can be treated as normal data, naturally leading to a programming style
  56       akin to <a href="http://en.wikipedia.org/wiki/Proof-carrying_code">proof-carrying-code</a>,
  57       where chunks of software
  58       come equipped with proofs of (some of) their properties.</p>
  59
  60       <p>Matita is currently adopted in the European Union "Certified Complexity" Project
  61       <a href="http://cerco.cs.unibo.it/">CerCo<a> for the formal verification of a
  62       complexity-preserving compiler from a large subset of C to a microcontroller
  63       assembly of the kind traditionally used in embedded systems.
  64       </p>
  65
  66
  67     </div>
  68   </body>
  69 </html>