MONTAGNA | Franco | |
(cognome) | (nome) | (cognome acquisito (facoltativo)) |
30 - SIENA | SCIENZE MATEMATICHE FISICHE e NATURALI |
(Università) | (Facoltà) |
Dip. di Matematica |
2.Titolo del progetto nazionale di ricerca
Logica matematica e applicazioni
3.Responsabile dell'unità operativa
MOGGI | Eugenio | PO - Ordinario o Straordinario |
(cognome) | (nome) | (qualifica) |
29/08/60 | MGGGNE60M29D612T | |
(cognome acquisito (facoltativo)) | (data nascita) | (codice fiscale) |
GENOVA | SCIENZE MATEMATICHE FISICHE e NATURALI |
(Università) | (Facoltà) |
Dip. di Informatica e Scienze dell'Informazione |
010/ 3536629 | 010/ 3536699 | moggi@disi.unige.it |
(telefono) | (Fax) | (E-mail) |
4.Finanziamenti richiesti per l'unità operativa
:
per materiale inventariabile (voce A): | 5.000.000 |
per spese generali (voce B): | 13.000.000 |
Totale complessivo: | 18.000.000 |
Eventuale titolo specifico del progetto di ricerca svolta dall'unità operativa:
5.Settori disciplinari interessati dalla ricerca:
A01A | K05B |
6.Mesi uomo previsti per il responsabile dell'unità operativa: 11
7.Obiettivo del Progetto di Ricerca dell'unità operativa:
a) Rappresentazione uniforme e modulare dei linguaggi di
programmazione, e sue applicazioni allo studio di linguaggi specifici.
b) Teoria della dimostrazione. Ruolo della logica nelle attuali ricerche sui fondamenti della matematica. Teoria della dimostrazione probabilistica.
c) Modelli per teoria sintetica dei domini ed applicazioni a teorie polimorfe forti.
8.Descrizione del Progetto di Ricerca dell'unità operativa
a) Si intende applicare l'approccio monadico e modulare alla semantica
denotazionale, in combinazione con altri strumenti logici e
categoriali, per analizzare linguaggi paradigmatici (p.e. il
pi-calculus) o aspetti finora trascurati dalla semantica denotazionale
(p.e. la complessita').
b) Si intende analizzare i rapporti fra deduzione naturale, calcolo dei sequenti e calcolo delle intercalazioni di Sieg. Inoltre si approfondira' l'analisi di tendenze recenti delle ricerche sui fondamenti della matematica, in particolare delle proposte di Simpson, Sieg et al.
c) I modelli di teoria sintetica dei domini dovrebbero permettere la realizzazione di categorie interne con notevoli proprieta' di completezza per lo studio di modelli di linguaggi sfruttando i risultati in [RR94]. Le proprieta' richieste includono la possibilita' di interpretazione dei sottotipi e dei tipi ricorsivi.
9.Risultati attesi dalla ricerca dell'unità operativa
a) Applicazioni dell' approccio modulare alla semantica per costruire
modelli del pi-calculus e modelli intenzionali per linguaggi
funzionali che catturino l'aspetto complessita'.
b) Confronto fra dimostrazioni formali e informali. Analisi dell'idea di rappresentazione formale canonica di una dimostrazione informale.
c) Costruzione del primo modello categoriale del lambda-calcolo di ordine superiore accoppiato con sottotipi e tipi ricorsivi utilizzando precedenti risultati. Caratterizzazione degli oggetti repleti in topos di Grothendieck e della realizzabilita'.
10. Elenco componenti unità operativa
Moggi; Eugenio; PO; 17-Scienze MFN; Informatica e Scienze dell'Informazione; 11/11
Borga; Marco; PA; 17-Scienze MFN; Matematica; 11/11
Palladino; Dario; PA; 09-Lettere e Filosofia; Filosofia; 5/11
Rosolini; Giuseppe; PA; 17-Scienze MFN; Matematica; 11/11
Bucalo; Anna; BD; Scienze MFN; Matematica; 11/11
Daniela; Archieri; DD; 17-Scienze MFN; Informatica e Scienze dell'Informazione; 11/11
Belle'; Gianna; DD; 17-Scienze MFN; Informatica e Scienze dell'Informazione; 11/11
Gentilini; Paolo; AL; CNR; collaboratore esterno presso IMA di Genova; 5/11
11.Attrezzature necessarie per la realizzazione del progetto di ricerca
disponibili nell'Università:
2 Pentium 100 MHz
1 SUN Sparcstation ELC
1 PC 486
attrezzature che si intende acquistare con i fondi della presente domanda:
1 Pentium 100 MHz, 16 Mb RAM, 1 Gb Hard Disk, Monitor 17"
12. Recenti risultati scientifici ottenuti dai componenti dell'unità operativa
[Mog95] fornisce la semantica categoriale per l' evaluation logic e
propone vari assiomatizzazioni sound e complete per varie classi di
modelli.
[HM95] analizza la categoria dei replete objects (proposta
originariamente da Hyland e Taylor) in un ambito molto piu' generale,
che e' istanziabile per costruire modelli sia di synthetic che di
axiomatic domain theory.
[Mog96] presenta l'approccio monadico ed incrementale alla semantica
denotazionale, facendo vedere come si puo' aggirare le complicazioni
dei modelli matematici mediante l'uso di metalinguaggi e traduzioni.
[Bor95] costituisce un manuale introduttivo alla teoria della dimostrazione, di cui vengono illustrati e confrontati l'accostamento hilbertiano, la deduzione naturale e il calcolo dei sequenti e i teoremi di normalizzazione ottenuti rispettivamente da Gentzen e da Prawitz per il calcolo dei sequenti e per la deduzione naturale. [Bor96] contiene un'analisi dell'empirismo in matematica. Alle critiche empiriste verso i fondamenti della matematica vengono contrapposti risultati recenti, o problemi aperti, relativi alle attuali ricerche sui fondamenti.
[Gen92] e [Gen93] sono alla base di una caraterizzazione sintattica dei legami tra aritmentica di Peano e logica modale. [FGM96] propone un nuovo filone di ricerca "teoria della dimostrazione probabilistica", in cui si cerca di misurare l'informazione contenuta in una struttura sintattica. In tal modo si e' sviluppato una nozione di probabilita' proof-theoretic.
[RR94] risolve il problema di costruire modelli parametrici del polimorfismo. [BR95] produce una nuova presentazione del funtore fascio associato ottenuta sviluppando un caso particolare per la nozione di oggetto repleto di [HM95].
13.Pubblicazioni scientifiche più significative dei componenti dell'unità operativa
Data | Firma | |||
________________ | ________________ |