RONCHI DELLA ROCCA	SIMONETTA
(cognome)	(nome)
Università degli Studi di TORINO	Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI
(università)	(facoltà)
INF/01	Dipartimento di INFORMATICA
(settore scient.discipl.)	(Dipartimento/Istituto)

ronchi@di.unito.it
(E-mail)

ABRUSCI	VITO MICHELE
(cognome)	(nome)

Professore ordinario	16/06/1949	BRSVMC49H16A662R
(qualifica)	(data di nascita)	(codice di identificazione personale)

Università degli Studi ROMA TRE	Facoltà di LETTERE e FILOSOFIA
(università)	(facoltà)
M-FIL/02	Dipartimento di FILOSOFIA
(settore scient.discipl.)	(Dipartimento/Istituto)

06/54577419	06/54577340	abrusci@uniroma3.it
(prefisso e telefono)	(numero fax)	(E-mail)

Testo italiano

Vito Michele Abrusci è professore ordinario di Logica e Filosofia della Scienza (M-FIL/02) presso l'Università Roma Tre dal 1996; è stato straordinario di Logica e Filosofia della Scienza presso l'Università di Bari (1994-1996), associato di Logica Matematica presso l'Università Roma La Sapienza (1991-1994), associato di Filosofia della Scienza presso l'Università di Bari (1988-1991) e ricercatore presso l'Università di Firenze (1981-1988).Dal 1999 è Presidente della Società Italiana di Logica e Filosofia delle Scienze.
Abrusci ha svolto la sua attività di ricerca in particolare nei seguenti campi:
a) Teoria della dimostrazione (teoria dei dilatatori), entro la quale i suoi maggiori risultati hanno riguardato la non-dimostrabilità di teoremi della matematica combinatoria entro (sottosistemi) della Aritmetica e dell'Analisi;
b) Logica lineare, entro la quale i suoi maggiori risultati sono stati quelli sulla semantica delle fasi per la logica lineare intuizionista, sulla logica lineare non-commutativa con due negazioni (calcolo dei sequenti e teorema di cut-elimination, semantica delle fasi, reti dimostrative), sulle applicazioni della logica lineare non-commutativa alla linguistica, sui criteri di correttezza per le reti dimostrative moltiplicative della logica lineare ciclica;
c) l'introduzione e l'indagine (con P. Ruet) della logica non-commutativa, raffinamento della logica lineare.
Abrusci è responsabile scientifico del sito "Roma Tre" entro la rete europea di ricerca TMR "Linear Logic in Theoretical Computer Science"(1998-2002), ed ha intensamente collaborato con centri di ricerca in Logica all'estero (in particolare, Università di Parigi 7, Institut de Mathematiques de Luminy a Marsiglia).
E' stato relatore in numerosi convegni nazionali e internazionali.
Ha promosso lo studio e la ricerca nella logica lineare e nelle sue applicazioni, in Italia, dirigendo e formando dottorandi di ricerca, e organizzando convegni nazionali e internazionali.

Testo inglese

Vito Michele Abrusci is Full Professor in Logic and Philosophy of Science at the University Roma Tre since 1996; he was Full Professor in Logic and Philosophy of Science at the University of Bari (1994-1996), associate professor in Mathematical Logic at the University Roma la Sapienza (1991-1994), associate professor in Philosophy of Science at the University of Bari (1988-1991) and researcher at the University of Firenze (1981-1988). He is President of the Italian Society of Logic and Philosphy of Sciecnes, since 1999.
Research activity of Vito Michele Abrusci covers mainly the following domains:
a) Proof theory (dilators), where his main results concern the non-provability of combinatorial mathematical theorems within (subsystems of) Arithmetics and Analysis;
b) Linear Logic, where his main results concern phase semantics of intuitionistic linear logic and non-commutative intuitionistic linear logic, the introduction and the investigation (sequent calculus with cut-elimination theorem, phase semantics, multiplicative proof nets) of non-commutative classical linear logic, applications of non-commutative linear logic to linguistics, correctness criteria for multiplicative proof-nets of Cyclic Linear Logic;
c) the introduction and the investigation (with P. Ruet) of Non-commutative logic, a refinement of Linear Logic.
Abrusci is scientific leader of team "Roma Tre" inside the European TMR Network "Linear Logic in Theoretical Computer Science" (1998-2002), and is in a strong and continuous collaboration with foreign research centers in Logic (mainly with Equipe de Logique at the University Paris 7 and with the Insititut de Mathematiques de Luminy in Marseille).
Abrusci has been invited speaker in many national and international conferences.
Abrusci has promoted the study and the research in Linear Logic and in the applications of Linear Logic in Italy, by supervising several PhD theses and by organizing national and international conferences.

1. ABRUSCI V.M., RUET P. (2000). Non-Commutative Logic, I: the multiplicative fragment. ANNALS OF PURE AND APPLIED LOGIC. vol. 101, pp. 29-64.
2. ABRUSCI V.M. (1995). Noncommutative proof nets. LONDON MATH. SOC. LECTURE NOTE SERIES. vol. 222, pp. 271--296 ISSN: 0-521-55961-8 Booktitle: Advances in linear logic (Ithaca, NY, 1993).
3. ABRUSCI V.M. (1991). Phase semantics and sequent calculus for pure noncommutativeclassical linear propositional logic. JOURNAL OF SYMBOLIC LOGIC. vol. 56 n.4, pp. 1403--1451 ISSN: 0022-4812 .
4. ABRUSCI V.M. (1987). Dilators, generalized Goodstein sequences, independence results: a survey. CONTEMPORARY MATHEMATICS. vol. 65, pp. 1--23 ISSN: 0271-4132 Logic andcombinatorics (Arcata, Calif., 1985), Amer. Math. Soc., Providence, R.I.
5. ABRUSCI V.M. (1999). Modules in Non-commutative Logic.
   In . TLCA '98 (J.-Y. Girard ed.), Springer.

Nº	Cognome	Nome	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
						2002	2003
