Matita e' un dimostratore interattivo di teoremi basato su una variante del Calcolo delle Costruzioni CoInduttive. Il software, che e' open source, e' rilasciato ai termini della GNU General Public Licence ed e' pubblicamente accessibile al nostro Subversion repository. Matita e' scritto in OCAML. La dimensione attuale dell'applicazione si aggira sulle 90.000 linee di codice. La versione 0.5.7 implementa e permette di testare qualitativamente e quantitativamente diverse nuove funzionalita' descritte e studiate nei lavori di ricerca degli autori pubblicati nel 2008. In particolare: 1) un innovativo meccanismo di gestione delle coercion che permette di effettuare inferenza di tipi in presenza di ereditarieta' multipla fra strutture matematiche; 2) il supporto per pattern notazionali non lineari, con applicazioni allo sviluppo a livello utente di interfacce didattiche per la rappresentazione di alberi di derivazione anche mal formati; 3) l'implementazione di un nuovo meccanismo di universi algebrici per la stratificazione predicativa di definizioni matematiche;

Matita 0.5.7

ASPERTI, ANDREA;SACERDOTI COEN, CLAUDIO;RICCIOTTI, WILMER;TASSI, ENRICO;ZACCHIROLI, STEFANO
2008

Abstract

Matita e' un dimostratore interattivo di teoremi basato su una variante del Calcolo delle Costruzioni CoInduttive. Il software, che e' open source, e' rilasciato ai termini della GNU General Public Licence ed e' pubblicamente accessibile al nostro Subversion repository. Matita e' scritto in OCAML. La dimensione attuale dell'applicazione si aggira sulle 90.000 linee di codice. La versione 0.5.7 implementa e permette di testare qualitativamente e quantitativamente diverse nuove funzionalita' descritte e studiate nei lavori di ricerca degli autori pubblicati nel 2008. In particolare: 1) un innovativo meccanismo di gestione delle coercion che permette di effettuare inferenza di tipi in presenza di ereditarieta' multipla fra strutture matematiche; 2) il supporto per pattern notazionali non lineari, con applicazioni allo sviluppo a livello utente di interfacce didattiche per la rappresentazione di alberi di derivazione anche mal formati; 3) l'implementazione di un nuovo meccanismo di universi algebrici per la stratificazione predicativa di definizioni matematiche;
2008
A.Asperti; C.Sacerdoti Coen; W. Ricciotti; E.Tassi; S.Zacchiroli
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/68551
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact