X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fmatita_it.shtml;h=04b43167c0780a6a1dac8718beb7615ba9a88857;hb=0c7129d74ba0bfbdf7f71ffcf46a8c8c93e7df14;hp=0d77ec373381217682b5c7d11f755409ff52fe7a;hpb=c6ebbcf8350dcf0b8020c9fcea27d7d9336df463;p=helm.git diff --git a/helm/www/matita/matita_it.shtml b/helm/www/matita/matita_it.shtml index 0d77ec373..04b43167c 100644 --- a/helm/www/matita/matita_it.shtml +++ b/helm/www/matita/matita_it.shtml @@ -38,15 +38,15 @@ Matita si fonda su di un Sistema di Tipi Dipendenti noto con il nome di Calcolo delle Costruzioni Induttive.

-

Questo calcolo integra al proprio interno alcuni cosrtutti computazionali tipici dei linguaggi di programmazione funzionali: in particolare, si - possono definire funzioni per ricorsione (ben fondata), la cui - applizazione puo' essere effetivamente calcolata come per normali programmi. +

Questo calcolo integra al proprio interno alcuni costrutti computazionali + tipici dei linguaggi di programmazione funzionali: in particolare, si + possono definire funzioni per ricorsione (ben fondata), che possono essere + valutate e testate come dei normali programmi.

Al tempo stesso, le dimostrazioni sono una parte integrale del formalismo, cosa che permette di ottenere, attraverso l' - isomorfismo di Curry Howard , una efficace integrazione tra specifica e - ragionamento: le prove sono oggetti di prima classe del linguaggio + isomorfismo di Curry Howard , una efficace integrazione tra specifica del comportamento, sua realizzazione implementativa e relativa verifica di correttezza: le prove sono oggetti di prima classe del linguaggio e possono essere trattati come dei normali tipi di dato, inducendo in modo naturale uno stile di programmazione simile al proof-carrying-code, dove frammenti di software sono arricchiti con dimostrazioni di