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)

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, ICTCS 01. 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º	Cognome	Nome	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
						2002	2003
Personale docente:
1	RONCHI DELLA ROCCA	SIMONETTA	INFORMATICA	Prof. ordinario	INF/01	8 (ore: 1100)	8 (ore: 1100)
2	DE' LIGUORO	UGO	INFORMATICA	Prof. associato	INF/01	5 (ore: 685)	6 (ore: 825)
3	GIOVANNETTI	ELIO	INFORMATICA	Prof. associato	INF/01	7 (ore: 959)	5 (ore: 685)
4	ROVERSI	LUCA	INFORMATICA	Ricercatore	INF/01	5 (ore: 685)	6 (ore: 825)
Altro personale:

1.7.2 Personale universitario di altre Università

Nº	Cognome	Nome	Università	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
							2002	2003
Personale docente:
Altro personale:
1	PAOLINI	LUCA	GENOVA	INFORMATICA E SCIENZE DELL'INFORMAZIONE	dottorando		3 (ore: 411)	3 (ore: 411)

1.7.3 Titolari di assegni di ricerca

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

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.7.6 Personale extrauniversitario dipendente da altri Enti

Nº	Cognome	Nome	Ente	Qualifica	Mesi uomo

Testo italiano

Logica Lineare come strumento per studiare proprietà computazionali e strutturali dei linguaggi di programmazione

Testo inglese

Linear Logic as a tool to study computational and structural properties of the programming languages

Testo italiano
LOGICA LINEARE ; LINGUAGGI DI PROGRAMMAZIONE ; LOGICA LINEARE LEGGERA ; LAMBDA CALCOLO ; TIPI

Testo inglese
LINEAR LOGIC ; PROGRAMMING LANGUAGES ; LIGHT LINEAR LOGIC ; LAMBDA CALCULUS ; TYPES

Testo italiano

L'introduzione della Logica Lineare (LL) [9] ha suggerito nuovi punti di vista e, quindi, nuovi strumenti, per lo studio e la soluzione di problemi informatici classici, di impronta sia fondazionale che applicativa.
I nuovi punti di vista scaturiscono dalla scoperta che alcuni concetti logici, considerati atomici, in realtà non lo sono. Il punto di partenza è la scomposizione dell'implicazione intuizionista in due operatori logici più primitivi: l'implicazione lineare `-o' ed una modalità `!'. Un'implicazione A-oB rappresenta una trasformazione che, preso UN oggetto della classe A, ne fornisce UNO nella classe B. La modalità denota un processo distinto dalla trasformazione lineare di A in B; essa evidenzia proprietà intensionali dell'oggetto in A da trasformare che descrivono la possibilità di replicare o ignorare del tutto l'oggetto, durante la trasformazione.
I principi ispiratori di LL possono essere adattati a diversi contesti tutti strettamente connessi con la teoria della dimostrazione, uno degli ambiti in cui le peculiarità di LL più nettamente si esprimono. Un contesto possibile è lo studio delle proprietà di linguaggi di programmazione paradigmatici, lambda-calcolo tipato/non-tipato in testa, dal punto di vista sia strutturale che computazionale.
Un altro contesto è lo studio di modelli astratti per la semantica. I risultati finora ottenuti in entrambi i contesti costituiscono la base di partenza scientifica di questo progetto.
1. Studio delle proprietà di linguaggi di programmazione paradigmatici.
Questa linea di ricerca a sua volta può essere suddivisa in due filoni, a seconda che si vogliano studiare proprietà computazionali o strutturali.
1.1) Proprietà computazionali
Lo studio di proprietà computazionali si orienta alla descrizione composizionale di classi di complessità interessanti, astraendo da definizioni legate a modelli computazionali, come le macchine di Turing. In questo contesto, l'idea principale è che la potenza computazionale di un linguaggio dipenda sia dalla capacità di replicare i termini, sia dalla libertà di manipolare separatamente repliche diverse di un singolo termine. La maggiore granularità operazionale e strutturale, suggerita da LL, permette di regolare finemente i gradi di libertà appena menzionati. Ne consegue la possibilità di caratterizzare alcune classi di funzioni, in modo indipendente da un qualsiasi modello computazionale.
[19] e [2] lavorano sulla Light Affine Logic (LAL), la versione affine di Light Linear Logic (LLL), introdotta in [10]. LAL è un sistema deduttivo, dotato di eliminazione del taglio, che caratterizza la classe delle funzioni polinomiali. In [19] Roversi dimostra che LAL è effettivamente completa rispetto alla classe delle funzioni polinomiali, vale a dire che è possibile codificare le macchine di Turing polinomiali sotto forma di derivazioni di LAL e simularle per mezzo della procedura di eliminazione del taglio. In [2] Asperti e Roversi formalizzano la definizione di LAL. In [10], inoltre, Girard introduce anche Elementary Linear Logic (ELL), formalmente ripulita in [8], la cui versione affine EAL è in [7].
1.2) Proprietà strutturali
Per proprietà strutturali si intendono essenzialmente proprietà sintattiche e operazionali dei linguaggi di programmazione; lo scopo è di esprimere solo le primitive di programmazione strettamente necessarie per ottenere l'espressività voluta. In [17] Ronchi e Roversi introducono una deduzione naturale per la LL Intuizionista, con un'analisi dei connettivi additivi, da cui disegnano anche, per mezzo del morfismo di Curry-Howard, un linguaggio di programmazione. Tale linguaggio estende in maniera naturale il lambda-calcolo usuale, pur conservando gli aspetti computazionali a basso livello, tipici di linguaggi disegnati a partire dalla LL. In [14] Pravato e Roversi introducono una versione tipata del linguaggio in [17]. In [18] e [20] Roversi studia una sintassi concreta per LAL. Il linguaggio in [18] e [20] e` tipabile automaticamente con formule di LAL, polimorfe alla ML. Tutti questi lavori si sviluppano strettamente a partire dalla teoria della dimostrazione di LL. [16] si ispira alla metodologia della teoria della dimostrazione, scaturita da LL, che scompone ulteriormente operatori logici, ritenuti primitivi. Infatti, in [16], Ronchi e Roversi propongono un connettivo logico con la stessa semantica della congiunzione dei tipi intersezione [6]. Intuitivamente, il nuovo connettivo si colloca tra la usuale congiunzione intuizionista e la congiunzione tensoriale di LL.
2) Studio di modelli astratti per la semantica.
Gli spazi coerenti [12], che sono un modello denotazionale della Logica Lineare, sono un raffinamento dei domini alla Scott. L'uso di tali spazi ha permesso di evidenziare interessanti proprietà semantiche di diversi tipi di computazioni. Ad esempio, per quanto riguarda lo studio delle computazioni lazy, Bastonero, Pravato e Ronchi [3] hanno dimostrato che l'uso di modelli coerenti permette una analisi più fine di quella possibile con i modelli alla Scott. Infatti questi ultimi eguagliano tutte le computazioni non terminanti, mentre i primi permettono di separare tra diversi tipi di non terminazione. Inoltre Pravato, Ronchi e Roversi [15] hanno elaborato una definizione categoriale di modello del lambda calcolo per valore, a partire dalla definizione categoriale di modello per la Logica Lineare [4].

Testo inglese

The invention and development of Linear Logic (LL) [9] suggests new perspectives and tools in the study and in the solution of classical problems in computer science, both foundational and applicative. The essential novelties stem from the discovery of the non atomic nature of certain logical concepts. The key point is the decomposition of the intuitionistic implication into a "linear" implication `-o' and a modal operator `!'. The meaning of A-oB is that there exists a transformation from realizers of A to realizers of B which makes use of the formers exactly once. On the other hand a realizer of !A is made up by an arbitrary replication of some realizer of A, hence !A-oB restores the intuitionistic meaning of the implication according to Heyting. Principles from LL are applicable in several concerns about and around proof theory, to which they are tidly connected. One of them is the formalization of structural and computational properties of programs coded into paradigmatic languages like the lambda-calculus, both typed and type free. Similarly they shed new light on denotational models of programming languages. The results obtained so far in these research areas are the starting point of the present proposal.
1) Study of properties of paradigmatic programming languages
Two issues can be distinguished.
1.1) Study of computational properties.
The main concern here is the description of complexity classes via syntactical restrictions, which abstract away from any notion of bounding resource of a particular model of computation. The basic intuition is that the computational strength of a programming language depends on its ability of replying information or manipulating several copies of the same data independently within the same computation. The higher granularity of LL with respect to intuitionistic logic (which is traditionally the basis of the theory of types) allows for the definition of finer constraints catching and classifying the mentioned features. This is the tool to classify functions on the basis of the structure of the algorithms that compute them while avoiding any reference to explicit bounds.[19] and [2] build over Light Affine Logic (LAL), the affine version of Light Linear Logic (LLL), introduced in [10]. LAL is a deductive system, satisfying cut elimination, whose proofs (of suitable formulas) encode exactly the functions in PTIME. In [19] Roversi proves that LAL is complete with respect to PTIME functions, that is it is possible to encode and simulate any Turing machine computing in polinomial time by means of deductions and of the cut elimination procedure of LAL. In [2] Asperti and Roversi completely formalize the definition of LAL. Moreover, in [10] Girard introduces Elementary Linear Logic (ELL), formally clarified in [8], whose affine counterpart is in [7].
1.2) Structural properties
By structural properties it is meant syntactical and operational properties of programming languages; the issue is to devise which programming constructs are essentially related to the desired expressivity. In [17] Ronchi and Roversi introduce a natural deduction system for the intuitionistic LL, including the additive connectives, from which a programming language is obtained via the Curry-Howard morphism. This is a natural extension of the lambda-calculus, which saves those aspects of control of the computation typical of LL.In [14] Pravato and Roversi study a typed version of the language in [17]. In [18] and [20] Roversi investigates a concrete syntax for LAL: the language presented in [18] and [20] is indeed typeable by formulae of LAL in the style of ML polymorphism. These papers exploit proof theoretical techniques. Much like the analysis of connectives in LL, in [16] Ronchi and Roversi propose an interpretation of the intersection type constructor [6]. Roughly speaking it turns out that this connective is in between the intuitionistic conjunction and the tensor of LL.
2. Abstract models and semantics
Coherent spaces [12] are a refinement of Scott models which provide a denotational semantics for LL, but also they have been used to enlighten properties of several types of computations. As an example in [3] Bastonero, Pravato and Ronchi show that coherent spaces allow for a finer analysis of the models for lazy computations than Scott models do. Indeed the latter identify all non terminating computations, while the formers distinguish between programs that do not terminate for different reasons. Furthermore Pravato, Ronchi and Roversi [15] elaborate a categorical notion of the call-by-value lambda-calculus based on the categorical models of LL [4].

[1] A. Asperti. "Light Affine Logic". Proc. of IEEE Symp. on Logic in Computer Science (LICS?98), IEEE, 1998.
[2] Asperti, A. and Roversi, L. "Intuitionistic Light Affine Logic". ACM Transactions on Computational Logic, 3(1), ACM, 2002, pp.137-175
[3] 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.
[4] 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.
[5] Bucciarelli A., Ehrhard T. "Sequentiality and strong stability",LICS?91, IEEE Computer Society Press, 1991, pp. 138-145.
[6] Coppo, M. and Dezani-Ciancaglini, M. "An extension of the basic functionality theory of the lambda-calculus". Notre Dame Journal of Formal Logic, 21(4), pp. 685 - 693, 1980.
[7] Coppola P., Martini S. "Typing lambda terms in Elementary Logic with linear contraints", in TLCA01, LNCS 2044, 2001, pp.76-90.
[8] V. Danos and J.-B. Joinet,"Linear Logic & Elementary Time", 1st international workshop on Implicit Computational Complexity (ICC'99)
Santa Barbara (California), 1999
[9] Girard J.-Y. "Linear logic: its syntax and semantics", Advances in Linear Logic, J.-Y. Girard, Y. Lafont and L. Regnier ed.s, Cambridge University Press, 1995, pp. 1 - 42
[10] Jean-Yves Girard."Light linear logic", Information and Computation, 143:175-204, 1998.
[11] Jean-Yves Girard. "Locus solum: from the rules of logic to the logic of rule", Math. Structures Comput. Sci., 11(3):301-506, 2001.
[12] Girard, J.-Y., Lafont, Y. and Tailor, P. "Proofs and Types". Cambridge University Press, 1989.
[13] Murawski A. S., Ong C.-H. L., "Can safe recursion be interpreted in light logic?". Second International Workshop on Implicit Computational Complexity, Santa Barbara, California, 2000.
[14] Pravato A. and Roversi L. "Lambda ! used as meta-language and as paradigmatic language".Fifth Italian Conference in Theoretical Computer Science, World Scientific, 1995, pp. 617-650.
[15] 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.
[16] S. Ronchi Della Rocca and Roversi L. "Intersection logic", CSL'01, LNCS 2412, Springer-Verlag, 2001, pp. 414-428.
[17] Ronchi Della Rocca S. and Roversi L. "Lambda Calculus and Intuitionistic Linear Logic" Studia Logica, 59(3), 1997, pp.417-448.
[18] L. Roversi. "A Polymorphic Language which is Typable and Poly-step". LNCS 1538, 1998, Springer Verlag. pp. 43 -- 60,
[19] L. Roversi. "A P-Time Completeness Proof for Light Logics", CSL'99, LNCS 1683, 1999, Springer-Verlag pp. 469 -- 483.
[20] 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.

Testo italiano

Il programma dell'unità sarà articolato secondo le linee di ricerca evidenziate nel punto 2.4.
1. Studio delle proprietà di linguaggi di programmazione paradigmatici.
1.1) Proprietà computazionali.
Si vuole innanzitutto studiare, da un punto di vista fondazionale, quali proprietà deve possedere una logica per caratterizzare in modo soddisfacente una classe di complessità computazionale. Data una classe di complessità 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 complessità C. In secondo luogo L(C) deve indurre la descrizione astratta della classe di complessità C. Solo l'esistenza di tutte e due queste proprietà ci garantisce una descrizione incrementale della
classe C, che sia 'machine independent', ma che nello stesso tempo definisca una precisa nozione dinamica di computazione. Nostro scopo è definire e studiare logiche che siano restrizioni della LL e che caratterizzino, nel senso detto sopra, differenti classi di computazione. Nostro punto di partenza sarà lo studio di LAL, che modella computazioni polinomiali. LAL non soddisfa completamente i nostri requisiti: è dimostrabile la non esistenza di una relazione incrementale tra LAL e caratterizzazioni alternative della computazioni polinomiali 'machine independent', basate su schemi ricorsivi [13]. Noi interpretiamo la necessità di passare attraverso le macchine di Turing polinomiali per relazionare LAL e gli schemi ricorsivi, come una dimostrazione della mancata individuazione degli aspetti astratti su cui una vera caratterizzazione 'machine independent' della classe in oggetto dovrebbe basarsi.
1.2) Proprietà strutturali
La ricerca si propone due obiettivi. Il primo è di utilizzare i risultati che saranno ottenuti nel punto 1.1), per il disegno di linguaggi di programmazione con complessità limitata. Infatti una logica L(C) che soddisfi i requisiti di cui al punto 1.1) può essere il punto di partenza per definire un linguaggio in cui esprimere a priori solo computazioni eseguibili in tempo C. Il procedimento di passaggio dalla logica al linguaggio non sempre può 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 [7]). Invece L(C) puo` generare un framework in cui studiare strategie di programmazione che suggeriscano primitive per un linguaggio, che non solo permetta di esprimere solo computazioni della complessità voluta, ma abbia delle buone caratteristiche di chiarezza sintattica e semantica. Nostro scopo sarà definire linguaggi per computazioni di complessità limitata, a partire dal caso di LAL. Alcuni risultati parziali in questa direzione sono stati ottenuti da Roversi.
Il secondo obiettivo è in qualche modo indipendente dai risultati ottenibili al punto 1.1), e quindi può essere sviluppato a partire dai risultati presenti nella base di partenza scientifica. Si assume che il lambda calcolo (o linguaggi disegnati a partire dal lambda-calcolo) sia l'essenza dei linguaggi di programmazione più naturali da usare e si usa il concetto di tipo per definirne proprietà legate alla complessità di riduzione. Data una logica L(C) la cui normalizzazione sia eseguibile in tempo C, l'assegnazione ai termini del lambda calcolo di tipi che siano formule di L(C) può garantire la loro riduzione in tempo C. Infatti, vedendo il lambda-calcolo come linguaggio delle prove nel frammento implicazionale della logica intuizionista, l'insieme dei termini tipati in questo contesto può rappresentare la restrizione di tali prove a quelle di complessità C. Il problema è che i termini del lambda calcolo non hanno abbastanza informazioni per codificare prove di L(C), e quindi le tecniche standard di assegnazione di tipo non sono direttamente applicabili. Alcuni risultati parziali in questo ambito sono stati ottenuti da Coppola e Ronchi per la logica EAL.
2) Studio di modelli astratti per la semantica
Un obiettivo particolarmente interessante nell'ambito della semantica denotazionale dei linguaggi di programmazione è la determinazione di classi di funzioni che modellino particolari proprietà operazionali. Esistono restrizioni in questo senso delle funzioni stabili e degli spazi coerenti [5]. Ci si propone di studiare differenti restrizioni che possano rappresentare caratteristiche operazionali interessanti di PCF, legate alla sequenzialità.
3) Ludica e Tipi intersezione
Le potenzialita' della ludica [10] e le sue possibili applicazioni formano un campo di ricerca completamente nuovo. Ci proponiamo di studiare il possibile uso della ludica per esplorare le proprieta' di sistemi logici complessi, disegnando un sistema logico che corrisponda all'assegnazione dei tipi intersezione [6], la cui soluzione, proposta in [16], non risulta ancora completamente soddisfacente.

Testo inglese

The work plan of this unit will follow directions described in section 2.4)
1) Study of properties of paradigmatic programming languages
1.1) Computational properties.
The research is aimed at a characterization of the properties that a logic must satisfy to catch in a satisfactory way 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 an abstract 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.
We aim at finding logics which are essentially restrictions of LL, but characterize various complexity classes. We will start with LAL, characterizing PTIME. Unfortunately LAL does not match the above requirements, as it can be shown that there is no incremental relation between LAL and other characterizations of PTIME via recursive schemes [13]. We think that the need of encoding Turing machines working in PTIME within LAL proofs to establish the equivalence of LAL representability and recursive schemes shows something missing in the machine independent characterization which is looked for.
1.2) Structural properties
The research aims at two objectives. One is to exploit possible results concerning task 1.1) to design programming languages ensuring that programs are of bounded complexity. In fact a logic L(C) satisfying the requirements in 1.1) could be the starting point to design a language exactly for functions in C. 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 [7]). 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.
The second objective does not strictly depend on possible results about 1.1), and therefore can be pursued starting from the achievements mentioned in the scientific background. We assume that the lambda-calculus (or languages designed after the lambda-calculus) is the essence of quite natural programming languages, and we use the notion of type to catch properties connected to the complexity of reduction.
Given a logic L(C), whose normalization has complexity C, the fact that a type which is a formula of L(C) can be assigned to a term will imply that its reduction is in C as well. 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 readly ruled out. Some preliminary results in this direction have been obtained by Coppola and by Ronchi for the logic EAL.
2) Abstract models and semantics
A major aim in denotational semantics is to find the abstract counterpart of certain operational properties. An example is the restriction of coherent spaces to model sequentiality in [5]. We propose to study similar constructions modeling other operational characters of the calculus PCF, which are connected to sequentiality.
3) Ludics and intersection types
Ludics [10] is a completely new, unexplored and potentially rich field.
We want to study its possible uses to describe complex logical systems.
In particular, we aim at the design of a logical system for the intersection types [6], whose proposal in [16] is not yet completely satisfactory.

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