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

1. [ABB95] F. Alessi, P. Baldan and G. Belle'. A fixed-point theorem in a category of compact metric spaces. Theoretical Computer Science, 146 (1995) 311-320.
2. [Bor95] M. Borga. Fondamenti di logica: introduzione alla teoria della dimostrazione. Angeli, Milano, 1995.
3. [Bor96] M. Borga. From certainty to fallibility in mathematics?. In E. Agazzi e G. Darvas (eds.), Philosophy of mathematics today, Kluwer, Dordrecht, 1996 (to appear).
4. [BR96] A. Bucalo and G. Rosolini. Repleteness and the associated sheaf, 1995. submitted for publication.
5. [FMRS92] P.J. Freyd, P. Mulry, G. Rosolini, and D.S. Scott. Extensional pers. Inform. and Comput., 98:211--227, 1992.
6. [HM95] J.M.E. Hyland and E. Moggi. The S-replete construction. In CTCS 1995, volume 953 of LNCS. Springer Verlag, 1995.
7. [Gen92] P. Gentilini. Provability logic in Gentzen formulation of arithmetic. Zeitschrift fur mathematische logik und grundlagen der mathematik, 38, 1992, pp. 535-550.
8. [Gen93] P. Gentilini. Syntactical results on the arithmetical completeness of modal logic. Studia Logica, 4, 1993, pp. 549-564.
9. [FGM96] P. Forcheri, P. Gentilini, M.T. Molfino, Research in automated deduction as a basis for a probabilistic proof-theory. In Logic and Algebra (eds. P. Agliano, A. Ursini), Dekker, 1996, pp. 491-528.
10. [Mog95] E. Moggi. A semantics for evaluation logic. Fundamenta Informaticae, 22(1/2), 1995.
11. [Mog96] E. Moggi. Metalanguages and applications. In Semantics and Logics of Computation (eds. P. Dybjer, A. Pitts), CUP, 1996 (to appear).
12. [Pal93] D. Palladino. Le logiche non monotone: caratteristiche e prospettive. Epistemologia 16 (1993), Fascicolo Speciale "Linguaggi e macchine", pp. 241-266.
13. [RR94] E.P. Robinson and G. Rosolini. Reflexive graphs and parametric polymorphism. In 9th LICS Conference. IEEE, 1994, pp 364-371.