matita.cs.unibo.it Git - helm.git/blob - helm/www/matita/matita.shtml

1

2

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

8 </head>

9 <body>

10

11

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 <p>

29 </p>

30

31

32 <p>An interactive prover is a software tool aiding the development of

33 formal proofs by man-machine collaboration. It provides a formal language

34 where mathematical definitions, executable algorithms and theorems cohexist,

35 and an interactive environment keeping the current status of the proof,

36 and updating it according to commands (usually called tactics) issued by the user.

37 </p>

38

39 <p>

40 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>

41

42 <p>It embeds key computational constructs of functional programming languages:

43 functions can be defined by (well-founded) recursion, and are live entities that can be

44 tested and executed.</p>

45

46 <p>At the same time, proofs are an integrated part of the formalism, allowing, via the

47 <a href="http://en.wikipedia.org/wiki/Curry-Howard_correspondence">Curry Howard

48 isomorphism</a>, a smooth interplay between

49 specification, implementation and verification: proofs are objects of the language, and

50 can be treated as normal data, naturally leading to a programming style

51 akin to <a href="http://en.wikipedia.org/wiki/Proof-carrying_code">proof-carrying-code</a>,

52 where chunks of software

53 come equipped with proofs of (some of) their properties.</p>

54

55 <p>Matita is currently adopted in the European Union "Certified Complexity" Project

56 <a href="http://cerco.cs.unibo.it/">CerCo</a> for the formal verification of a

57 complexity-preserving compiler from a large subset of C to a microcontroller

58 assembly of the kind traditionally used in embedded systems.

59 </p>

60

61

62

63 </div>

64 </body>

65 </html>