Testo italiano

Dalla Prova alla Computazione con la Logica Lineare

Testo inglese

From Proof to Computation through Linear Logic

Testo italiano

La Logica Lineare e' stata introdotta da Girard nel 1986 come un raffinamento della logica classica e intuizionista, caratterizzato in particolare dall'introduzione di nuovi connettivi (esponenziali) che danno uno status logico alle operazioni di cancellazione e copia (corrispondenti alle "regole strutturali" dei calcoli a sequenti classico e intuizionista).
In altri termini, con la Logica Lineare, le formule logiche sono assimilate a "risorse fisiche", con innumerevoli e quasi immediate applicazioni all'Informatica, che vanno dalla rappresentazione di aspetti operazionali dei linguaggi di programmazione e delle loro strategie, ad una ridefinizione dinamica della nozione di complessita' di calcolo, da analisi di linearita' e raffinamenti dei sistemi di tipi per linguaggi sequenziali, alla definizione di nuovi strumenti per la semantica di linguaggi sequenziali e concorrenti.
Dalla sua nascita, la Logica Lineare ha assunto un ruolo via via crescente nel campo delle applicazioni della logica all'informatica; ha introdotto un insieme di concetti completamente originali (semantica delle fasi, reti di prova, spazi coerenti, geometria dell'interazione), ha riscoperto e messo in uso strumenti precedenti (categorie *-autonome, teoria e semantica dei giochi), e ha profondamente rinnovato e ringiovanito l'intero settore della ricerca teorica.
Dunque, la Logica Lineare non e' solo una teoria elegante ed estremamente potente, ma anche, e innanzitutto, una sorgente di linee guida metodologiche. Per questa ragione lo scopo di questo progetto e' duplice. In primo luogo vogliamo utilizzare la logica lineare come un tema federativo, particolarmente adatto per raccogliere l'esperienza di quei ricercatori italiani che si sono imbattuti nelle sue nozioni o hanno utilizzato i suoi strumenti nel corso della loro pratica scientifica. In questo ambito vogliamo collaborare per ulteriormente indagare sulla struttura della Logica Lineare e per applicare le metodogie da essa suggerite a specifici problemi dell'Informatica. In secondo luogo vogliamo riflettere in generale sulle relazioni tra Logica Lineare e Informatica Teorica, iniziando un lavoro di sistematizzazione dei vari risultati ottenuti e cercando di definire ulteriori sviluppi.
Le sedi partecipanti al progetto raccolgono quasi tutti i ricercatori che lavorano in Italia nell'ambito della Logica Lineare, e che gia' hanno collaborato tra loro in progetti di ricerca nazionali e internazionali. Ci attendiamo quindi da tale sinergia una conoscenza piu' profonda di vari problemi fondamentali dell'Informatica, una organizzazione piu' chiara e unitaria dei nostri campi di ricerca, una visione critica e innovativa dei rapporti tra Logica Lineare e Informatica Teorica.

Testo inglese

Linear logic was introduced by Girard in 1986 as a refinement of classical and intuitionistic logic, in particular characterized by the introduction of new connectives (exponentials) which give a logical status to the operations of erasing and copying (corresponding to the "structural rules" of classical and intuitionistic sequent calculi). In other words, with linear logic, logical formulae really becomes physical resources, with a lot of almost immediate applications to Computer Science, spanning from the representation of operational aspects of programming languages and their evaluation strategies, to a dynamic definition of the notion of computational complexity, from linearity analysis and refined type synthesis for sequential languages, to the semantics of sequential and concurrent programming languages. Since its birth, Linear Logic has taken increasing importance in the field of logic in computer science; it carried a set of completely original concepts (phase semantics, proof nets, coherent spaces, geometry of interaction), rediscovered and put to use previous tools (*-autonomous categories, game semantics), and deeply renewed the field. So, Linear logic is not only an elegant and powerful technical theory but, first of all, a source of methodological guidelines. For this reason, the aim of our project is twofold. Firstly, we want to use Linear Logic as federating theme, very suitable for gathering the expertise and experience of all those Italian researchers who have encountered it in their scientific practice. In this context, we want to collaborate each other in order to further explore the structure of Linear Logic and to use the methodologies from it for solving particular problems in Computer Science. Secondly, we want to reason on the relationships between Linear Logic and Theoretical Computer Science, through an analysis of the obtained results. We aim to define new developments. Almost all the Italian researches working in Linear Logic are present in this project, and they already collaborated in Italian and international research projects. What we expect from such a synergy is a deeper understanding of several fundamental problems of Computer Science, a clearer and more unified organization of our fields of research, and a new critical view of the relationships between Linear Logic and Theoretical Computer Science.

INF/01 - INFORMATICA

Testo italiano
LOGICA LINEARE ; RETI DI PROVA ; LUDICA ; LOGICA LINEARE LEGGERA ; SEMANTICA A GIOCHI ; LOGICA LINEARE ELEMENTARE ; SPAZI COERENTI

Testo inglese
LINEAR LOGIC ; PROOF-NETS ; LUDICS ; LIGHT LINEAR LOGIC ; GAME SEMANTICS ; ELEMENTARY LINEAR LOGIC ; COHERENCE SPACES

RONCHI DELLA ROCCA	SIMONETTA
(cognome)	(nome)

Professore ordinario	20/11/1946	RNCSNT46S60B111P
(qualifica)	(data di nascita)	(codice di identificazione personale)

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

011/6706734	011/751603	ronchi@di.unito.it
(prefisso e telefono)	(numero fax)	(E-mail)

Testo italiano

Simonetta Ronchi Della Rocca è, dal 1987, professore ordinario di “Fondamenti dell’Informatica” presso l’Università di Torino, Dipartimento di Informatica.
E’ stata professore visitatore presso l’Equipe di Logica Lineare dell’IML di Marsiglia. E’ stata responsabile di unità per progetti della UE (HCM Lambda
Calcul Typé, TMR Linear Logic) e per progetti cofinanziati (Logica Lineare, Logica Lineare ed oltre). E’ stata membro di Comitati di Programma e invited
speaker per varie conferenze internazionali, tra cui piu’ recentemente: LICS 92, Logic Colloquium 94, Logic Colloquium 95, TLCA 99, TLCA 01, ICTCS 01.
E’ stata conference co-chair del LICS 99. E’ membro dell’Organizing Program del LICS. E’ membro del collegio docenti del corso di dottorato in Informatica dell’Università di Torino. E’ stata relatore di tesi di dottorato di Luca Roversi (ora ricercatore presso l’Università di Torino), Luigi Liquori (ricercatore presso l’INRIA) e Alberto Pravato (professore a contratto presso l’Università di Venezia), ed è stata membro di numerose commissioni di dottorato all’estero. E’ editore della rivista “ACM Transactions on Computational Logic”. I suoi interessi di ricerca sono nel campo dell’Informatica Teorica, in particolare Semantica Formale dei linguaggi di programmazione, Logica della programmazione e Teorie dei Tipi.

Testo inglese

Simonetta Ronchi Della Rocca is full Professor since 1987, teaching "Foundations of Computer Science" at the University of Torino, Departement of Computer
Science. She has been visiting professor at the Linear Logic Group of IML in Marseille. She has been site leader for UE research projects (HCM Typed
lambda calculus, TMR Linear Logic) and of MIUR projects (Linear Logic, Linear Logic and Behind). She has been member of program Committees and
invited speaker for some international conferences, the more recent being : LICS 92, Logic Colloquium 94, Logic Colloquium 95, TLCA 99, TLCA 01, ICTCS01. She has been conference co-chair for LICS 99. She is member of LICS Organizing Committee. She is in the teaching board of the Computer Science PhD Program of Turin University. She has been PhD advisor of Luca Roversi (research fellow, University of Turin), Luigi Liquori (INRIA researcher) and Alberto Pravato (lecturer, University of Venice), and member of some PhD committees in foreign countries. She is editor of the journal “ACM Transactions on Computational Logic”. Her research interests are in the field of Theoretical Computer Science, in particular Formal Semantics of Programming Languages, Program Logics and Type Theories.

1. RONCHI DELLA ROCCA S., ROVERSI L. (2001). Intersection Logic. LNCS. vol. 2142, pp. 414-429.
2. RONCHI DELLA ROCCA S. (2000). Operational Semantics and Extensionality. Principles of Declarative Programming Languages (PPDP'00). (pp. 24-31).
3. KFOURY A., RONCHI DELLA ROCCA S., TIURYN J., URZYCZYN P. (1999). Alpha-conversion and Typability. INFORMATION AND COMPUTATION. vol. 150, pp. 1 -- 21.
4. PAOLINI L., RONCHI DELLA ROCCA S. (1999). Call-by-value Solvability. THEORETICAL INFORMATICS AND APPLICATIONS. vol. 33, pp. 507 -- 534.
5. PRAVATO A., RONCHI DELLA ROCCA S., ROVERSI L. (1999). The call-by-value lambda calculus: a semantic investigation. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE. vol. 9(5), pp. 617 -- 650.

Nº	Responsabile scientifico	Qualifica	Settore disc.	Università	Dipart./Istituto	Mesi uomo
1.	ABRUSCI VITO MICHELE	Prof. ordinario	M-FIL/02	ROMA TRE	FILOSOFIA	119
2.	MARTINI SIMONE	Prof. ordinario	INF/01	UDINE	MATEMATICA E INFORMATICA	84
3.	MASINI ANDREA	Prof. ordinario	INF/01	VERONA	INFORMATICA	65
4.	RONCHI DELLA ROCCA SIMONETTA	Prof. ordinario	INF/01	TORINO	INFORMATICA	56

Testo italiano

Questo progetto intende proseguire lo sviluppo di promettenti filoni di ricerca fondazionale e applicativa, nell'ambito dell'informatica teorica, scaturiti dall'introduzione della Logica Lineare (LL). E' infatti ormai largamente riconosciuto che la logica e' uno degli strumenti teorici principali dell'Informatica, e LL ha aperto nuove strade in questa direzione, in parte gia' largamente esplorate.
La definizione di LL ha insegnato che concetti logici, ritenuti atomici, in realta` non lo sono. La proprieta' essenziale di LL e' la decomposizione dell'implicazione intuizionista A=>B come !A-oB. Un'implicazione A-oB rappresenta una trasformazione che, preso UN oggetto della classe A, ne fornisce UNO nella classe B. La modalita' ! denota un processo distinto dalla trasformazione lineare di A in B; essa evidenzia proprieta' intensionali dell'oggetto in A da trasformare che descrivono la possibilita' di essere replicato o ignorato durante la trasformazione. LL quindi mette a disposizione operatori primitivi per le
azioni di duplicazione e cancellazione, che nell'approccio standard sono presenti essere sfruttati per controllare il modo in cui le dimostrazioni sono costruite ed eseguite (cioe' normalizzate). Sfruttando la ben nota relazione tra dimostrazioni logiche e linguaggi funzionali, formalizzata nel cosidetto "morfismo di Curry-Howard", grazie a LL possiamo definire una funzione calcolabile come composizione di una operazione di duplicazione/cancellazione seguita da una funzione lineare. Un altro esempio e' la modalita' § della Logica Lineare Leggera (LLL) che scompone ulteriormente l'operazione di duplicazione, permettendo quindi un controllo sul tempo di normalizzazione. Questa nuova visione permette quindi di modellare linguaggi di programmazione con un esplicito controllo delle risorse, sia in tempo che in spazio.
Inoltre LL ha introdotto un nuovo approccio alla teoria della dimostrazione, con la nozione di "proof-net" (rete di prova). Le reti di prova sono dimostrazioni (programmi, via la corrispondenza di Curry-Howard) caratterizzate mediante pure proprieta' geometriche (i "criteri di correttezza"). Esse sono uno strumento essenziale per raffinare il sistema logico, per studiarne gli aspetti dinamici (la normalizzazione delle prove) e per caratterizzare frammenti con proprieta' computazionali notevoli (come la logica lineare polarizzata o i sistemi a bassa complessita'). Si sono studiate notazioni di reti di prova che permettono la
definizione di procedure di normalizzazione delle prove basate su operazioni locali, che abilitano una duplicazione incrementale. Il risvolto applicativo di queste proprieta' e' la realizzazione di interpreti con strategie di riduzione ottimali per linguaggi funzionali.
LL ha fornito anche nuovi strumenti per studiare la semantica della computazione: gli spazi coerenti, domini funzionali alternativi ai classici domini alla Scott per studiare la semantica denotazionale, e la "semantica a giochi", che e' una sintesi dei due approcci classici alla semantica, quello operazionale e quello denotazionale, e che ha interessanti applicazioni nella costruzione di modelli fully abstract.
Figlia recente di LL e' la ludica, che si puo' sintetizzare come un nuovo approccio allo studio delle regole della logica basato su una rivisitazione della nozione di gioco, la cui caratteristica e' la localizzazione fisica delle formule/risorse. Questo studio sembra condurre al superamento della distinzione classica tra sintassi e semantica, ed e' interessante esplorare le sue possibili connessioni con l'Informatica.
In conclusione LL ha rivoluzionato i rapporti classici tra teoria della dimostrazione e teoria della computazione: in questo contesto il presente progetto di ricerca si propone di studiare LL in se', come soggetto di ricerca, ma anche di definire a partire da essa nuovi strumenti per lo sviluppo dell'informatica teorica, in particolare nello studio di linguaggi di programmazione.
Il progetto si sviluppera' secondo tre filoni:
1) Teoria strutturale della dimostrazione;
2) Studio di computazioni con complessita' predefinita;
3) Semantica della dimostrazione e dei linguaggi di programmazione.
Il primo filone e` di impronta nettamente fondazionale. Oltre ad affrontare problemi inerentemente connessi con la teoria della dimostrazione di LL, esso si pone l'obiettivo di estendere l'approccio di LL, importandolo, ad esempio, nell'ambito della teoria della dimostrazione della logica classica.
Il secondo filone vuole in particolare studiare logiche derivate da LL che caratterizzino computazioni di complessita' predefinita, e i loro legami con i linguaggi di programmazione.
Il terzo vuole approfondire l'aspetto semantico, e si propone sia di modellare il significato delle logiche (in particolare delle reti di prova) sia di usare strumenti ricavati da LL (come la teoria dei giochi o gli spazi coerenti) per studiare la semantica formale di linguaggi di programmazione paradigmatici.

Testo inglese

The aim of this project is to further develop promising research arguments both foundational and applicative, all arising from Linear Logic (LL), inside the field of Theoretical Computer Science. Indeed it is a common opinion that logic is one of the most important theoretical tools in Computer Science, and LL opened new lines in this direction, some partially explored. We learned from the definition of LL that some logical connectives, which were considered atomic, are composite. In fact the essential property of LL is the decomposition of the intuitionistic implication A=>B in !A-oB. A linear implication A-oB represents a transformation process, that, taken as input ONE object belonging to A, gives as output ONE object belonging to B. The modality ! denotes a different process, which gives explicit evidence to intensional properties of the object A to be transformed. These properties describe the potentiality of the object to be either duplicated or deleted during the transformation. So LL supports primitive operators for duplication and erasure, which are only present at a meta-level in the standard approach. Such operators can be used to control how the proofs are built and executed (i.e., normalized). Through the well known connection between logical proofs and functional languages, formalized in the so-called "Curry-Howard morphism", LL allows to define a computable function as composition of a duplication/erasure operation followed by a linear function. Another example is the modality § of the Light Linear Logic (LLL), which further decomposes the duplication operation, so allowing to control the normalization time. This new view-point allows to model programming languages with an explicit resources control, both in space and time. Moreover LL introduced a new approach to proof theory, through the notion of "proof-net". Proof-nets are proofs (programs, via Curry-Howard correspondence) characterized by pure geometrical properties (the "correctness criteria"). They are an essential tool for refining the logical system, for studying its dynamic aspects (proofs normalization) and for characterizing fragment of the system with particular computational properties (like the polarized linear logic or the low complexity systems). Particular notations for proof-nets have been studied, which allow to define normalization procedures based on local operations, making incremental duplications. An interesting application of these properties is the design of interpreters for functional languages using optimal reduction strategies. LL gave new tools for studying the semantics of computations: coherence spaces, functional domains more refined than the previous Scott domains, for studying the denotational semantics, and the "game semantics", which is a synthesis of the two classical approaches to semantics, the operational and the denotational one. Game semantics can be fruitfully used for building fully abstract models.
Recently from LL Ludics sprouted. In a very synthetic way, Ludics can be described as a new approach to the study of logical rules, based on a revised notion of game, whose main characteristic is the physical localization of formulas/resources. It seems to open a new scenario, when the classical distinction between syntax and semantics aims to disappear. It is interesting to explore its possible applications to Computer Science. In conclusion LL turned the classical relationships between proof theory and computation theory: in this context the present research project want both to study LL in itself and to start from LL to design new tools for the development of Theoretical Computer Science, in particular in the field of Programming Languages. The project will be organized into three lines:
1) Structural proof theory
2) Study of computations of fixed complexity
3) Semantics of both proofs and programming languages.
The first line is clearly foundational. Along it we want both to study problems related to the proof theory of LL, and to export proof theory techniques from LL to other systems (for example, classical logic). Along the second line, we want in particular to study logics derived from LL, with the property of characterizing computations of given complexity, and to explore their possible applications to programming languages. Along the third line, we want to deal with semantics. In particular we want both to model the meaning of logical systems (in particular of proof-nets) and to use tools from LL (e.g. game theory or coherence spaces) for studying the formal semantics of programming languages.

Testo italiano

