-

Persone con competenze nell'area
Competenze

Iosif Petrakis: Ricercatore a tempo determinato

Peter Michael Schuster: Professore ordinario

Competenze
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	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.