Personale docente:
1	ABRUSCI	VITO MICHELE	FILOSOFIA	Prof. ordinario	M-FIL/02	7 (ore: 959)	7 (ore: 959)
Altro personale:
2	TORTORA DE FALCO	LORENZO	FILOSOFIA	Contrattista		7 (ore: 959)	7 (ore: 959)

1.7.2 Personale universitario di altre Università

Nº	Cognome	Nome	Università	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
							2002	2003
Personale docente:
1	GUERRINI	STEFANO	ROMA "La Sapienza"	INFORMATICA	Prof. associato	INF/01	3 (ore: 411)	8 (ore: 1100)
2	PIAZZA	MARIO	CHIETI	FILOSOFIA, SCIENZE UMANE E SCIENZE DELL'EDUCAZIONE	Ricercatore	M-FIL/02	8 (ore: 1100)	8 (ore: 1100)
Altro personale:
3	MAIELI	ROBERTO	ROMA "La Sapienza"	INFORMATICA	Assegnista		7 (ore: 959)	7 (ore: 959)

1.7.3 Titolari di assegni di ricerca

Nº	Cognome	Nome	Dipart./Istituto	Anno del titolo	Mesi uomo
					2002	2003
1	RE DAVID	LAURA	Dip. FILOSOFIA	2001	11 (ore: 1507)	7 (ore: 959)

1.7.4 Titolari di borse per Dottorati di Ricerca e ex L. 398/89 art.4 (post-dottorato e specializzazione)

Nº	Cognome	Nome	Dipart./Istituto	Anno del titolo	Mesi uomo

1.7.5 Personale a contratto da destinare a questo specifico programma

Nº	Qualifica	Costo previsto	Mesi uomo
1.	Contratto o assegno di ricerca	6000	4  (ore: 550)

1.7.6 Personale extrauniversitario dipendente da altri Enti

Nº	Cognome	Nome	Ente	Qualifica	Mesi uomo
1.	MASCARI	GIANFRANCO	CNR-Istituto per le applicazioni del calcolo	Ricercatore	14  (ore: 1925)
2.	PEDICINI	MARCO	CNR-Istituto per le applicazioni del calcolo	Ricercatore	14  (ore: 1925)

Testo italiano

Reti dimostrative: interazione e complessità

Testo inglese

Proof-nets: interaction and complexity

Testo italiano
LOGICA LINEARE ; RETI DI DIMOSTRAZIONE ; GEOEMETRIA DELL'INTERAZIONE

Testo inglese
LINEAR LOGIC ; PROOF- NETS ; GEOMETRY OF INTERACTION

Testo italiano

La Logica Lineare ([Gir87]) ha portato con sè un insieme di nuovi concetti che hanno permesso un notevole rinnovamento nella logica e nelle sue applicazioni all'informatica.
I. Proof-nets.
Tra i concetti introdotti dalla logica lineare, spicca quello di "proof-net" (rete di dimostrazione). Alle origini della logica lineare, i proof-nets sembravano semplicemente un nuovo formalismo ottenuto dai sistemi di deduzione naturale; in qualche modo si sono poi rilevati uno strumento essenziale per raffinare il sistema stesso, per studiarne gli aspetti dinamici (la normalizzazione delle prove) e per caratterizzare frammenti con proprietà computazionali notevoli (come la logica lineare polarizzata [Gir91], o i sistemi a bassa complessità [Gir98]).
I proof-nets sono dimostrazioni (programmi, via la corrispondenza di Curry-Howard) caratterizzate mediante pure proprietà geometriche (i "criteri di correttezza" [Gir87],[DR89]). D'altra parte, a ciascun proof-net si associa una funzione lineare tra spazi coerenti (una "cricca" [Gir87]) che resta invariata sotto il processo di normalizzazione. Lavori più recenti ([OTdF01]) sembrano indicare la possibilità di calcolare la forma normale di un proof-net a partire dalla cricca ad esso associata. Pertanto i proof-nets costituiscono già un primo passo nella direzione del superamento della distinzione tra sintassi e semantica, uno degli aspetti salienti della "ludica" di Girard ([Gir01]), che è una naturale evoluzione delle ricerche iniziate con la logica lineare. Nella logica non commutativa ([AR00],[MAI01]), usata anche per dare semantica a linguaggi di programmazione concorrente con vincoli, si considera un raffinamento del concetto di proof-net (i proof-nets non commutativi). I proof-nets, per il loro carattere modualare, hanno anche permesso di avviare uno studio matematico del concetto di "modulo di dimostrazione" ([DR89]), [Gir88]). Proprio questa caratteristica dei proof-nets, e la scoperta di due proprietà fondamentali quali la polarizzazione e la focalizzazione ([AM99],[Gir91]) sono alla base anche della ludica di Girard. La ludica e' un nuovo approccio allo studio delle regole della logica basato su una nuova nozione di gioco, nel quale il concetto fondamentale e' la localizzione fisica delle formule/risorse, anzi, la localizzazione e' il concetto primitivo del sistema ("Locus Solum", vedi [Gir01]). Questo studio sembra condurre al superamento della distinzione tra sintassi e semantica, una delle prospettive più promettenti aperte dalla ludica. Infatti, è nei risultati di completezza interna che sembra culminare gran parte del carattere innovativo e del bagaglio di conoscenze prodotti dalle ricerche in logica lineare. Il termine ``completezza interna'' sta ad indicare che la nozione di modello e di contromodello per un oggetto formale, va ricercata attraverso proprietà ``interne'' al sistema; ad esempio, nel caso si vogliano studiare le proprietà computazionali del sistema è la nozione interna di computazione che determina la nozione (derivata) di tipo e di modello.
II) Complessità.
In [Gir98], sono stati introdotti i sistemi ``Light Linear Logic'' ed ``Elementary Linear Logic'' che hanno permesso di caratterizzare in modo del tutto nuovo le classi di complessita' polinomiale ed elementare. Questo lavoro ha fornito ai ricercatori in logica lineare un nuovo e potente strumento per studiare i più noti e difficili problemi aperti in teoria della complessità.
III) Applicazioni.
Il paradigma di computazione basato sulla "costruzione focalizzata" delle dimostrazioni del calcolo dei sequenti, è stato uno dei primi risultati ottenuti da Andreoli nell'applicazione della logica lineare alla programmazione logica [And01,And92]. In particolare, ha segnato una svolta nella fondazione dei paradigmi di computazione grazie al punto di vista più fine permesso dai nuovi connettivi della logica lineare.
La proprietà di focalizzazione apporta interessanti contributi ad alcuni dei piu' importanti aspetti della computazione, come l'effettivo non-determinismo e l'informazione parziale. Questi aspetti sono particolarmente importanti nei contesti delle applicazioni fortemente distribuite, come la programmazione in Internet, dove non esiste un "focus" centrale con una visione dell'intera esecuzione, e dove si rivela necessaria una forma di coordinazione delle risorse fisiche e computazionali. Il paradigma attuale, basato sul calcolo dei sequenti focalizzati, tuttavia, risulta inadeguato quando si tratta di modellare l'esecuzione di applicazioni fortemente distribuite.
Il paradigma di costruzione focalizzata delle prove fornisce un buon livello di astrazione per comprendere gli aspetti principali della coordinazione grazie principalmente all'impiego della logica lineare e alla sua nozione di "risorse". Da un lato c'è il calcolo dei sequenti della logica lineare, dotato di una importante nozione di tempo e reversibilità di certe inferenze logiche, pagate al prezzo di una artificiale sequenzializzazione di tutte le inferenze che non è realistica nei domini di applicazione dove i componenti sono essenzialmente concorrenti (non-sequenziali).
Dall'altro lato ci sono le reti dimostrative che seppur prive degli aspetti di sequenzialiazzazione sono però:
(i) basate su un criterio di correttezza globale che richiede una visione dell'intera computazione per mantenere questa consistenza,
(ii) pensate principalmente per caratterizzare dimostrazioni complete, rendendo difficile il trattamento di dimostrazioni parziali (o incomplete) generate durante il processo di costruzione.

