<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>
<p>An interactive prover is a software tool aiding the development of
formal proofs by man-machine collaboration. It provides a formal language
<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 and reasoning: proofs are objects of the language, and
+ 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
+ <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>