| Argomento | Persone | Descrizione |
|---|---|---|
| Il programma di Hilbert per la matematica astratta |
Peter Michael Schuster
|
Estrarre il contenuto computazionale dalle dimostrazioni classiche nella matematica concettuale. Sotto particolare considerazione sono le istanze matematiche della completezza logica che tipicamente appaiono come varianti del lemma di Zorn. |
| Teoria dei tipi e teoria delle categorie |
Iosif Petrakis
|
La teoria dei tipi di Martin Loef è una struttura fondamentale sia per la programmazione funzionale che per la matematica costruttiva. La sua recente estensione, la teoria dei tipi di omotopia, ha rivelato nuove e inaspettate connessioni tra la topologia algebrica e l'informatica teorica. Alcuni modelli categoriali di tipi dipendenti generano la cosiddetta teoria delle categorie dipendenti e la sua duale, la teoria delle categorie codipendenti. |
| Teoria della dimostrazione e matematica costruttiva |
Andrea Masini
Iosif Petrakis Peter Michael Schuster |
La teoria della dimostrazione si occupa delle dimostrazione matematiche, che in tal modo diventano oggetti della matematica. L'obiettivo è capire “cosa si può dimostrare con cosa” e ottenere informazione computazionale dalle dimostrazioni. La matematica costruttiva mira a dimostrazioni dirette da cui si possono estrarre algoritmi; ogni tale algoritmo viene fuori con un certificato di correttezza gratuito, che è la dimostrazione originale. |
© 2025 | Verona University
******** CSS e script comuni siti DOL - frase 9957 ********