Testo inglese

Linear Logic ([Gir87]) introduced some new concepts that allowed a great renovation in logic and its applications in computer science.
I. Proof-nets
The concept of "proof-net" is one of the most important of linear logic. In the beginning, proof-nets seemed to be a new formalism obtained by natural deduction systems; then they resulted to be, in some way, an essential tool to refine the same systems, to study the dynamic aspects (normalization of proofs) and to characterize fragments with significant computational properties (such as polarized linear logic [Gir91] or systems with a low complexity [Gir98]). Proof-nets are proofs (and programs, by Curry Howard isomorphism) characterized by means of purely geometrical properties (the "correctness criteria" [Gir87] [DR89]). Besides, to each proof-net is associated a linear function in a coherent space (a "clique" [Gir87]), invariant under the normalization process. More recent studies ([OTdF01]) seem to indicate the possibility of calculating the normal form of a proof-net, just starting from that clique. For this reason, proof-nets are already a first step towards the abolition of the distinction syntax/semantics, an essential aspect in Ludics by Girard ([Gir01]), which in fact is a natural evolution of the research originated with linear logic. In non-commutative logic ([AR00], [Mai01]), even used to give semantics for concurrent programming languages with constraint, a new refined concept of proof-net (non commutative proof-net) is considered. Proof nets, for their modular characterization, also permit a mathematical study on a new object, the "proof-module" ([DR89], [Gir88]). This quality of proof-nets, with the two sighted properties of polarization and sequentialization ([AM99] [Gir91]), are at the base of Ludics by Girard. Ludics is an unknown approach to the rules of logic, based on a new notion of games, in which the spatial localization of the formulas/resources represents the essential, but even more the primitive, idea of the system ("Locus Solum", see [Gir01]). This study, which seems to abolish the distinction syntax/semantics, opens an attractive perspective in this direction with a sort of internal completeness. The expression "internal completeness" means that the notion of model and counter-model for a formal object has to be found just through immanent properties of the object itself. This novelty, coming from the knowledge acquired in linear logic, is the greatest innovative aspect of the new logic. If we want to study, for example, the computational features of a system we have to search the internal notion of computation, which produces the (derived) notion of type and model.
II. Complexity
In [Gir98], the systems "Light Linear Logic" and "Elementary Linear Logic" are introduced, allowing a completely new method for characterizing the classes with polynomial and elementary complexity, and giving to the researchers a powerful technique for studying the well-known open questions in the theory of complexity.
III. Applications
The computational paradigm based on the "focalized construction" of proofs in sequent calculus is one of the first results, by Andreoli, in the area of the applications of linear logic to logical programming ([And01], [And02]). In particular, it represents a turning point for the foundation of the computational paradigms, thanks to the refined approach provided by the new connectives of linear logic. The focalization property gets interesting contributions to some of the main aspects of computation, like the effective non-determinism and the partial information. These elements are particularly important in contexts with strongly distributed applications, like programming in Internet, where there isn’t a central "focus" with a global outlook of the execution and therefore a coordination between the resources is required. Nevertheless, the existing paradigm, based upon the focalized sequent calculus, is not adequate for modeling the execution of strongly distributed applications. The paradigm of the focalized proofs construction provides a good abstraction level in order to comprehend the main features of cooperation, because of the notion of "resource", introduced by linear logic. On one side, there is the sequent calculus of linear logic, equipped with an important notion of time and reversibility of logical inferences, obtained by means of an artificial sequentialization of all the inferences, which is not realistic in the application domains with concurrent components (not sequentializable). On the other side, there are proof nets which, although they are not sequentializable:
(i) are based on a global correctness criterion, requiring a visualization of the whole computation for keeping the consistency
(ii) are mainly thought for characterizing whole proofs and for this reason it's difficult to study the partial proofs arising during the construction process.

