-<!-- $Id$ -->
<!--#include virtual="xhtml-header.shtml" -->
-<html>
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta name="keywords" content="Matita, prover, assistant" />
<title>Matita - Home Page</title>
<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 class="spaced">
- <span class="screenshots">
- <a class="quiet" href="images/screenshot-matita.png">
- <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
- </a>
- </span>
- Matita is based on the
- Calculus of (Co)Inductive Constructions, and is compatible, at some
- extent, with <a href="http://coq.inria.fr">Coq</a>.
- 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.
+ <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 class="spaced">
- <span class="screenshots">
- <a class="quiet" href="images/screenshot-matita-href.png">
- <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
- </a>
- <a class="quiet" href="images/screenshot-matita-selection.png">
- <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
- </a>
- </span>
- The graphical interface has been inspired by CtCoq and
- <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
- It supports high quality bidimensional rendering of
- proofs and formulae transformed on-the-fly to
- <a href="http://www.w3.org/Math/">MathML</a> markup</p>
- <p class="spaced">
- <span class="screenshots">
- <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
- <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
- </a>
- <a class="quiet" href="images/screenshot-cicbrowser-query.png">
- <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
- </a>
- <!--
- <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
- <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
- </a>
- -->
- </span>
-
- The <a href="library.shtml">knowledge base</a> can be
- <a href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
- (locally or on the World Wide Web) and
- <a href="http://helm.cs.unibo.it/whelp/"> searched by means of
- content-based queries</a>; </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 class="spaced">
- <span class="screenshots">
- <a class="quiet" href="images/screenshot-tinycals.png">
- <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
- </a>
- </span>
- The tactical language, part of the proof language, has
- step-by-step semantics, enabling inspection and replaying of deeply
- structured proof scripts. </p>
-
- <p>Matita is partially supported by the following Projects:
- <ul>
- <li><a href=http://www.cs.chalmers.se/Cs/Research/Logic/Types/>
- Types Project</a>
- <li><a href=http://www.mctafi.math.unipd.it/>McTafi</a></li>
- </ul>
- </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>
</html>
projects / helm.git / blobdiff