helm/www/matita/matita_it.shtml

   1 <!-- $Id: matita.shtml 6610 2006-07-14 12:06:30Z zacchiro $ -->
   2 <!--#include virtual="xhtml-header.shtml" -->
   3 <html>
   4   <head>
   5     <meta name="keywords" content="Matita, prover, assistant" />
   6     <title>Matita - Home Page Italiana</title>
   7     <!--#include virtual="xhtml-meta.shtml" -->
   8   </head>
   9   <body>
  10     <!--#include virtual="menubar_it.shtml" -->
  11     <!--#include virtual="news_it.shtml" -->
  12     <div class="main">
  13
  14       <div class="topimage">
  15         <img src="images/matita-text-big.png" alt="Matita" />
  16         <a href="matita.shtml">
  17           <img src="flags/wgb.gif" alt="english flag" />
  18         </a>
  19       </div>
  20
  21       <p class="spaced">
  22       Matita e' un tool sperimentale di supporto alla dimostrazione
  23       interattiva di teoremi, in via di sviluppo al
  24       <a href="http://www.cs.unibo.it">Dipartimento di Scienze
  25       dell'Informazione</a> della
  26       <a href="http://www.unibo.it">Universita' degli Studi di Bologna</a>.
  27       </p>
  28
  29       <p>Un dimostratore interattivo e' uno strumento software di
  30      ausilio alla dimostrazione formale di teoremi attraverso
  31      la collaborazione tra l'uomo e la macchina. Fornisce un liguaggio
  32      formale in cui coesistono definizioni matematiche, algoritmi eseguibili,
  33      teoremi e relative dimostrazioni, ed un ambiente interattivo che tiene
  34      traccia dello stato corrente delle prove, e le aggiorna in funzione dei
  35      comandi (tattiche) impartiti dall'utente. </p>
  36
  37       <p>
  38       Matita si fonda su di un Sistema di <a href="http://en.wikipedia.org/wiki/Dependent_type">Tipi Dipendenti</a> noto con il nome di Calcolo delle
  39       Costruzioni Induttive.</p>
  40
  41       <p>Questo calcolo integra al proprio interno alcuni costrutti computazionali
  42      tipici dei linguaggi di programmazione funzionali: in particolare, si
  43      possono definire funzioni per ricorsione (ben fondata), che possono essere
  44      valutate e testate come dei normali programmi.
  45      </p>
  46
  47       <p>Al tempo stesso, le dimostrazioni sono una parte integrale del
  48       formalismo, cosa che permette di ottenere, attraverso l'
  49       <a href="http://en.wikipedia.org/wiki/Curry-Howard_correspondence">isomorfismo di Curry Howard </a>, una efficace integrazione tra specifica del comportamento, sua realizzazione implementativa e relativa verifica di correttezza: le prove sono oggetti di prima classe del linguaggio
  50       e possono essere trattati come dei normali tipi di dato, inducendo
  51       in modo naturale uno stile di programmazione simile al
  52       <a href="http://en.wikipedia.org/wiki/Proof-carrying_code">proof-carrying-code</a>, dove frammenti di software sono arricchiti con dimostrazioni di
  53       alcune delle loro proprieta'.</p>
  54
  55       <p>Matita e' attualmente adottato nel Progetto Europeo <a href="http://cerco.cs.unibo.it/">CerCo</a> (Certified Complexity)  per la verifica formale
  56       della preservazione della complessita' durante la fase di compilazione
  57       da linguaggio C verso un linguaggio assembly tipico di microprocessori
  58       per sistemi embedded.</p>
  59
  60       <!--#include virtual="bottombar.shtml" -->
  61
  62     </div>
  63   </body>
  64 </html>