[Abr91]
V. Michele Abrusci.
Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic.
J. Symbolic Logic, 56(4):1403-1451, 1991.
[AG98]
Andrea Asperti and Stefano Guerrini.
The optimal implementation of functional programming languages.
Cambridge University Press, Cambridge, 1998.
With a foreword by Jean-Jacques Lévy.
[AM99]
Jean-Marc Andreoli and Roberto Maieli.
Focusing and proof-nets in linear and non-commutative logic.
In Logic for programming and automated reasoning (Tbilisi, 1999), pages 320-336. Springer, Berlin, 1999.
[AMR01]
Jean-Marc Andreoli, Roberto Maieli and Paul Ruet.
Constraint Based Proof Construction in Non-commutative Logic.
Preprint Institut de Math\`ematiques de Luminy.
Volume 33, 2001. Submitted.
[And92]
Jean-Marc Andreoli.
Logic programming with focusing proofs in linear logic.
J. Logic Comput., 2(3):297-347, 1992.
[And01]
Jean-Marc Andreoli.
Focussing and proof construction.
Ann. Pure Appl. Logic, 107(1-3):131-163, 2001.
[AR00]
V. Michele Abrusci and Paul Ruet.
Non-commutative logic. I. The multiplicative fragment.
Ann. Pure Appl. Logic, 101(1):29-64, 2000.
[BES98]
U. Berger, M. Eber, and H. Schwichtenberg.
Normalization by evaluation.
Lectures Notes in Computer Science, 1546, 1998.
[BP01]
Patrick Baillot and Marco Pedicini.
Elementary complexity and geometry of interaction.
Fund. Inform., 45(1-2):1-31, 2001.
Typed Lambda calculi and applications (L'Aquila, 1999).
[DR89]
Vincent Danos and Laurent Regnier.
The structure of multiplicatives.
Arch. Math. Logic, 28(3), 1989.
[DRR01]
Olivier Danvy, Morten Rhiger, and Kristoffer H. Rose.
Normalization by evaluation with typed abstract syntax.
J. Funct. Programming, 11(6):673-680, 2001.
[ER60]
P. Erdos and A. Rényi.
On the evolution of random graphs.
Magyar Tud. Akad. Mat. Kutató Int. Közl., 5:17-61, 1960.
[Gir87]
Jean-Yves Girard.
Linear logic.
Theoret. Comput. Sci., 50:1-101, 1987.
[Gir88]
Jean-Yves Girard.
Multiplicatives.
Universitá e Politecnico di Torino. Seminario Matematico. Rendiconti, 1987:11-33, 1988.
[Gir91]
Jean-Yves Girard.
A new constructive logic: classical logic.
Math. Structures Comput. Sci., 3, 1991.
[Gir96]
Jean-Yves Girard.
Proof-nets: the parallel syntax for proof-theory.
Lecture Notes in Pure and Appl. Math., 180(3):97-124, 1996.
Logic and algebra (Pontignano, 1994).
[Gir98]
Jean-Yves Girard.
Light linear logic.
Inform. and Comput., 143:175-204, 1998.
[Gir01]
Jean-Yves Girard.
Locus solum: from the rules of logic to the logic of rule.
Math. Structures Comput. Sci., 11(3):301-506, 2001.
[GM01]
Stefano Guerrini and Andrea Masini.
Parsing MELL proof nets.
Theoret. Comput. Sci., 254(1-2):317-335, 2001.
[GMM01]
Stefano Guerrini, Simone Martini, and Andrea Masini.
Proof nets, garbage, and computations.
Theoret. Comput. Sci., 253(2):185-237, 2001.
Models and paradigms for concurrency (Udine, 1997).
[Mai01]
Roberto Maieli.
A new correctness criterion for multiplicative non commutative proof-nets.
Preprint Institut de Mathèmatiques de Luminy, n.13, 2001.
To appear in Archive for Mathematical Logic.
[Mas00]
G. F. Mascari.
Towards noncommutative computing.
In Proceedings of the 1999 Euroconference: On Non-commutative Geometry and Hopf Algebras in Field Theory and Particle Physics (Torino), volume 14, pages 2451-2454, 2000.
[MF00]
M.Pedicini and F.Quaglia.
A parallel implementation for optimal lambda-calculus reduction.
In Proc. ACM-SIGPLAN 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal (Canada). ACM Press., September 2000.
[MP94]
G. F. Mascari and M. Pedicini.
Head linear reduction and pure proof net extraction.
Theoret. Comput. Sci., 135(1):111-137, 1994.
Selected papers of the Meeting on the Mathematical Foundations of Programming Semantics (MFPS '92), Part I (Oxford, 1992).
[MR00]
Roberto Maieli and Paul Ruet.
Non-commutative logic III: focusing proofs.
Preprint Institut de Math\`ematiques de Luminy.
Volume 14, 2000. Submitted.
[OTdF01]
Laurent Olivier and Lorenzo Tortora de Falco.
Slicing polarized additive normalization.
Quaderno I.A.C.-C.N.R., n.12, 2001.
To appear in Advances in Linear Logic, Cambridge University Press.
[Ped96]
Marco Pedicini.
Remarks on elementary linear logic (preliminary report).
In Linear logic 96 (Tokyo), page 12 pp. (electronic). Elsevier, Amsterdam, 1996.
[Pia01a]
Mario Piazza.
Geometrical (non commutative) phase spaces.
Technical report, Dipartimento di Filosofia, Università di Chieti, 2001.
Submitted.
[Pia01b]
Mario Piazza.
Multiple context-free grammars have a greibach normal form.
Technical report, Dipartimento di Filosofia, Università di Chieti, 2001.
Submitted.
[TdF01a]
Lorenzo Tortora de Falco.
The additive multiboxes.
Quaderno I.A.C.-C.N.R., n.8, 2001.
To appear in Annals of Pure and Applied Logic.
[TdF01b]
Lorenzo Tortora de Falco.
Obsessional experiments for linear logic proof-nets.
Quaderno I.A.C.-C.N.R., n.11, 2001.
To appear in Mathematical Structures in Computer Science.

Testo italiano

A) I temi della Ricerca
La ricerca dell'Unità si concentrerà su tre temi nei quali si fondono problematiche semantiche e sintattiche, aspetti dinamici e statici delle computazioni, questioni fondazionali e applicative.
I. Proof-nets.
1. Iniettività della semantica denotazionale e sua estensione a frammenti più ampi.
Nel suo primo lavoro sulla logica lineare, Girard introduce la nozione di "esperienza", che viene poi usata per associare ad ogni dimostrazione (proof-net) una funzione (la "semantica" della dimostrazione). Nell'introdurre le esperienze, Girard mostra come esse permettano di "calcolare" la semantica di una dimostrazione. In [TdF01b] viene posto il problema dell'iniettivita` della semantica dei proof-nets: si vuol compiere un confronto tra la relazione di equivalenza definita sui proof-net dal processo di eliminazione del taglio (o sintattica) e quella definita dalla semantica. Quando le due relazioni coincidono, si dice che la semantica e` "iniettiva". Grazie alla nozione di "esperienza ossessiva", si dimostra che la semantica coerente e` iniettiva per alcuni frammenti significativi della logica lineare, ma non e` iniettiva in generale. Il risultato negativo contenuto in [TdF01b] (la non iniettivita` della semantica coerente) spinge a ripensare la procedura di eliminazione del taglio, alla luce della proprieta` di "uniformita`" della semantica coerente. In assenza di uniformita`, la semantica coerente diventa semplicemente la semantica relazionale, ed i controesempi alla non iniettivita` svaniscono. Questo conduce al (difficile) problema di trovare un'alternativa agli esponenziali della logica lineare (cioe` un'alternativa alla gestione della duplicazione in logica lineare). Ci proponiamo di affrontare la questione usando le semantica introdotta da T. Ehrhard nel suo recente lavoro "Finiteness spaces" (sottoposto a pubblicazione), e la normalizzazione del lambda-calcolo differenziale (introdotto da Ehrhard e Regnier proprio facendo uso della nuova semantica): sembra infatti che per il lambda-calcolo differenziale possa definirsi una normalizzazione "non uniforme". Questa pone dei problemi molto simili a quelli posti dalla normalizzazione in presenza di additivi, e si pensa di tentare un approccio facendo uso della nozione di "multiscatole" (introdotta in [TdF01a]). In alternativa, dall'osservazione che i proof-nets e le loro interpretazioni sono a tutti gli effetti degli oggetti combinatori si deriva la possibilità di utilizzare metodi combinatori nello studio della semantica. Verrà considerata la possibilità di applicare, allo studio dell'iniettività per la semantica di qualche frammento della logica lineare, il metodo probabilistico introdotto da Erdos ed utilizzato con grande successo nella teoria dei grafi (cf. [ER60]).
2. Calcolo semantico della forma normale dei proof-nets.
I risultati positivi presenti in [TdF01b] vengono utilizzati nel lavoro [OTdF01] per introdurre una nuova sintassi per il frammento polarizzato della logica lineare (con gli additivi). In presenza di additivi, la normalizzazione (come la sequenzializzazione) pone da sempre seri problemi. Varie proposte di sintassi sono state avanzate negli ultimi anni (tra cui quella facente uso di "multiscatole", vedi [TdF01a]), ma solo grazie alla iniettivita` della semantica (ed unicamente per il frammento polarizzato) sembra essersi trovata una soluzione abbastanza soddisfacente: si dimostra in [OTdF01] che la vecchia idea di Girard di pensare ad un proof-net come all'insieme delle sue "fette non additive" e` corretta se ci si restringe al frammento polarizzato. La tecnica utilizzata in [TdF01b] per dimostrare l'iniettivita` della semantica consiste nel "ricostruire" un proof-net senza tagli (e con soli assiomi atomici) a partire dalla sua semantica. Recentemente, ci si e` resi conto che questa tecnica permette in realta` anche di "calcolare semanticamente" la forma normale di un proof-net (si calcola la semantica di un dato proof-net e poi si ricostruisce l'unico proof-net senza tagli con tale semantica: questo non puo` essere altro che la forma normale del proof-net di partenza). Questo approccio al calcolo e` noto, nell'ambito dello studio dei linguaggi di programmazione funzionale, come "Normalization by evaluation" (vedi [BES98] e [DRR01]). Ci proponiamo di approfondire i legami tra la "Normalization by evaluation" e le tecniche dimostrative introdotte in [TdF01b]. Il lavoro [OTdF01] puo` essere considerato come un primo passo in questa direzione. Per condurre con successo un tale studio, sembra importante cominciare con l'estendere a frammenti piu` ampi il risultato di iniettivita` dimostrato in [TdF01b], partendo dall'intero frammento polarizzato.
3. Moduli di dimostrazione.
Ci proponiamo di sviluppare la teoria dei moduli di dimostrazione, nel frammento moltiplicativo della logica lineare e della logica non-commutativa. In particolare, intendiamo: a) dare una definizione di modulo e di tipo di un modulo nella logica non-commutativa, senza far ricorso alla nozione di bilateralità (che richiede l'esame dell'interno del modulo); b) studiare altre operazioni sui moduli, oltre quella che permette - dati due moduli ortogonali tra loro - di ottenere una rete dimostrativa; c) investigare le relazioni tra i moduli e la ludica.
4. Contenuto computazionale della riduzione dei proof-nets della logica non-commutativa.
Intendiamo caratterizzare il contenuto computazionale della logica non-commutativa, mediante una fine analisi delle riduzioni guidata dal concetto di ortogonalità implicito negli interruttori.
5. Costruzione focalizzata delle prove attraverso proof-nets focalizzati.
L'obiettivo è quello di sviluppare ulteriormente il paradigma di costruzione focalizzata delle prove, cercando di superare i limiti dell'attuale modello legato al calcolo dei sequenti. In un sistema distribuito manca infatti un locus centrale dove le transizioni vengono effettuate; in realtà ogni componente è visto come un gestore di risorse che si occupa solo di un pezzo della prova e che effettua solo alcune determinate inferenze; in altre parole, ogni componente dovrebbe essere più realisticamente visto come un "modulo" che partecipa al processo di costruzione della dimostrazione. Ora, è difficile "tagliare" le dimostrazioni del calcolo dei sequenti in moduli componibili, e ciò principalmente a causa della loro natura sequenziale. L'approccio attuale, nonostante faccia ricorso a dimostrazioni bipolari astratte equipaggiate con sistemi di equazioni lineari (che desequenzializzano le prove), non può essere considerato soddisfacente. Una soluzione più interessante e naturale - proposta da Andreoli nel convegno "Logic and Interaction"(Marsiglia,febbraio 2002)- sembra essere quella del ricorso alle reti dimostrative, o più in generale a strutture parziali (o moduli) e alla loro composizione. Il primo passo è dunque quello di scegliere la nozione adeguata di struttura di prova, mediante la definizione di una variante della tradizionale nozione di struttura dimostrativa, che tenga conto della proprietà di focalizzazione e bipolarizzazione già riscontrate nel calcolo dei sequenti della logica lineare e della logica non commutativa. Un secondo passo è quello di definire un criterio di correttezza, intrinseco alle strutture dimostrative bipolari e focalizzate, che risulti equivalente a quello dei proof-nets ([DR89]) e dei proof-nets non-commutativa ([AR00,Mai01])e che sia inoltre incrementale e modulare. In altre parole un criterio che non richieda necessariamente di percorrere tutta la struttura coinvolta, bensì solo l'effettivo bordo della struttura impiegato nella composizione dei componenti. Nel frammento moltiplicativo (commutativo o non commutativo) della logica lineare la questione dell'adattabilità del criterio sembra semplice: in tale caso, infatti, assicurarsi che una struttura di prova parziale sia corretta può essere fatto in maniera modulare, locale ed incrementale. Un terzo passo è quello poi di estendere tale approccio ad un frammento più largo che tenga conto almeno dei connettivi additivi. In realtà anche in questo caso i presupposti sembrano essere incoraggianti dato che esistono già dei criteri per le reti di MALL [Gir96] che potrebbero bene adattarsi alla definizione del nuovo paradigma di computazione basato sulle reti dimostrative.
6. Connettivi e nuovi quantificatori in Ludica.
Ci proponiamo lo studio di nuovi connettivi suggeriti dalla Ludica ([GIR01]), e n particolare l'analisi, mediante reti dimostrative, di nuovi quantificatori che estendono quelli sinora definibili nella Logica Lineare. A tale fine sembra essenziale il passaggio attraverso reti dimostrative, visto che tali quantificatori non sembrano facilmente definibili mediante una nozione di correttezza locale per la la loro introduzione - come avviene nel calcolo dei sequenti o nella deduzione naturale - ma serve invece, una nozione di correttezza globale della dimostrazione - come avviene nei criteri di correttezza delle reti di dimostrazione.
II. Interazione e Complessità.
1. Geometria dell'interazione e complessità.
L'obiettivo è indagare la possibilità di legare il concetto di complessità algoritmica alla rappresentazione matematica ``operazionale'' e dinamica del concetto di computazione. Questo campo di ricerca unisce gli sviluppi recenti nell'ambito delle logiche derivate dalla logica lineare e a complessità intrinseca (Light Linear Logic ed Elementary Linear Logic) con lo studio della semantica operazionale principalmente nei suoi aspetti interattivi. La novità di questo approccio risiede nel fatto che sino ad ora le interazioni tra logica e complessità hanno sempre avuto come tramite le versioni ``descrittive'' della computazione, quindi descrizioni statiche, mentre grazie a questo approccio si cercherà di mettere in evidenza gli aspetti dinamici. L'orizzonte applicativo di questa ricerca è dato dalla possibilità di stabilire i requisiti che un linguaggio di programmazione deve soddisfare per avere un limite di complessità fissato a priori: cioè tale che i programmi che vanno oltre una data classe di complessità non possano essere neanche espressi nel linguaggio [Ped96,BP01].
2. Caratterizzazione di classi di complessità tramite sistemi logici.
L'obiettivo è quello di studiare sistemi che permettano di caratterizzare classi di complessita' computazionale, seguendo la linea di ricerca indicata da Girard con la Light Linear Logic e la Elementary Linear Logic. In particolare, si intende studiare l'estensione di tali sistemi mediante connettivi per il non-determinismo. Tali sistemi saranno descritti ed analizzati mediante grafi, seguendo il paradigma locale ed asincrono delle riduzioni condivise.
III. Orizzonti Applicativi.
1. Applicazione della logica non-commutativa alla linguistica.
La logica non commutativa è la naturale estensione del Calcolo Sintattico di Lambek, che trova applicazioni alla linguistica attraverso la corrispondenza tra formule e tipi di espressioni linguistiche, e tra derivazione di un sequente e attribuzione di un tipo ad un'espressione in dipendenza dal tipo delle sue componenti. La maggiore capacità espressiva della logica non-commutativa (dovuta alla presenza simultanea di congiunzioni/disgiunzioni non commutative e congiunzioni/disgiunzioni commutative, e alla presenza degli esponenziali) rende possibile ampliare tali applicazioni linguistiche.
2. Logica Lineare e concorrenza.
Recenti risultati sulle reti dimostrazioni ed i progressi sulla Logica Lineare Polarizzata, consentono di fornire sistemi per la Logica Classica con un contenuto computazionale. Il naturale campo di applicazione di questi sistemi logici e' lo studio delle proprieta' dei sistemi concorrenti.
3. Semantica dei giochi e calcoli distribuiti.
A partire dalla semantica della riduzione sono stati ottenuti risultati sugli aspetti operazionali della computazione nel lambda calcolo, in particolare sistemi per la riduzione ottimale. Inoltre, questi sistemi si caratterizzano per il fatto di operare mediante transizioni locali ed asincrone (a differenza della beta-riduzione che è sostanzialmente un'operazione globale). Questi sistemi, denominati di riduzione virtuale, hanno permesso di sviluppare un'implementazione distribuita della riduzione del lambda calcolo a partire dalla geometria dell'interazione derivata da:
a)un lavoro teorico che ha messo in luce i legami tra geometria dell'interazione e riduzione ottimale e che ha semplificato gli aspetti algebrici del calcolo necessari alla gestione della condivisione,
b)un lavoro di tipo più applicativo per gestire la grana estremamente fine della computazione allo scopo di limitare il costo computazionale necessario a distribuire il lavoro.
Il linguaggio implementato è poi stato esteso con ulteriori costrutti funzionali e non, che richiedono un ulteriore passo di modellizzazione teorica per chiarirne i rapporti con la teoria generale delle riduzioni virtuali, per mettere in luce gli aspetti di complessità e quelli che riguardano il parallelismo. Il quadro più adatto per questo lavoro è fornito dai modelli dei giochi di Abramsky et al. che permettono di catturare un gran numero di costrutti (anche non funzionali), e di modellizzare anche gli aspetti intensionali delle computazioni.
B) Attività di ricerca.
I) Collaborazione Nazionale e internazionale, Convegni e Workshops.
- Soggiorni di corta e media durata presso altre sedi in Italia ed all'estero;
- inviti a eminenti studiosi stranieri per periodi di circa un mese;
- organizzazione di workshops tematici sui temi della ricerca.
II) Pubblicazioni.
I risultati delle ricerche sopra elencate saranno oggetto di pubblicazioni sulle riviste internazionali di logica e di informatica teorica.