A partire dalla sua nascita [Gir87], la Logica Lineare (LL) ha acquisito una rilevanza via via crescente nel campo delle applicazioni della logica all'informatica, come puo' essere facilmente osservato guardando ai programmi delle recenti maggiori conferenze internazionali del settore (la bibliografia corrente sulla LL comprende oltre 500 pubblicazioni di rilievo). Qui daremo quindi solo una rapida rassegna di questi contributi e delle principali influenze che la LL ha avuto sui recenti sviluppi dell'informatica, enfatizzando in modo particolare il contributo dei ricercatori italiani.Per motivi di chiarezza espositiva, classificheremo questi contributi nei tre filoni in cui vogliamo organizzare il nostro lavoro di ricerca.
1) TEORIA STRUTTURALE DELLA DIMOSTRAZIONE
LL ha introdotto un nuovo e potente strumento per l'analisi strutturale della dimostrazione: le "proof-nets" (reti di prova). Definite inizialmente in [Gir87], le reti di prova forniscono una descrizione grafica delle prove, finalizzata a catturare la loro essenza in contrasto con la ridondanza e gli inutili dettagli sintattici della formulazione a sequenti. Dal punto di vista sintattico le reti di prova sono (iper)grafi liberamente generati tramite regole logiche locali e verificanti un opportuno criterio geometrico di correttezza [Gir87] [DR89] [GM01][Gue99]. Esse sono strumenti raffinati per studiare gli aspetti dinamici delle prove (la normalizzazione, o eliminazione dei tagli) e hanno utili applicazioni nell'analisi operazionale dei linguaggi funzionali di programmazione. In particolare, [GAL92] mostra che la riduzione ottimale dei lambda-termini secondo Levy-Lamping [Lev78, Lam90] puo' essere interpretata come eliminazione dei tagli in reti di prova "senza box". In queste strutture, la nozione "globale" di box e' rimpiazzata da informazioni "locali" (nodi aggiuntivi della rete) che esprimono informazioni sia relativamente alla condivisione che al suo corretto mantenimento: varianti di applicazioni di questa tecnica sono in [GMM01,AG98]. La nozione di riduzione ottimale e' stata discussa e rivisitata in [AM98] e [ACM00], dove vengono suggerite misure per una effettiva valutazione della sua complessita'.Sono stati introdotti raffinamenti del concetto di rete di prova per varianti di LL, tra cui la logica non commutativa. La logica non commutativa [AR00],[Mai01] e' un raffinamento della logica lineare dove la commutativita' non e' presupposta (come esplicita o implicita regola strutturale) e connettivi moltiplicativi commutativi coesistono con quelli non commutativi. La logica non commutativa ha notevoli applicazioni in linguistica ed e' stata inoltre utilizzata da Ruet per dare semantica a linguaggi di programmazione concorrenti con vincoli.
Le reti di prova, per il loro carattere modulare, hanno inoltre permesso di avviare uno studio matematico del concetto di "modulo di dimostrazione" [DR89], [Gir88].Proprio questa caratteristica delle reti di prova, e la scoperta di due proprieta' fondamentali quali la polarizzazione e la focalizzazione ([AM99],[Gir91]) sono alla base anche della ludica di Girard [Gir01, Cur]. La ludica e' un soggetto in piena evoluzione, basato su una rivisitazione della nozione di gioco, la cui caratteristica e' la localizzazione fisica delle formule/risorse. Uno degli aspetti piu' innovativi della ludica e' l'eliminazione della dicotomia sintassi/semantica, attraverso la definizione di sistemi formali
internamente completi. Ad esempio, se lo scopo e' studiare le proprieta' computazionali di un sistema, tali proprieta' devono risultare da una rilettura della nozione interna di computazione, e non aggiungendo informazioni ad hoc, di natura meta-teoretica.
Infine, nell'ottica di estendere gli strumenti introdotti per LL anche ad altri contesti logici, particolare importanza assume la rivisitazione del problema della normalizzazione forte e della confluenza per la logica classica (LK). La vasta letteratura sull'argomento (citiamo qui per ragioni di spazio solo [Gir91]
condivide il presupposto che il fallimento di queste proprieta` in LK e` dovuto ad una mancanza di informazione (piu` precisamente, di focalizzazione) che si puo` fornire direttamente oppure attraverso traduzioni in logica intuizionistica o lineare: tentativi in questo senso per frammenti di LK sono in [Bela], [BW95].
I metodi di analisi delle prove introdotti per LL possono essere usati per modellare comportamenti che non rientrano nelle logiche usuali. Ad esempio, in [RR01], viene proposto un connettivo logico con la stessa semantica della congiunzione dei tipi intersezione. Intuitivamente, il nuovo connettivo si colloca tra la usuale congiunzione intuizionista e la congiunzione tensoriale di LL.
2) STUDIO DI COMPUTAZIONI CON COMPLESSITA' PREDEFINITA
In [Gir98] Girard ha introdotto la Logica Lineare Leggera (LLL) che caratterizza la classe delle funzioni polinomiali (P), nel senso ogni funzione in P e' rappresentabile in LLL, e, viceversa, ogni dimostrazione in LLL che sia una codifica di una funzione in P e' normalizzabile in tempo polinomiale.
LLL e suoi raffinamenti, come la Logica Leggera Affine (LAL) [Asp98] [AR02] e la Logica Lineare Soft [Laf01] permettono una descrizione composizionale di P, astraendo da definizioni legate a modelli computazionali, come le macchine di Turing.Seguendo le stesse linee, si sono caratterizzate le computazioni elementari con la Logica Lineare Elementare (ELL) ([Gir98,DJ99]) e con la sua versione affine (EAL) [CM01]. Su proprieta' di EAL si e' basata l'analisi di complessita' in [ACM00], citata nel filone precedente. A conferma della solidita' di questo approccio, in [BP01] si caratterizza la classe delle funzioni elementari sfruttando la geometria delle interazioni, che e' una semantica algebrica delle prove.Queste logiche caratterizzanti complessita' limitate possono essere utilizzate per estrarre strategie di valutazione in linguaggi di programmazione paradigmatici. In [Rov00] viene proposta una sintassi concreta per LAL, tipabile automaticamente con formule di LAL, polimorfe alla ML. In [CM01] e' presentato un algoritmo di inferenza di tipo per i termini del lambda-calcolo, dove i tipi sono formule di EAL. La tecnica usata deriva in modo uniforme, data una dimostrazione intuizionista, tutte le possibili decorazioni in EAL. [CM01] fornisce anche un metodo alternativo a quello usato in [DJS95], per ottenere un'immersione (non uniforme) ottimale (nel numero di box) della logica intuizionista in LL.
Ulteriori risultati preliminari e non ancora pubblicati in questo campo sono stati ottenuti da Coppola e Ronchi (per EAL) e Baillot (per LAL).
3) SEMANTICA DELLA DIMOSTRAZIONE E DEI LINGUAGGI DI PROGRAMMAZIONE
L'introduzione di LL ha rinnovato anche la ricerca sulla semantica della dimostrazione e dei linguaggi di programmazione, suggerendo nuovi strumenti e nuovi punti di vista per ridurre l'analisi di proprieta' computazionali e strutturali allo studio di propriet*Ý matematiche astratte. Da un lato, per ciascuna prova di LL, sia essa espressa come rete di prova, o come derivazione in un calcolo dei sequenti, esiste una funzione lineare tra spazi coerenti [Gir87] che la rappresenta e che e' invariante rispetto alla normalizzazione, e che quindi ne puo' costituire una semantica. Girard mostra come si possa "calcolare" la semantica di una dimostrazione. In [TdF01b] si dimostra che la semantica coerente e' "iniettiva" (cioe' la nozione di equivalenza definita sulle reti di prova dal processo di eliminazione del taglio e quella definita dalla semantica coerente coincidono) per alcuni frammenti significativi di LL, ma non e` iniettiva in generale. La nozione di iniettivita' e' chiaramente corrispondente alla nozione di modello fully-abstract per i linguaggi di programmazione.
I risultati positivi presenti in [TdF01b] vengono utilizzati nel lavoro [OTdF01] per introdurre una nuova sintassi per il frammento polarizzato della LL (con gli additivi).
Gli spazi coerenti, che raffinano domini alla Scott, sono uno spazio interessante per dare la semantica denotazionale di lambda-calcoli. Essi infatti hanno permesso di distinguere diversi tipi di non terminazione, in linguaggi lazy, risultato non ottenibile con i domini alla Scott che, invece, eguagliano ogni comportamento computazionale che non produce risultati [BPR98] . Inoltre, astraendo dalla struttura degli spazi coerenti necessaria a modellare il lambda calcolo per valore, e sfruttando la definizione di modello categoriale di LL [Bie98], in [PRR99] si e' elaborata una definizione di modello categoriale per questa variante del lambda calcolo.Dall'altro lato, la presenza del connettivo "negazione involutiva", scaturito anch'esso dall'analisi dell'implicazione intuizionista, ha suggerito l'analisi dei processi di computazione come un gioco di domande e risposte tra le componenti i processi stessi. Ne e' nata la "semantica a giochi" (game semantics)[AJM00]. Con essa sono stati definiti modelli fully abstract di PCF, di linguaggi sequenziali e di LL. Una metodologia alternativa alla semantica a giochi che, pero', ne condivide gli obiettivi, e' la
recente Realizzabilita' Lineare [AL00]. Essa permette di costruire modelli di Partial Equivalence Relations (PER) su algebre combinatorie lineari. In [AL00] e` stato definito un modello di PER fully complete per il frammento del sistema F corrispondente ai tipi di ML. Come gli spazi coerenti, la semantica a giochi ha permesso di ottenere modelli di diverse strategie di riduzione sul lambda calcolo. In [DFH99] si dimostra che nella categoria dei giochi tutti gli oggetti riflessivi, vale a dire tutti i lambda-modelli estensionali, hanno la stessa teoria, e in [DF00] si dimostra che ci sono solo due lambda-teorie possibili indotte da modelli non-estensionali, da cui si deduce che sfruttando i giochi si
possono ottenere modelli fully-abstract solo per strategie di testa su lambda-modelli puri. Infine, [Dig01,OD02], definendo una nuova categoria di modelli basati sui giochi, costruiscono due modelli fully-abstract ed universali per il lambda calcolo con una strategia di riduzione lazy.

Testo inglese

Since its introduction in [Gir87], the relevance of Linear Logic (LL) in the field of the applications of the Logic to the Computer Science has continuously grown, as witnessed by the programmes of the most recent and major international conferences of the filed (the actual bibliography on LL amounts to more than 500 titles.) This introduction is a quick overview of these contributions and of the relevance that linear logic has had on the most recent developments of the Computer Science, mainly emphasizing the contributions by the italian researchers.
For a better exposition, these contributions will be grouped into three research mainstream, under which we shall organize our research activity, relative to this project.
1) STRUCTURAL PROOF THEORY
LL introduced the proof-nets, a new and very expressive tool for the structural analysis of the formal derivations. The proof-nets were defined in [Gir87]. They supply a graphical description of a formal derivation, the goal being to catch their structural essence, while avoiding the irrelevant syntactical details of a sequent calculus formulation. The proof-nets are (iper)graphs; they are freely generated by local logical rules that satisfy a correctness criterion, expressed in terms a geometrical constraints [Gir87] [DR89] [GM01] [Gue99]. The proof-nets become a tool to study the dynamical properties of a logical derivation (their normalization, or cut elimination) and can be fruitfully used for the operational analysis of the functional programming languages. In particular, [GAL92] shows that the optimal-reduction of the lambda-terms a' la Levy-Lamping [Lev78, Lam90] can be interpreted by means of the cut elimination in proof-nets "without boxes". In these structures, the usual "global" notion of box is replaced by some local information on the net (new nodes) that keep recording how the structure of a net is shared and how this sharing must be preserved; variants are in [GMM01,AG98]. [AM98] e [ACM00] discuss and revisit the notion of optimal reduction, suggesting measures to effectively asses its complexity. Refinements of the proof-nets for variants of LL exist. Among these variants there is Non Commutative Logic [AR00],[Mai01]; it refines LL in a way that the commutativity is inherently inside the system (neither implicit, nor explicit rule introduces it in the system) and the commutative multiplicative connectives coexist with the non commutative ones. Non Commutative Logic has notable applications inside Linguistics, and was used by Ruet as a semantics for constrained logic programming. Moreover, the modular nature of the proof-nets allow to mathematically study the notion of "proof-module" [DR89], [Gir88]. Precisely their modular structure, and the basic properties called "polarization" and "focalization" ([AM99],[Gir91]) led Girard to the definition of the Ludics [Gir01,Cur]. Ludics, a subject not in its final form, is funded on an alternative notion of game, whose main notion is the localization of the formulas/resources. The main innovative aspect of Ludics is its ability to get rid of the dichotomy syntax/semantics, thank to the definition of systems which are intrinsically complete. For example, if the goal is to study the computational properties of some system, such properties must be obtained by reading the internal notion of computation,, and must not result from adding ad hoc and meta-theoretical information. Finally, LL can be used in other contexts and it has a major role to cope with the problem of the strong normalizability and of the confluence of the Classical Logic (LK). The rich literature (we cite just [Gir91], for lake of space) share the idea that the failure of these properties on LK lies in the lack of information (read focalization). The lacking information can be supplied explicitly, or by embedding LK into Intuitionistic Logic or LL: [Bela], [BW95] work in these directions. The analysis methods of the formal derivations, introduced with LL, can be used to model "unusual" logical behaviors. For example, [RR01] defines a logical connective with the same semantics as the conjunction of the intersection types. Intuitively, the new connective falls in between the usual intuitionistic conjunction and the tensor product of LL.
2) STUDY OF THE COMPUTATIONS WITH A GIVEN COMPLEXITY
In [Gir98] Girard introduces Light Linear Logic (LLL), that characterizes the class of the polynomial functions (P); this means that every function of P can be represented in LLL, and, vice versa, that every derivation of LLL that encodes a function of P can be normalized in polynomial time. LLL and all its refinements, like Light Affine Logic (LAL) [Asp98] [AR02] and Soft Linear Logic [Laf01] allow a compositional description of P, abstracting away from definitions of P dependent from computational models, like the Turing machines. Under the same principles, there are characterizations of the elementary functions by means of Elementary Linear Logic (ELL) ([Gir98,DJ99]) and by its affine version (EAL) [CM01]. The analysis of the complexity of the optimal reductions in [ACM00], cited in the first research mainstream, exploits EAL. The strength of this approach is further witnessed by [BP01], where the elementary functions are characterized exploiting the geometry of interaction, an algebraic semantics of the proof-nets. The logics that allow to characterize a given complexity class can be used to find good evaluation strategies on paradigmatic programming languages. [Rov00] introduce a concrete syntax of LAL. It has a decidable polymorphic type inference a` la ML, that uses the formulas of LAL as types. [CM01] defines a type inference algorithm for the lambda-terms, such that the types are the formulas of EAL: given an intuitionistic derivation the technique uniformly derives all its possible EAL decorations. Methodologically, [CM01] is an alternative to [DJS95] to obtain a (non uniform) optimal (in the number of placed boxes) embedding of intuitionistic logic into LL. Further preliminary results on this subject have recently been obtained by Coppola and Ronchi (relatively to EAL) and Baillot (on LAL).
3) SEMANTICS OF THE FORMAL DERIVATION AND OF THE PROGRAMMING LANGUAGES
The introduction of LL renewed also the research on the semantics of the formal derivation and of the programming languages, suggesting new tools and perspectives to reduce the analysis of computational and structural properties to the study of abstract mathematical properties. On one side, for every derivation in LL, independently from its representation, there exists a linear function that maps a coherence spaces to a coherence spaces [Gir87], which represents it. This function is an invariant with respect to the normalization, so it can be taken as the semantics of the derivation. Girard shows how to "calculate" the semantics of a derivation. [TdF01b] proves that the semantics of some interesting fragments of LL, built on the coherent spaces is "injective" (the equivalence on the derivations, induced by the normalization, and the equivalence on the interpretation in the coherence spaces coincides). In general, however, injectivity does not hold for full LL. Notably, "injective" is the logical counterpart of "fully-abstract" in the context of the programming languages. The positive results in [TdF01b] are used in [OTdF01] to introduce a new syntax for the polarized fragment of LL (with additives.) The coherence spaces, that refine the Scott domain, are interesting structures to define a semantics for the lambda-calculi. The coherence spaces allowed to distinguish between different kinds of non termination of lazy languages. This kind of analysis cannot be achieved with the Scott domains for which all kinds of non termination are indistinguishable [BPR98]. Moreover, abstracting away from the structure of the coherence spaces, required to model the call-by-value lambda calculus, and exploiting the definition of categorical model for LL [Bie98], [PRR99] introduces a notion of categorical model for this variant of the usual lambda calculus. Moreover, the "involutive negation", a connective obtained by the initial analysis of the intuitionistic implication, suggests to look at the computation as it was a question-answer game, between the components of the processes. The game semantics is the result of this new perspective [AJM00]. The game semantics allows to define fully abstract models for PCF, for sequential languages and for LL. A methodological alternative to game semantics, for defining models, is Linear Realizability [AL00]. It allows to build models of Partial Equivalence Relations (PER) on linear combinatory algebras. A fully complete PER model for the fragment of system F that corresponds to ML type system is in [AL00]. Like coherence spaces, the game semantics models various reduction strategies on the lambda calculus. [DFH99] proves that the reflexive objects, namely the extensional lambda models, in the category of games all have the same theory. Moreover, [DF00] shows that only two lambda theories are induced by non-extensional models. This means that the game semantics can yield fully abstract models only for head reduction strategies on pure lambda models. Finally, [Dig01,OD02] build two fully abstract and universal models for a lazy lambda calculus. The result is obtained by defining a new category of game models.

[Abr02] S. Abramsky, "A Structural Approach to Reversible Computation", POPL 2002.
[AL00] S. Abramsky, M. Lenisa "A Fully-complete PER Model for ML Polymorphic Types", CSL'2000, P. Clote, H.Schwichtenberg eds., Springer LNCS vol. 1862, 2000, pp. 140-155.
[AL01] Abramsky S., M. Lenisa. "Fully Complete Minimal PER Models for the Simply Typed Lambda-calculus", CSL'2001, LNCS 2142, 2001, pp. 443-457.
[AJM00] Abramsky S., Malacaria P., Jagadeesan R., Full Abstraction for PCF. Inf. and Comp. 163, 2000, 409—470 (extended abstract in LNCS 789, pp 1ff, 1994).
[Abr91] V. Michele Abrusci. "Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic." J. Symbolic Logic, 56(4):1403-1451, 1991.
[AR00] V. Michele Abrusci and Paul Ruet. Non-commutative logic. I. The multiplicative fragment. Ann. Pure Appl. Logic, 101(1):29-64, 2000.
[And92] Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. Logic Comput., 2(3):297-347, 1992.
[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.
[Asp98] A. Asperti. "Light Affine Logic". Proc. of IEEE Symp. on Logic in Computer Science (LICS’98), IEEE, 1998.
[ACM00]Asperti A., Coppola P., Martini S., (Optimal) duplication is not elementary recursive. ACM Principles of Programming Languages POPL2000, pp. 96-107, 2000.
[AG98] Asperti, A. and Guerrini, S., "Optimal Implementation of Functional Programming Languages", Cambridge University Press, 1998.
[AM98] Asperti A., Mairson H., Parallel beta reduction is not elementary recursive Conference Record of POPL '98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 303-315, 19-21 January 1998.
[AR02] Asperti, A. and Roversi, L. "Intuitionistic Light Affine Logic". ACM Transactions on Computational Logic, 3(1), ACM, 2002, pp.137-175
[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).
[BPR98] Bastonero O., Pravato A. and Ronchi Della Rocca S. "Structures for lazy semantics". Programming Concepts and Methods, Gries and de Roever ed.s, Chaptman and Hall , 1998, pp. 30-48.
[Bela] Bellin G. (to appear). Two paradigms of logical computation in Affine Logic?. in Logic for Concurrency and
Synchronization. R. de Queiroz (ed.). Trends in Logic. Kluwer.
[BW95] Bellin G., Van De Wiele J. (1995). Subnets of Proof-nets in MLL-. in Advances in Linear Logic, J.-Y. Girard, Y. Lafont. L. Regnier (Eds.). number 222 of the London Mathematical Society Lecture Note Series. Cambridge University
Press. pp.249-270.
[Bie95] Bierman, G. "What is a Categorical Model of Intuitionistic Linear Logic?", Proceedings of Typed Lambda Calculus and Applications (TLCA95), LNCS 902, , Springer-Verlag, pp. 78-93.
[BE91] Bucciarelli A., Ehrhard T. "Sequentiality and strong stability",LICS’91, IEEE Computer Society Press, 1991, pp. 138-145.
[CM01] Coppola P. and Martini S. Typing lambda terms in elementary logic with linear constraints, in TLCA01, LNCS 2044, pp. 76-90, Springer, 2001.
[Cur] Curien, P.-L. "Introduction to Ludics". Available at http://www.pps.jussieu.fr/~curien
[DJS95] Danos V., Joinet J-B, and Schellinx H. On the linear decoration of intuitionistic derivations. In Archive for Mathematical Logic, volume 33, pages 387-412, 1995.
[DJ99] V. Danos and J.-B. Joinet,"Linear Logic & Elementary Time", 1st international workshop on Implicit Computational Complexity (ICC'99)
Santa Barbara (California), 1999
[DR89] Vincent Danos and Laurent Regnier. The structure of multiplicatives. Arch. Math. Logic, 28(3), 1989.
[Dig01] Di Gianantonio, P. Game Semantics for the Pure Lazy Lambda-calculus. In TLCA '01, LNCS 2044, pp 106-120, Springer-Verlag, 2001.
[DF00] Di Gianantonio, P and G. Franco. The fine structure of game lambda-models. In FSTTS '00, LNCS 1974, pp. 429-441, Springer-Verlag, 2000.
[DFH99] Pietro Di Gianantonio, Gianluca Franco, and Furio Honsell, Game semantic for untyped lambda calculus. Proc. of the conference Typed Lambda Calculus and Applications 99, LNCS 1591, pp. 114-128, Springer- Verlag.
[Gir87] Jean-Yves Girard. Linear logic. Theoret. Comput. Sci., 50:1-101, 1987.
[Gir88] Jean-Yves Girard. Multiplicatives. Universita' 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.
[Gir95] Girard J.-Y. "Linear logic: its syntax and semantics", Advances in Linear Logic, J.-Y. Girard, Y. Lafont and L. Regniered.s, Cambridge University Press, 1995, pp. 1 - 42
[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. Information and Computation, 204(2):143-175, 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.
[GLT89] Girard, J.-Y., Lafont, Y. and Tailor, P. "Proofs and Types". Cambridge University Press, 1989.
[GAL92] Gonthier G., Abadi M., L'evy J-J, Linear logic without boxes, 7th LICS, 223-234, IEEE Press, 1992.
[GUE99] Guerrini S. (1999). Correctness of multiplicative proof nets is linear. In Proceedings of 14th Annual Symposium on Logic in Computer Science (LICS '99). Trento. Italy. IEEE pp.454-463
[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).
[Laf01] Y. Lafont. Soft Linear Logic and Polynomial Time. To appear in Theoretical Computer Science.
[Lam90] Lamping J., An algorithm for optimal lambda-calculus reduction, 17th ACM POPL, 16-30, ACM Press, 1990.
[Lev78] L'evy J.-J., Reductions correctes et optimales dans le lambda-calcul, PhD thesis, Univ. Paris VII, 1978.
[Mai01] Roberto Maieli. A new correctness criterion for multiplicative non commutative proof-nets. Preprint Institut de Mathematiques de Luminy, n.13, 2001. To appear in Archive for Mathematical Logic.
[MM97] S. Martini, and A. Masini (1997). Experiments in Linear Natural Deduction. theoretical computer science. vol. 176, pp. 159-173.
[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.
[OD02] L. Ong and Di Gianantonio Pietro. Games characterizing Levy-Longo trees. In ICALP '02, LNCS, to appear, Sprinter-Verlag, 2002.
[PRR99] Pravato A., Ronchi Della Rocca S., Roversi L. "The call-by-value lambda calculus: a semantic investigation", Mathematical Structures in Computer Science, 9, 5, (1999), pp. 617-650.
[RR01] S. Ronchi Della Rocca and Roversi L. "Intersection logic", CSL'01, LNCS 2412, Springer-Verlag, 2001, pp. 414-428.
[Rov99] L. Roversi. "A P-Time Completeness Proof for Light Logics", CSL'99, LNCS 1683, 1999, Springer-Verlag pp. 469 -- 483.
[Rov00] Roversi, L. " Light affine logic as a programming language: a first contribution". International Journal of Foundations of Computer Science, , 2000, 11(1), pp.113 -- 152.
[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.

Fase 1

Durata:	18 mesi		Costo previsto:	121.000 Euro

Descrizione:

Testo italiano

La Logica Lineare non e' solo un potente strumento tecnico ma anche, e forse prioritariamente, una sorgente di importanti metodologie di ricerca. Per questa ragione, l'originalita' del nostro progetto e', innanzi tutto, nella metodologia che intendiamo adottare: il nostro obiettivo e' quello di utilizzare la logica lineare come un tema federativo, particolarmente adatto a raccogliere le conoscenze e le esperienze di tutti quei ricercatori italiani che si sono imbattuti in essa nella loro pratica scientifica. Tecnicamente, cio' che attendiamo da una tale sinergia e' una piu' profonda conoscenza di vari problemi fondamentali dell'Informatica e una visione piu' chiara ed unitaria dei nostri settori di ricerca. In conseguenza di questo, nonche' per il fatto che la nostra ricerca e' incentrata su problematiche di base e a lungo termine, e' estremamente difficile articolare il progetto in una rigida struttura sequenziale. Dunque, il progetto sara' sostanzialmente organizzato in una unica fase "di ricerca" di 18 mesi, seguita da una fase finale "consuntiva" di 6 mesi. La fase di ricerca sara' organizzata nei tre filoni gia' definiti in precedenza, che sono a loro volta suddivisi in task piu' specifici, alcuni dei quali possono a loro volta presentare una ulteriore suddivisione in sotto-task che definiscono problematiche puntuali. Ci sembra qui importante evidenziare due fatti. Innanzitutto tutte le sedi coinvolte nel progetto sono impegnate in tutti e tre i filoni, a dimostrazione di una effettiva collaborazione. Inoltre, i task non sono indipendenti, e a volte problematiche simili possono comparire in piu' di un task, anche in filoni diversi: in effetti i problemi possono essere studiati da piu' punti di vista, e proprio da questa ottica multipla ci aspettiamo risultati interessanti. Ogni filone sara' seguito da un coordinatore, che avra' il compito di monitorare il lavoro svolto, e stimolare incontri, discussioni e cooperazioni sui vari problemi. I filoni e i task in cui questi sono suddivisi sono i seguenti:
Filone 1: TEORIA STRUTTURALE DELLA DIMOSTRAZIONE
Task 1.1: Reti di prova
Task 1.2: Ludica
Filone 2: STUDIO DI COMPUTAZIONI CON COMPLESSITA' PREDEFINITA
Task 2.1: Caratterizzazione logica di computazioni con complessita' limitata
Task 2.2: Controllo del tempo di esecuzione tramite assegnazioni di tipo
Task 2.3: Riduzioni ottimali
Filone 3: SEMANTICA DELLA COMPUTAZIONE E DEI LINGUAGGI DI PROGRAMMAZIONE
Task 3.1: Semantica delle dimostrazioni
Task 3.2: Semantica dei linguaggi di programmazione

Testo inglese

Linear Logic is not just a powerful tool; it is rather a source of methodological research issues. Therefore our central concern is methodological in nature: we plan to use linear logic as a leading theme connecting Italian researchers whose expertise and skill has profited of it. Technically we expect from such a synergy a deeper understanding of several fundamental issues in computer science as well as a clearer and more systematic grasping of each own research themes. Because of this a rigid structure does not seem appropriate to a variety of works in progress in basic research areas; rather we foresee a simpler organization into two phases: a first one of "search", lasting 18 months. Eventually a second one will follow drawing conclusions and lasting 6 months. The search phase will follow three main lines, as specified in advance, each one includes more specific tasks, possibly subdivided into subtasks concerning very specific problems. We stress here that all sites involved in the project are actually working on all of the search issues, which is clearly an advantage in view of cooperation. Moreover tasks may overlap in a fruitful way, namely by addressing the same problem from different perspectives: it is indeed from this multiple approach that more interesting results are expected. Each line of search will have a responsible leader, who will be charged of monitoring the running work, proposing meetings and favoring the exchange of knowledge and expertise among the participants. Research lines and tasks are as follows:
Line 1: STRUCTURAL PROOF THEORY
Task 1.1: Proof nets
Task 1.2: Ludics
Line 2: COMPUTATIONS OF BOUNDED COMPLEXITY
Task 2.1: Logical characterizations of computations of bounded complexity
Task 2.2: Controlling the running time via type assignment systems
Task 2.3: Optimal reduction
Line 3: SEMANTICS OF COMPUTATIONS AND PROGRAMMING LANGUAGES
Task 3.1: Proof semantics
Task 3.2: Semantics of programming languages

Risultati parziali attesi:

Testo italiano

Filone 1: TEORIA STRUTTURALE DELLA DIMOSTRAZIONE
La Logica Lineare e' stata introdotta da Girard come un raffinamento della logica classica e intuizionista, caratterizzata dall'enfasi sulle regole strutturali (indebolimento,scambio e contrazione), e dalla gestione dei contesti. Il punto di vista originale della logica lineare sulle operazioni strutturali ha molte importanti conseguenze nella teoria della dimostrazione, tra cui una migliore comprensione, da un punto di vista costruttivista, dei sistemi di logica "classica".
I nostri principali obiettivi in questo filone sono i seguenti:
1.1: Reti di prova
[unita' partecipanti: 1, 3, 4]
Come gia' evidenziato nei punti precedenti, lo strumento tecnico principale per lo studio di dimostrazioni, nell'ambito di LL, sono le reti di prova. Noi ci proponiamo di raffinare ulteriormente tale strumento, studiandone le proprieta' in differenti contesti.
In particolare, lavoreremo sui seguenti sotto-task:
1.1.1 Estensione e generalizzazione della nozione di rete di prova
Partendo dalle reti di prova e dai logical flow graphs (Buss, Carbone) ci si propone di studiare il ruolo di strutture generali per la rappresentazione di dimostrazioni (principalmente, ma non solo, nell'ambito della logica lineare). Lo scopo e' di ottenere un'analisi piu' fine degli aspetti funzionali (e non funzionali) della normalizzazione dei sistemi deduttivi, in particolare quelli "lineari".Una istanza particolare di questo problema e' lo studio delle proprieta` caratteristiche della normalizzazione delle prove in logica classica, che sono generalmente identificate nel non-determinismo e nel trattamento dell'irrilevanza e della focalizzazione. Si vogliono trovare formulazioni alternative delle reti di prova per studiare tale problema, anche allo scopo di contribuire alla difficile questione dell'identita` delle prove classiche. Un'ulteriore problema, che si puo' collegare a questo ambito, e' lo studio del paradigma di costruzione focalizzata delle prove. La focalizzazione e' stata originariamente introdotta da Andreoli [And92] in termini della descrizione a sequenti della logica lineare commutativa. Questo approccio, nonostante faccia ricorso a dimostrazioni bipolari astratte equipaggiate con sistemi di equazioni lineari (che desequenzializzano le prove), non puo' essere considerato soddisfacente. Una soluzione piu' interessante e naturale - proposta sempre da Andreoli nel convegno "Logic and Interaction"(Marsiglia,febbraio 2002)- sembra essere quella del ricorso alle reti di prova, o piu' in generale a strutture parziali (o moduli) e alla loro composizione. Ci si propone quindi di studiare qual'e' la nozione adeguata di rete di prova, che tenga conto delle proprieta' di focalizzazione e bipolarizzazione gia' riscontrate nel calcolo dei sequenti della logica lineare e della logica non commutativa. Su questa nuova definizione di rete di prova vogliamo poi definire un criterio di correttezza, che risulti equivalente a quello delle reti di prova standard ([DR89]) e di quelle non-commutative ([AR00,Mai01]) e che sia inoltre incrementale e modulare
1.1.2. 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 bilateralita' (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 di prova; c) investigare le relazioni tra i moduli e la ludica.
1.1.3 Contenuto computazionale della riduzione delle reti di prova della logica non-commutativa.
Intendiamo caratterizzare il contenuto computazionale della logica non-commutativa, mediante una analisi raffinata delle riduzioni.
1.2 Ludica.
[unita' partecipanti: 1, 4]
Le potenzialita' della ludica [Gir01,Cur] e le sue possibili applicazioni formano un campo di ricerca ancora in gran parte inesplorato. Ci proponiamo di studiare sia la ludica in se', sia il suo possibile uso per esplorare le proprieta' di sistemi logici complessi. Nell'ambito del primo obiettivo, vogliamo studiare nuovi connettivi suggeriti dalla Ludica , e in particolare vogliamo analizzare, mediante reti di prova, nuovi quantificatori che estendano quelli sinora definibili nella Logica Lineare. Nell'ambito del secondo obiettivo, vogliamo disegnare, a partire dalla ludica, un sistema logico che corrisponda all'assegnazione dei tipi intersezione, la cui soluzione parziale proposta in [RR01] non risulta ancora completamente soddisfacente.
Filone 2: STUDIO DI COMPUTAZIONI CON COMPLESSITA' PREDEFINITA
Aggiungendo degli opportuni vincoli alla logica lineare, si ottengono dei sottosistemi in cui tutte e solo le funzioni di una data complessita' possono essere programmate. Esempi sono LLL[Gir98] e i suoi raffinamenti LAL [Asp98, AR02] e la Logica Lineare Soft [Laf01], che caratterizzano le computazioni polinimiali, e EAL [Gir98,DJ99], che caratterizza le computazioni elementari. Questi risultati hanno un potenziale notevolissimo per applicazioni alla teoria dei linguaggi di programmazione.In questo filone il nostro lavoro si propone i seguenti obiettivi:
Task 2.1: Caratterizzazione logica di computazioni con complessita' limitata
[unita' partecipanti: 1, 2, 3, 4]
Si vuole innanzitutto studiare, da un punto di vista fondazionale, quali proprieta' deve possedere una logica per caratterizzare in modo soddisfacente una classe di complessita' computazionale. Data una classe di complessita' C, una logica L(C) che la caratterizzi, nell'ottica in cui ci poniamo, deve possedere due caratteristiche fondamentali. In primo luogo la procedura di normalizzazione di L(C) deve avere intrinsecamente complessita' C. In secondo luogo L(C) deve indurre la descrizione astratta della classe di complessita' C. Solo l'esistenza di tutte e due queste proprieta' ci garantisce una descrizione incrementale dell classe C, che sia 'machine independent', ma che nello stesso tempo definisca una precisa nozione dinamica di computazione. Da questo punto di vista le formulazioni attuali sia di LAL che di EAL non sono ancora completamente soddisfacenti, ed e' nostra intenzione cercare raffinamenti che soddisfino le proprieta' sopra esposte. Vogliamo poi definire altri sistemi logici ispirati a LL che modellino altre classi di complessita'.Un problema particolare che vogliamo studiare in questo ambito e' la possibilita' di introdurre nuovi connettivi per rappresentare costrutti non deterministici, con l'obiettivo di arrivare ad una buona formulazione logica di classi di complessita' nondeterministiche (in prima istanza NP). Un secondo, e susseguente, obiettivo in questo task e' quello di partire da una logica caratterizzante computazioni di data complessita' per disegnare linguaggi di programmazione paradigmatici in cui esprimere a priori solo computazioni eseguibili in tempo corrispondente. Il procedimento di passaggio dalla logica al linguaggio non sempre puo' essere basato sulla mera applicazione del morfismo di Curry-Howard: infatti tale morfismo in genere crea linguaggi con costrutti intrinsecamente complessi, e quindi difficili da usare in maniera diretta (vedi EAL [CM01]). Invece la logica puo` costituire un framework in cui studiare strategie di programmazione che suggeriscano primitive per un linguaggio, che non solo permetta di esprimere solo computazioni della complessita' voluta, ma abbia delle buone caratteristiche di chiarezza sintattica e semantica. Nostro scopo sara' definire linguaggi per computazioni di complessita' limitata, a partire dal caso di LAL.
Task 2.2: Controllo del tempo di esecuzione tramite assegnazioni di tipo
[unita' partecipanti: 2, 4]
Assumendo che il lambda calcolo (o linguaggi disegnati a partire dal lambda-calcolo) sia il paradigma universale dei linguaggi di programmazione, l'idea e' di usare il concetto di tipo per definirne proprieta' legate alla complessita' di riduzione, dove i tipi sono formule di una logica che caratterizza tale complessita', secondo quanto illustrato nel task precedente. Infatti, vedendo il lambda-calcolo come linguaggio delle prove nel frammento implicazionale della logica intuizionista, l'insieme dei termini tipati in una logica caratterizzante la classe di complessita' C puo' rappresentare la restrizione di tali prove a quelle di complessita' C. Il problema e' che i termini del lambda calcolo non hanno abbastanza informazioni per codificare prove di questa nuova logica, e quindi le tecniche standard di assegnazione di tipo non sono direttamente applicabili. Si indaghera' l'esistenza di tipi principali in tale contesto, un problema per il quale gia' (per i tipi che siano formule di EAL) si hanno alcuni promettenti risultati preliminari, sia gia' pubblicati [CM01] sia in elaborazione . L'algoritmo di inferenza proposto lavora su termini che contraggono al piu' delle variabili. Ci proponiamo, come primo passo, di estendere tale lavoro rilassando questo vincolo e permettendo quindi anche termini che contraggono sotto-termini non banali. Tale estensione allargherebbe la classe di lambda-termini riducibili con l'algoritmo di Lamping astratto, cioe' senza oracolo (si veda il task 2.2).
Task 2.3: Riduzioni ottimali
[unita' partecipanti: 2]
La riduzione ottimale puo' essere criticata per il fatto che, dopo dieci anni dalla disponibilita' dell'algoritmo di Lamping, nessun confronto su vasta scala della sua performance e ancora disponibile. Uno dei motivi di questa situazione e' che il confronto dovrebbe esser condotto su benchmarks, ma quelli usati per i linguaggi funzionali fanno pesante uso di strutture dati addizionali, in genere non disponibili nei riduttori ottimali costruiti sinora. BOHM (il riduttore ottimale sviluppato a Bologna da Asperti) e' l'eccezione piu' cospicua, ma manca della possibilita' di modificare dinamicamente la rappresentazione iniziale dei termini, o di evitare del tutto l'oracolo. Implementazioni piu' efficenti possono essere trovate utilizzando proprieta' della logica EAL. Infatti, se un termine ha un tipo in EAL (si veda il task 2.2), la proprieta' che questo tipo esprime non concerne solo un limite alla sua complessita' di esecuzione (del resto la classe elementare e' vastissima!) ma garantisce che il termine stesso si possa ridurre con l'algoritmo di Lamping senza usare l'oracolo. Pertanto investigheremo la possibilita' di arricchire il linguaggio puramente logico di EAL/LAL. Intendiamo aggiungere naturali, booleani, liste e le relative operazioni, e estendere le tecniche di decorazione minimale a questi linguaggi. Il risultato sarebbe un prototipo di implementazione di linguaggio funzionale mediante l'algoritmo di Lamping e con l'aggiunta delle euristiche che derivano dallo studio di EAL. Un tale prototipo potrebbe essere confrontato con altre implementazioni utilizzando i benchmark standard disponibili in letteratura.
Filone 3: SEMANTICA DELLA COMPUTAZIONE E DEI LINGUAGGI DI PROGRAMMAZIONE
Come gia' detto in precedenza, l'introduzione di LL ha rinnovato anche la ricerca sulla semantica della dimostrazione e dei linguaggi di programmazione, suggerendo nuovi strumenti e nuovi punti di vista per ridurre l'analisi di proprieta' computazionali e strutturali allo studio di proprieta' matematiche astratte. In questo filone la nostra ricerca si articolera' nel modo seguente.
Task 3.1: Semantica delle dimostrazioni
[unita' partecipanti: 1, 3]
3.1.1 Semantica delle reti di prova
Si vuole cercare una semantica denotazionale delle reti di prova che sia iniettiva per un frammento di LL piu' ampio di quello considerato in [TdF01b]. Ci proponiamo di affrontare il problema seguendo due linee. Nella prima vogliamo usare la semantica denotazionale 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). Nella seconda, vogliamo usare un metodo probabilistico. La tecnica utilizzata in [TdF01b] per dimostrare l'iniettivita` della semantica consiste nel "ricostruire" una rete di prova senza tagli (e con soli assiomi atomici) a partire dalla sua semantica. Questa tecnica permette in realta` anche di "calcolare semanticamente" la forma normale di una rete di prova (si calcola la semantica di una data rete di prova e poi si ricostruisce l'unica rete di prova senza tagli con tale semantica: questo non puo`essere altro che la forma normale della rete di prova di partenza). Questo approccio al calcolo e` noto, nell'ambito dello studio dei linguaggi di programmazione funzionale, come "Normalization by evaluation" . Ci proponiamo di approfondire i legami tra la "Normalization by evaluation" e le tecniche dimostrative introdotte in [TdF01b].
3.1.2 Semantica categoriale di LL
Intendiamo studiare la semantica categoriale della logica lineare moltiplicativa nel contesto piu' generale possibile. Per esempio la regola di scambio dovrebbe essere considerata "intrecciata" (braided); daremo un teorema di coerenza per le categorie "ribbon braided *-autonomous". La relazione tra la formulazione intuizionista e quella classica dovra' essere chiarita in un contesto non commutativo e intrecciato. In particolare in tale contesto studieremo le costruzioni di Chu; studieremo inoltre le versioni intuizioniste complete di tali sistemi. Un ulteriore aspetto importante sara' quello di generalizzare le
costruzioni proposte al caso del par pre monoidale.
3.1.3 Dalla semantica alla pragmatica
Ci proponiamo di sviluppare un sistemi logico (LP) per la pragmatica basato su una semantica classica multi modale ed una pragmatica intuizionistica, che utilizza l'implicazione lineare per rappresentare la causalita` e l'interazione di processi. La proiezione della pragmatica sul livello semantico si basa su una estensione della interpretazione di Goedel, McKinsey e Tarski della logica intuizionistica in S4, in cui gli operatori espressivi di asserzioni e congetture corrispondono aglil operatori di interno e di chiusura (oppure di necessita` e possibilita`) nell'interpretazione topologica (o modale) della logica intuizionistica e nell'interpretazione duale. L'azione della semantica classica sulla pragmatica permette invece un nuovo approccio alla formalizzazione di frammenti costruttivi della logica classica. Il sistema proposizionale esistente verra` esteso al primo ordine; si considerera` anche l'introduzione di operatori modali indiciati tipici delle logiche della conoscenza. Il sistema (LP) potrebbe in futuro avere applicazioni anche alla assiomatizzazione dei fondamenti del diritto e alla formalizzazione dell'argomentare giuridico.
Task 3.2: Semantica dei linguaggi di programmazione
[unita' partecipanti: 2, 4]
Secondo un'approccio ormai consolidato, consideremo il lambda calcolo (e le sue varianti), tipato e non, come linguaggi di programmazione paradigmatici, a cui applicheremo le nostre indagini semantiche. Intendiamo in primo luogo continuare lo studio di modelli per vari lambda calcoli, tipati e non, utilizzando sia le PER sia la semantica a giochi. L'obiettivo e' la costruzione di nuovi modelli fully complete/fully abstract per diverse teorie operazionali di lambda calcoli. In particolare, vogliamo costruire un modello fully abstract per il lambda calcolo non tipato con una stategia di riduzione call by value, sfruttando i giochi con nozione con d'ordine, introdotti in [Dig01,OD02]. Inoltre vogliamo utilizzare i modelli di PER anche in direzione assiomatica, ad esempio per estendere il risultato di full completeness in [AL00] a classi di tipi del sistema F che vanno oltre i tipi polimorfi di ML. Al riguardo, una linea di ricerca molto promettente consiste nell'utilizzare i modelli di PER per fornire prove semantiche di decidibilita` di teorie. In particolare, i modelli di PER basati su algebre combinatorie per computazioni reversibili [AL00,AL01,Abr02], quali le algebre di partial involutions, possono essere sfruttate per fornire prove semantiche di decidibilita`, alternative alle prove sintattiche di Loader e Padovani, per le equivalenze osservazionali sul lambda calcolo tipato semplice e sulla versione unaria del PCF. E' noto che il problema della costruzione di una semantica fully-abstract e' problematico se si parte da spazi semantici che siano spazi funzionali: il concetto di funzione sequenziale in effetti e' un concetto difficile da catturare. Esistono restrizioni in questo senso delle funzioni stabili e degli spazi coerenti [BE91]. Ci si propone di studiare differenti restrizioni che possano rappresentare caratteristiche operazionali interessanti di PCF, legate alla sequenzialita'.

Testo inglese

Line 1: STRUCTURAL PROOF THEORY
Linear Logic has been introduced by Girard as a refinement of both classical and intuitionistic logic, by emphasizing the logical meaning of structural rules in Gentzen style sequent calculi (weakening, exchange, contraction), and consequently of the use of contexts in logical rules. This discover of the relevance of structural rules has several important consequences in proof theory, leading, among others, to a better grasping of the constructive content of classical logic. Our main objectives concerning the first line are:
1.1: Proof nets
[Sites: 1, 3, 4]
As stressed in the preceding items, the main tool in the study of proofs in LL are proof nets. We plan to refine further proof nets by studying their properties in different contexts. In particular we shall work on the following sub-tasks:
1.1.1 Extension and generalization of the concept of proof net
Moving from proof nets and logical flow graphs (Buss, Carbone) we shall investigate the role played by general structures in the representation of proofs (especially, but not exclusively, in the field of linear logic). Our aim is to achieve a finer analysis of aspects of normalization in deductive systems both functional and non functional. A relevant instance of this problem is the investigation of properties of normalization in the case of classical logic, usually identified with non-determinism and the treatment of proof irrelevance and focusing. We aim to elaborate new formulations of proof nets in the study of this topic especially to attack the difficult problem of proof identity in classical logic. Connected to the last topic is the study of the proof focusing paradigm. Proof focusing has been introduced by Andreoli [And92] in connection with the presentation of commutative linear logic by means of sequent calculi. His approach, making use of bipolar abstract proofs and linear equations, cannot be considered satisfactory. A solution has been proposed by the same author (Marseille, February 2002) and resorts to proofs nets and, more generally, modules (partial structures). The question about which notion of proof net is adequate while accounting for bipolarity and focusing properties emerging from the analysis of the standard LL and of the non commutative linear logic. The ultimate goal is to formulate a correctness criterion which is equivalent to that one which has been known for standard proof nets [DR89] and for the non-commutative case [AR00,Mai01]; moreover it should be incremental and modular.
1.1.2. Proof Modules.
We propose the development of a theory of proof modules, considering the multiplicative fragment of LL and of the non commutative linear logic. In particular: a) we look for a definition of module and of module type in the case of the non commutative linear logic without resorting to the notion of bipolarity (which involves an examination of the internal structure of a module); b) we seek new useful operations on the modules, beside that one which combines orthogonal modules into a proof net; c) we want to investigate the relation between proof modules and ludics.
1.1.3 Computational content of reduction of proof nets in the case of the non commutative linear logic.
We plan to characterize the computational content of the non commutative linear logic via a refined analysis of reductions.
1.2 Ludics.
[Sites: 1, 4]
Potentialities of the ludics [Gir01,Cur] as well as its applications are largely open to investigation. We intend to study the ludics both as a theory in itself and as a tool in the investigation of properties of complex logical systems. Concerning the first line of search we plan to study new connectives as they are suggested by the ludics; moreover we devise proof nets as a tool to analyze new quantifiers, extending and generalizing those which are definable in LL.
Concerning the second line, we plan to draw a logic system corresponding to intersection types, starting from the ludics: a partial solution to the same problem, as proposed in [RR01], is not yet satisfactory.
Line 2: COMPUTATIONS OF BOUNDED COMPLEXITY
By adding constrains to LL one obtains logical systems whose proofs encode exactly functions of some given class. Examples of such subsystems of LL are LLL[Gir98] and its refinements LAL [Asp98,AR02] and Soft Linear Logic [Laf01], characterizing functions in PTIME, and EAL [Gir98,DJ99], exactly catching the elementary functions. These results are of great importance for application to the theory and practice of programming languages. Within this line of search we aim at the following objectives:
Task 2.1: Logical characterization of computations of bounded complexity
[Site: 1, 2, 3, 4]
The research is aimed at a characterization of the properties that a logic must satisfy if it catches a complexity class of functions. Given such a class C, a logic L(C) characterizing C should satisfy two fundamental conditions. First the normalization procedure of L(C) has to be of complexity C; second L(C) must induce a complete description of the functions in C. These conditions are necessary to ensure an incremental description of the class C, being both machine independent and dynamically adequate. In this perspective the present formulations of LAL and EAL are not completely satisfactory, so that we look for suitable refinements of such systems matching the requirements above. Further we plan to define logical systems, inspired by LL, modeling other complexity classes. A relevant issue is the possibility of introducing new connectives modeling non determinism, which should lead to a logical characterization of non deterministic classes, first of all of NP. A subsequent objective of this task is to derive programming languages from logics capturing complexity classes. To derive the language from the logic the Curry-Howard morphism does not suffice: usually programming constructs obtained in this way are too involved to be of use in practice (see e.g. EAL [CM01]). On the contrary L(C) might be a framework in which programming strategies can be studied, to write code that is syntactically and semantically clear while retaining the property of implementing algorithms of bounded complexity. We shall aim at defining programming languages from LAL which allow for coding functions of bounded complexity.
Task 2.2: Controlling the running time via type assignment systems
[Sites: 2, 4]
Assuming that the lambda-calculus (or languages designed after the lambda-calculus) is a universal paradigm for programming languages, we devise to use the notion of type to catch properties connected to the complexity of reduction, where types are formulae of some logic capturing some complexity class, as illustrated in the preceding task. As a matter of fact, by seeing the lambda-calculus as the language of proofs of the implicational fragment of the intuitionistic logic, the set of terms which are typeable in L(C) might well represent the subset of those proofs which have complexity C. The obstacle is that in general the syntax of the lambda calculus cannot be expected to be expressive enough to catch all aspects of the proofs in L(C); therefore standard typing techniques are readily ruled out. We shall investigate the existence of principal typing in this context, a problem faced, with promising results, in the case of EAL, both published [CM01] and in progress. The proposed type inference algorithm works properly with terms contracting variables only. We propose to relax this constraint, allowing terms whose redexes are arbitrary. This would broaden the class of lambda terms which are reducible by means of Lamping abstract algorithm, namely without any oracle (see task 2.2).
Task 2.3: Optimal reduction
[Site: 2]
A criticism to optimal reduction is that, ten years after Lamping algorithm, no study of its performance in large scale is available. One reason is that benchmarks normally used in the case of functional languages make heavy use of additional data structures, which are not available in optimal reducers developed so far. BOHM (the optimal reducer developed by Asperti in Bologna) is the most relevant exception to this state of affairs, but it still lacks the ability to modify dynamically the representation of the initial terms, as well as to avoid the oracle at all. More efficient implementations can be found using properties of EAL. In fact, if a term is typable in EAL, (see task 2.2), then it is reducible by means of the Lamping algorithm without oracle. Therefore we plan to enrich the language of EAL/LAL, which is purely logical, by adding booleans, integers, lists and the related primitives; also the technique of minimal decoration should be extended to these languages. The expected result would be a prototypical implementation of a functional language based on Lamping algorithm integrated with the euristics coming from the study of EAL. Such a prototype could be tested against standard benchmarks available from the literature.
Line 3: SEMANTICS OF PROOFS AND PROGRAMMING LANGUAGES
As said before, the invention of LL renewed the research concerning programming languages semantics, by hinting at new tools and perspectives while reducing computational properties to abstract mathematical concepts. Along this line our work will be structured as follows:
Task 3.1: Proof semantics
[Site: 1, 3]
3.1.1 Proof nets semantics
We look for an injective denotational semantics for a larger fragment than that considered in [TdF01b]. We devise two approaches. Under the first one we plan to use the "Finiteness spaces" by T. Ehrhard (submitted for publication) and the normalization of the differential lambda-calculus (introduced by Ehrhard and Regnier by means of the mentioned semantics) The second approach consists in the use of a probabilistic method. The technique used in [TdF01b] to establish injectivity of the semantics is based on a "reconstruction" of a cut free proof net (and with logical axioms only) from its semantics. The same technique allows for computing semantically the normal form of a proof net. This approach is known in the field of programming languages as "Normalization by evaluation". We seek a deeper understanding of the relation between "Normalization by evaluation" and the proof theoretic techniques in [TdF01b].
3.1.2 Categorical semantics of LL
We aim at studying categorical semantics of the multiplicative linear logic in a quite general setting. For example the exchange rule should be considered in braided form; we look for a proof of a coherence theorem for ribbon braided *-autonomous categories. We expect to clarify the relation between classical and intuitionistic formulations of LL in the case of non commutative braided rules. In particular we shall investigate Chu constructions; other complete versions of these systems will be also considered. A relevant issue will be the generalization of these constructions to the case of pre-monoidal par.
3.1.3 Pragmatics from semantics
We propose to develop a logical system for pragmatics (LP), based on a multi modal classical semantics and an intuitionistic pragmatics, using linear implication to model causality and process interaction. This is based on a suitable extension of Goedel, McKinsey and Tarski interpretation of intuitionistic logic into S4, according to which assertions and conjectures correspond to interior and closure operators (necessitation and possibilitation) in the topological interpretation of intuitionistic logic and in the dual interpretation. The impact of classical semantics over pragmatics should be a new approach to the formalization of constructive fragments of classical logic. The existing propositional system will be extended to cope with first order quantification; indexed modal operators will be also considered as they are typical of epistemic logics. The system LP could have applications in the field of the axiomatization of rights and of formalization of legal arguments.
Task 3.2: Semantics of programming languages
[Sites: 2, 4]
According to an established approach, we consider the lambda calculus and its variants, both typed and type free, as paradigmatic languages, well suited to semantics investigations. We intend to pursue further the study of models of these calculi, both using PER and game semantics. This aims to the construction of new models fully complete/fully abstract for several operational theories. In particular we are interested to the construction of a fully abstract model of the type free lambda calculus endowed with a call-by-value reduction strategy, by exploiting the idea of ordered game models proposed in [Dig01,OD02]. Moreover we intend to use PER models also for the axiomatic, for example to extend the full completeness theorem of [AL00] to certain classes of types polymorphic second order types behind ML type system. A promising line of attack consist in using PER models to give semantics proofs of decidability of theories. PER models based on combinatory algebras for reversible computations [AL00,AL01,Abr02], such as partial involution algebras, are of use to establish decidability via semantics, in place of syntactical proofs due to Loader and Padovani, in the case of observational theories of the simply typed lambda calculus and unary PCF. It is well known that fully abstract semantic interpretations are difficult when in presence of functional spaces: the concept of sequential function is indeed difficult to catch. Suitable restrictions of the idea of stable functions and coherent spaces help [BE91]. We propose to study similar constructions modeling other operational characters of the calculus PCF, which are connected to sequentiality.

Unita' di ricerca impegnate:

Unità nº 1	Unità nº 2	Unità nº 3
Unità nº 4

Fase 2

Durata:	6 mesi		Costo previsto:	60.900 Euro

Descrizione:

Testo italiano

La seconda fase del nostro progetto sara', come si e' gia' detto, una fase "consuntiva", dedicata alla riflessione, sia in particolare sul lavoro svolto, sia in generale sul ruolo e sugli ulteriori possibili sviluppi e applicazioni della Logica Lineare e della Ludica all'Informatica. Ormai e' passato un lasso di tempo ragionevole dall'introduzione della Logica Lineare, e secondo noi e' ora possibile un primo consuntivo. Tale consuntivo non sara' certo definitivo ma potra' costituire una pausa di riflessione e una definizione di nuovi obiettivi. In particolare per la Ludica le sue possibili applicazioni all'Informatica, per quanto promettenti e stimolanti, non sono state ancora ben esplorate, e noi speriamo di dare un contributo in questo senso alla comunita' scientifica.

Testo inglese

The second phase will be devoted to meditation about the achievements obtained in the first one, as well as about the role that such results may play in future developments of Linear Logic and Ludic, with special attention to the perspective of its applications to computer science. A reasonable amount of time has elapsed since the beginning of LL, so that it is time, we think, of drawing a balance. Probably this will be not a conclusive one, rather will be of help to define further objectives. The situation is different in the case of Ludic, and indeed the possibility of applications to computer science are open to investigation: we hope to contribute to this work.

Risultati parziali attesi:

Testo italiano

Come abbiamo gia' spiegato, la Logica Lineare e' stata utilizzata in molti campi diversi dell'Informatica, che vanno dall'implementazione dei linguaggi di programmazione, all' analisi di computazioni di complessita' limitata, alla semantica denotazionale. Questa sua importanza per le applicazioni informatiche implica naturalmente la necessita' di uno studio dettagliato non solo dal punto di vista matematico e logico, ma dal punto di vista specifico dell'Informatica Teorica. Inoltre la recente nascita della Ludica, da una costola di LL stessa, richiede che ci si interroghi sulle sue possibili applicazioni per l'Informatica. Riflettere su questi punti e' il progetto della fase 2 della nostra ricerca. Vogliamo analizzare criticamente i risultati ottenuti nella Fase 1, nonche' le metodologie usate, per capire meglio le basi metodologiche e per poter evidenziare nuove applicazioni. Vogliamo portare avanti questa analisi critica sul ruolo di LL e Ludica in Informatica con l'aiuto di esperti a livello internazionale, organizzando un workshop finale espressamente dedicato a questo tema, e con pubblicazione dei risultati su uno special issue di una qualche rivista internazionale.

Testo inglese

Linear Logic has been used in many fields of computer science, ranging from denotational semantics and implementation of programming languages, to static analysis of computational complexity. This relevance of LL to computer science calls for a detailed analysis from the specific point of view of theoretical computer science. Moreover the rice of Ludic from LL opens the question of its applications to computer science. A careful consideration of such issues is the focus of phase 2 in our project. A critical analysis of the results of phase will be in order, both under the methodological and the applicative point of view. We want to pursue the critical analysis of the role that LL and Ludic may play in computer science profiting of the help of experts at international level, by organizing a final workshop dedicated to this theme. Publication of results is planned in some special issue of an international journal.

Unita' di ricerca impegnate:

Unità nº 1	Unità nº 2	Unità nº 3
Unità nº 4

Testo italiano

I criteri di valutazione di un progetto come questo, i cui risultati saranno soprattutto di tipo teorico, sono i seguenti:
- Le pubblicazioni prodotte nell'ambito del progetto sono valutabili in funzione del prestigio (impact factor) e della pertinenza della rivista, o degli atti del convegno, su cui appariranno.
- Ad ogni workshop del progetto saranno invitati revisori esterni, a cui saranni chiesti rapporti sulla qualita' dell'attivita' scientifica svolta. Tali rapporti saranno allegati al rapporto finale.
- Gli strumenti software sviluppati nell'ambito del progetto saranno resi disponibili in rete alla comunita' scientifica internazionale, che potra' sperimentarli. A tutti gli utenti verra' richiesto di redigere un rapporto sulla loro esperienza.
- Gli atti del convegno finale verranno pubblicati. La forma di pubblicazione e il successo del volume saranno un indice del prestigio del progetto.

Testo inglese

The evaluation criteria for a project like this one, characterized by the fact that the results will be theoretical, are the following:
- The publications developed during the project can be evaluated with respect to the impact factor and pertinence of either the journal or the conference proceedings, when they will appear.
- We will invite, at every workshop of the project, external referees, which will be asked to write reports on the quality of our scientific research. Such reports will be attached to the final one.
- The software developed inside the project will be put in the web, for be freely used by the scientific community. To all users a report on their experience will be asked.
- The proceedings of the final meeting will be published. The modalities of the publication and the success of the volume will be a measure of the result of the project.

Unità di ricerca	Voce di spesa, Euro										Totale
	Materiale inventariabile	Grandi Attrezzature	Materiale di consumo e funzionamento	Spese per calcolo ed elaborazione dati	Personale a contratto	Servizi esterni	Missioni	Pubblicazioni	Partecipazione / Organizzazione convegni	Altro
Unità nº 1	11.500		3.000		6.000		16.000	500	3.000	10.000	50.000
Unità nº 2	9.000		1.000		30.000		16.000		2.000	2.600	60.600
Unità nº 3	4.000				14.300		10.000		2.000	11.000	41.300
Unità nº 4	5.000		3.000				15.000		2.000	5.000	30.000
TOTALE	29.500		7.000		50.300		57.000	500	9.000	28.600	181.900

Il coordinatore certifica che il progetto ha carattere di originalità e non e' finanziato o cofinanziato
da altre amministrazioni pubbliche o private (art. 4 bando 2002)    

Unità di ricerca	Voce di spesa, Euro
	RD	RA	RD+RA	Cofinanziamento di altre amministrazioni pubbliche o private	Cofinanziamento richiesto al MIUR	Costo totale del programma	Costo minimo
Unità nº 1	6.000	9.000	15.000		35.000	50.000	40.000
Unità nº 2	9.100	9.100	18.200		42.400	60.600	60.600
Unità nº 3		12.400	12.400		28.900	41.300	41.300
Unità nº 4	4.200	4.800	9.000		21.000	30.000	30.000
TOTALE	19.300	35.300	54.600		127.300	181.900	171.900

171.900 Euro	(dal sistema, quale somma delle indicazioni dei Modelli B)
171.900 Euro	(dal Coordinatore del Programma)

(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")

Firma ____________________________________________	Data ___________________________ (inserita dal sistema alla chiusura della domanda)

.