Testo inglese

A) The research themes
The research activity will focus on three main themes. Their study involves syntax and semantics, statical and dynamical aspects of computations, foundational problems and applications.
I. Proof-nets.
1. Injectivity of denotational semantics and its extension to larger fragments. In his first work on linear logic, Girard introduces the notion of "experiment", which he uses to associate with every proof-net a function (the "semantics" of the proof). He also shows how it is possible to "compute" the semantics of a proof-net by means of this notion of experiment. In [TdF01b] the question of injectivity of the semantics of proof-nets is addressed: one wants to compare the (syntactical) equivalence relation defined on proof-nets by the cut-elimination procedure and the one defined by denotational semantics. If the two relations coincide, the semantics is said to be injective. Thanks to the notion of "obsessional experiment", it is proven that coherent semantics is injective for some remarkable fragments of linear logic, but it isn't injective in the general case. The negative result of [TdF01b] (the counter-example to the injectivity of coherent semantics) suggests to reconsider the cut-elimination procedure, and more precisely its "uniformity feature", coming from the "uniformity property" of coherent semantics. In the absence of uniformity, coherent semantics becomes relational semantics, and the counter-examples to the injectivity property vanish. This leads to the (difficult) problem of finding an alternative to the exponentials of linear logic (which means an alternative way to deal with duplication in linear logic). For his purpose we would like to use the recent work of T. Ehrhard "Finiteness spaces" (submitted for publication), and the normalization of the differential lambda-calculus (introduced by Ehrhard and Regnier as a syntactical counterpart of the new semantics): indeed, it seems to be possible to define in this framework a "non uniform" normalization. There are several problems arising when considering such a normalization procedure, all very similar to the ones induced by the presence of the additive connectives of linear logic, and we plan to attack them by means of the notion of "multibox" (introduced in [TdF01a]). A different possible approach is to remember that proof-nets and their semantical interpretations are combinatoric objects, so that the methods of combinatorics should apply to study the semantics of proof-nets. We will consider the possibility of applying to the study of the injectivity property of some fragments of linear logic the probabilistic method introduced by Erdos, which has been very successful in graph theory (cf. [ER60]).
2. Semantical computation of the normal form of a proof-net.
The positive results of [TdF01b] are used in [OTdF01] to introduce a new syntax for the polarized fragment of linear logic (including the additive connectives). In presence of the additives, normalization and sequentialization are problematic. Several improvements of the original syntax have been proposed (among which the one making use of "multiboxes", see [TdF01a]), but only thanks to the injectivity property (and only for the polarized fragment) a satisfactory solution seems to have been found: it is proven in [OTdF01] that Girard's old idea to define a proof-net as the set of its "non additive slices" is correct, provided one restricts to the polarized fragment. The technique used in [TdF01b] to prove the injectivity of the semantics is to "rebuild" a cut-free proof-net (with atomic axiom links) from its semantical interpretation. Recently, we realized that the same technique allows actually to "semantically compute" the normal form of a proof-net (one computes the semantics of a given proof-net and one rebuilds the unique cut-free proof-net with the given semantics: this can only be the normal form of the proof-net we started from). This approach to computation is known, among the researchers of the functional programming language community, as "Normalization by evaluation" (see [BES98] and [DRR01]). We will study the relationships between "Normalization by evaluation" and the techniques developed in [TdF01b]. The work [OTdF01] can actually be seen as a first step in this direction. In order for this research to be successful, it seems important to first extend the injectivity result of [TdF01b] to wider fragments, starting from the whole polarized fragment.
3. Modules of Proof-nets.
We aim to further develop the theory of modules for proof-nets of the multiplicative fragment of linear and non-commutative logic. In particular we aim at: a) giving a definition of module and module type of non-commutative logic without making use of the bilaterality notion (which requires to explore the inner part of a proof-net); b) studying new operations besides those which allow to obtain a correct proof-net starting from two modules which are orthogonal between them; c) investigating the relationship between modules and Ludics.
4. Computational contents of non-commutative proof-nets reduction.
We intend to characterize the computational contents of non-commutative logic by means of a fine analysis of reduction driven by the notion of orthogonality which is implicit in the behaviours of switchings.
5 Proof construction via focussing proof-nets.
Our goal will be to further develop the current focussing proof construction paradigm, with trying to overcome the limitations of the current model, based on the sequent calculus. Indeed, in distributed systems there is no "central locus" where transactions are executed. Actually, each component is viewed as a resource manager which holds a bit of a proof and executes only some specific inferences; in a more realistic way, each component should be viewed as a module taking part in the proof construction process. Now, it seems quite hard "to cut" sequent proofs into composable modules; that, mainly, depends on the strong sequential nature of the former ones. Although the current approach makes use of abstract bipolar proofs, equipped with linear constraint systems allowing the sequentialization of proofs, it cannot be considered satisfiable. A more natural and promising approach, recently pointed out by Andreoli at the "Logic and Interaction Weeks" held in Marseille (February 2002), seems to make use of proof-nets: more in general, partial proof-structures (or modules) and their compositionality. The first step in this direction, is to choose a notion of proof-structure, by varying the traditional definition of proof-structure, that takes into account the focussing and bipolar properties, already satisfied by the linear and the non-commutative sequent calculi [MR00,AMR01]. A second step consists in defining a correctness criterion intrinsic to the focussed and bipolarized proof-structures; this criterion should also result to be equivalent to the existing ones (linear [Gir87] and non-commutative [AR00, Mai01]), modular and incremental. In other words this new criterion should not require to visit all the involved proof-structures, but only the border actually required for their composition. Now, as also suggested by Andreoli, the question of fitting the existing criteria to the new problem seems reasonably feasible, at least in the multiplicative fragment of linear and non-commutative logic. Indeed, we can provide the correctness of (linear and non-commutative) proof structures in a modular, local and incremental way. A further step will finally be to extend the previous approach (seen at step one and two) to a larger fragment of linear and non-commutative logic, which will take into account at least the additive connectives. In this case encouraging premises come from the existing correctness criteria for MALL [Gir96] which appear quite suitable for the definition of the new computational paradigm based on proof-nets.
6. New connectives and quantifiers in Ludics.
We propose to study the new connectives suggested by Ludics [Gir01], in particular we aim to analyze, by means of the proof-net technology, the new quantifiers which extend those ones already defined in linear logic. In order to grasp this aim we need, again, to look at proof-nets, since, there is no easy way to define, like in the case of the sequent calculus or natural deduction, a local notion of correctness for the introduction of these new quantifiers; indeed, these latter require, like in the case of proof-nets, a global notion of correctness.
II. Interaction and Complexity
1. Geometry of interaction and complexity.
The scope of this study is to investigate the possibility to link the concept of computational complexity to the mathematical interpretation of operational semantics appearing in the dynamics of execution of proof-nets.
Many recent developments have been conflated in order to obtain logical systems with intrinsic complexity bounds. They are based on control and restriction of exponential connectives of linear logic (Light Linear Logic and Elementary Linear Logic). We wish to extend this approach in order to unify the syntactic results and the operational aspects mainly from an interactive point of view.
The main novelty of this approach is to be found in the fact that classical studies on this topic consider complexity classes as a descriptive tool to analyze computations, whence its nature is static. Enforcing the operational approach to these studies, we will be able to establish how to obtain complexity bounds on the execution by restrictions on dynamics.
Expected application of this search is the possibility to establish requirements that a programming language must satisfy in order to respect a complexity bound fixed a priori: i.e. such that programs beyond this given complexity class cannot be expressed in the language.
2. Study of a characterization of complexity classes implicitly derived from logical systems.
The object is the study of systems which allow to characterize computational complexity classes, following the line of search indicated by J.-Y. Girard with the introduction of Light Linear Logic and Elementary Linear Logic. In particular, we expect extensions of such systems by means of new connectives for non-determinism. Such systems will be described and analyzed using graphs, following the local and asynchronous paradigm of shared reductions.
III. Applications.
1. Application of non-commutative logic to linguistics.
Non-commutative logic is the natural extension of the syntax of Lambek Calculus; this calculus finds its application to linguistics through a correspondence between formulas of logic and types of linguistic expressions, and between derivations of a sequent and attribution of a type to a linguistic expression obtained from the type of its members.
The finer expressive power of non-commutative logic widens the linguistic applicability of Lambek Calculus, especially due to the simultaneous presence of conjunctive/disjunctive commutative/non-commutative connectives, and to the presence of exponentials.
2. Linear logic and concurrency.
Recent progress in the study of proof nets and in the study of Polarized Linear Logic, suggests the possibility to obtain systems with computational meaning associated to proofs coming from Classical Logic.
The natural field of application of these systems is the study of programming languages for concurrent systems.
3. Games semantics and distributed systems.
Semantics of reduction is the theoretical tool considered to tackle operational aspects of lambda calculus, in particular with the studies on shared reductions. Moreover, in these systems execution is based on local and asynchronous transitions, and this is a remarkably property with respect to beta-reduction of lambda calculus which is essentially a global operation.
These systems, called virtual reductions, permitted the development of a distributed implementation of execution, based on geometry of interaction. In order to obtain this implementation:
a) a theoretical work was required to bring out the deep connection between geometry of interaction and optimal reduction and a
simplification of the theory to clarify the algebraic aspects involved in the shared management of the computation.
b) an applicative work to manage the extremely fine-grained kind of computation discovered, in order to limit computational overhead cased by distributing workload in a parallel architecture.
We implemented a functional language based on PCF, but the operational aspects of the newly introduced constructs demand an improvement of the theoretical model to be integrated in the general theory of virtual reductions.
It seems that the most promising direction in this research is to consider game semantics for programming languages, exploited to capture intensional aspects of computation (especially for what may concern continuations and side effects) in Abramsky et al.'s works on fully abstraction.
B) Research Activity.
I) National and International Collaborations, Meetings and Workshops.
We plan short term stays at research centers working on the above listed research themes.
We will promote a short term visiting researchers programme from European and Extra-European laboratories.
We will organize joint thematic workshops on the research themes.
II. Publications.
We plan to publish our results in international journals of logic, theoretical computer science and mathematics.

Nº	Anno di acquisizione	Descrizione
		Testo italiano	Testo inglese

Attrezzatura I
Descrizione

valore presunto ( Euro)   percentuale di utilizzo per il programma

Attrezzatura II
Descrizione

valore presunto ( Euro)   percentuale di utilizzo per il programma

QUADRO RD

4.1.1 Altro

QUADRO RA

4.2.1 Altro

Firma ____________________________________________

(per la copia da depositare presso l'Ateneo e per l'assenso alla diffusione via Internet delle informazioni riguardanti i programmi finanziati; legge del 31.12.96 n° 675 sulla "Tutela dei dati personali")