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)

MARTINI	SIMONE
(cognome)	(nome)

Professore ordinario	26/12/1959	MRTSMN59T26H901X
(qualifica)	(data di nascita)	(codice di identificazione personale)

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

0432/558454	0432/558499	martini@dimi.uniud.it
(prefisso e telefono)	(numero fax)	(E-mail)

Testo italiano

Studi:
Dottorato di Ricerca in Informatica, 1988
Posizioni:
Univ. di Udine, ordinario di Informatica, dal 1994
Univ. di Pisa, associato di Informatica, dal 1992 al 1994
Univ. di Pisa, ricercatore, dal 1988 al 1994
Visitatore:
Ecole Normale Sup., Parigi, nov - dic 1992
Stanford Univ., sett 1989 - sett 1990
Digital Eq. Co., System Res. Center, giu - sett 1986
Direzione giovani ricercatori:
Stefano Guerrini (dottorato Pisa 1996), su Logica Lineare; Guerrini e' prof. ass. a Roma Sapienza;
Paolo Coppola (dottorato Udine 2001), su riduzione ottimale del l-calcolo; Coppola e' assegnista di ric. a Udine.
Comitati programma:
Computer Science Logic 1992, San Miniato (Pisa); Computer Science Logic 1995, settembre 1995, Paderborn.
Workshops per soli inviti:
- Computer Science Logic, Dagstuhl Seminar, July 13 -- 17, 1992.
- Linear Logic, Cornell University, Ithaca, NY, USA; June 14--18, 1993.
- IFIP Working Group 2.2, Formal Description of Programming Concepts, Observer. San Miniato, Italy, June 11--13, 1994; Amsterdam, The Netherlands, June 1995; Udine, Italia, June 1999.
- Mathematische Logik, Mathematisches Forschungsinstitut Oberwolfach, April 2 -- 8, 1995.
- Applicative theories and explicit mathematics, Bern (CH), June 19 -- 21, 1996.
Interessi di ricerca:
Sistemi di tipi, polimorfismo; Fondamenti della programmazione logica; Teoria delle categorie in informatica teorica; Logiche per computazioni con risorse limitate.
In Logica Lineare (LL) Martini ha studiato immersioni della logica modale S4 in LL e calcoli in deduzione naturale per LL col connettivo par. Sfruttando una tecnica sviluppata con Masini (sequenti indicizzati) per le logiche modali, ha studiato sottologiche di LL e tecniche per la riduzione locale di reti di prova. Si interessa ora all'applicazione di tali tecniche alla riduzione ottimale, dove ha ottenuto, con Coppola e Asperti, risultati sulla complessita' intrinseca della riduzione ottimale senza operatori di controllo e sulla Elementary Affine Logic.

Testo inglese

Studies:
Ph.D. in Computer Scie., Pisa, 1988
Posizioni:
Univ. di Udine, full prof. of Comp. Scie., since 1994
Univ. di Pisa, associate prof. of Comp. Scie., from 1992 to 1994
Univ. di Pisa, research fellow, from 1988 to 1994
Visiting:
Ecole Normale Sup., Parigi, nov - dec 1992
Stanford Univ., sept 1989 - sept 1990
Digital Eq. Co., System Res.Center, jun - sept 1986
Ph.d. supervision:
Stefano Guerrini (1996), on linear logic; Guerrini is currently assoc.prof. Rome-Sapienza
Paolo Coppola (2001), on optimal reduction; Coppola is research ass. in Udine.
Programm committees:
Computer Science Logic 1992, San Miniato (Pisa); Computer Science Logic 1995, settembre 1995, Paderborn.
Workshops by invitation:
- Computer Science Logic, Dagstuhl Seminar, July 13 -- 17, 1992.
- Linear Logic, Cornell University, Ithaca, NY, USA; June 14--18, 1993.
- IFIP Working Group 2.2, Formal Description of Programming Concepts, Observer. San Miniato, Italy, June 11--13, 1994; Amsterdam, The Netherlands, June 1995; Udine, Italia, June 1999.
- Mathematische Logik, Mathematisches Forschungsinstitut Oberwolfach, April 2 -- 8, 1995.
- Applicative theories and explicit mathematics,
Bern (CH), June 19 -- 21, 1996.
Research interests:
Type systems and polymorphism; Category theory in theoretical computer science; logics with limited resources (linear, in particular).
In the context of Linear Logic (LL), Martini studied an embedding of the modal propositional logic S4 into LL, and natural deduction calculi for LL with the par connective. Applying techniques developed togheter with Masini (Verona) for modal logics, Martini defined sublogics of LL and techniques for the local reduction of proof-nets.
Current interests are in the application of proof theoretical techniques to optimal reduction of functional programming languages. In this field he has obtained, with Asperti and Coppola, results on the intrinsic complexity of optimal reduction without control operators and on elementary affine logic.

1. COPPOLA P., MARTINI S. (2001). Typing lambda terms in elementary logic with linear constraints. Conference on Typed Lambda-Calculus and Applications, TLCA01. (vol. LNCS 2044, pp. 76-90). Springer-Verlag, Berlin.
2. GUERRINI S., MARTINI S., MASINI A. (2001). Proof nets, garbage, and computation. THEORETICAL COMPUTER SCIENCE. vol. 253, pp. 185-237 ISSN: 0304-3975 .
3. ASPERTI A., COPPOLA P., MARTINI S. (2000). (Optimal) duplication is not elementary recursive. ACM PRINCIPLES OF PROGRAMMING LANGUAGES POPL2000. pp. 96-107 ISSN: 1-58113-125-9 .
4. MARTINI S., MASINI A. (1995). On the fine structure of the exponential rule. ADVANCES IN LINEAR LOGIC. ISSN: 0 521 55961 8 Cambridge U. Press.
5. MARTINI S., MASINI A. (1994). A modal view of linear logic. JOURNAL OF SYMBOLIC LOGIC. vol. 59, pp. 888-899 ISSN: 0022-4812 .

Nº	Cognome	Nome	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
						2002	2003
Personale docente:
1	MARTINI	SIMONE	MATEMATICA E INFORMATICA	Prof. ordinario	INF/01	8 (ore: 1100)	8 (ore: 1100)
2	ALESSI	FABIO	MATEMATICA E INFORMATICA	Ricercatore	INF/01	3 (ore: 411)	3 (ore: 411)
3	DI GIANANTONIO	PIETRO	MATEMATICA E INFORMATICA	Prof. associato	INF/01	2 (ore: 275)	8 (ore: 1100)
4	HONSELL	FURIO	MATEMATICA E INFORMATICA	Prof. ordinario	INF/01	4 (ore: 550)	2 (ore: 275)
5	LENISA	MARINA	MATEMATICA E INFORMATICA	Ricercatore	INF/01	2 (ore: 275)	8 (ore: 1100)
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.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.	Assegno di ricerca, I anno	15000	11  (ore: 1507)
2.	Assegno di ricerca, II anno	15000	11  (ore: 1507)

1.7.6 Personale extrauniversitario dipendente da altri Enti

Nº	Cognome	Nome	Ente	Qualifica	Mesi uomo
1.	DAL LAGO	UGO	ITC-IRST, Trento	Contrattista di ricerca	14  (ore: 1925)

Testo italiano

Applicazioni della Logica Lineare: riduzione ottimale, computazioni limitate, lambda-modelli

Testo inglese

Applications of Linear Logic: optimal reduction, bounded computations, lambda-models

Testo italiano
LOGICA LINEARE ; RIDUZIONE OTTIMALE ; SEMANTICA DEI GIOCHI ; LAMBDA-CALCOLO

Testo inglese
LINEAR LOGIC ; OPTIMAL REDUCTION ; GAME SEMANTICS ; LAMBDA-CALCULUS

Testo italiano

La Logica Lineare (LL) ha ricevuto interesse non solo come sistema formale in se`, ma anche quale strumento per studiare problemi già noti da nuove prospettive. Ci interessano due di questi usi della LL, il primo connotato dai suoi obiettivi sintattici, il secondo con un carattere semantico. Entrambi sono applicazioni della LL al lambda-calcolo, un componente essenziale della nostra comprensione delle computazioni come riscrittura di simboli. Il punto di partenza di entrambe le applicazioni e’ la decomposizione dell’implicazione intuizionista A=>B come !Ao->A. Questa codifica uniforme interpreta un’implicazione (una funzione calcolabile) come un’azione di duplicazione/cancellazione (!) sugli argomenti, passati poi ad una funzione lineare (o->). La LL mette a disposizione operatori primitivi per queste azioni (duplicazione, cancellazione) che nell’approccio standard sono presenti solo al metalivello. Tali operatori possono essere sfruttati per: (i) controllare il modo in cui le dimostrazioni (programmi funzionali) sono costruite ed eseguite; (ii) costruire sofisticati modelli matematici di linguaggi funzionali. Sono questi i due contesti che discuteremo del seguito.
1. Annotazione di dimostrazioni intuizioniste per controllare le loro proprieta’ durante la riduzione.
L’immersione uniforme che abbiamo citata poc’anzi fornisce un primo modo per delimitare quelle parti (box) di una dimostrazione che possono necessitare di duplicazioni o cancellazioni durante la riduzione (computazione). L’operazione di duplicazione/cancellazione e’ vista, nell’approccio classico della LL, come un’azione atomica e istantanea. Ci si rese conto ben presto, tuttavia, che si potevano dare delle notazioni “distribuite” per i box che ne permettessero una duplicazione incrementale. In particolare, [GAL92] mostra che la riduzione ottimale dei lambda-termini secondo L’evy-Lamping [Lev78, Lam90] poteva essere interpretata come eliminazione dei tagli in proof-net “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. Le informazioni di condivisione (fans) controllano la duplicazione; le informazioni di mantenimento (brackets e croissants) indicano (e ricalcolano dinamicamente) i bordi dei box. Sono note diverse varianti di questa tecnica, che differiscono tra loro nel modo in cui le informazioni di mantenimento sono gestite (pe. [Asp95,GMM96, GMM01, AG98]). Lo studio dell’effettiva complessita’ di queste tecniche – quando sono applicate alla riduzione ottimale dei lambda-termini – ha ricevuto notevole attenzione negli ultimi anni, in risultati di Asperti, Lawall e Mairson che culminarono con [AM98]: E’ possibile esibire lambda-termini per i quali la riduzione a forma normale e’ non Kalmar elementare nella dimensione dei termini, e tuttavia possono essere normalizzati con un numero polinomiale di beta riduzioni ottimali (per famiglie). In [ACM00] viene mostrato che il risultato rimane vero anche per termini che non necessitino della complessa informazione di mantenimento che e’ necessaria in generale. Il principale strumento per ottenere questo risultato e’ la Logica Elementare Affine (EAL), un sottosistema della LL ([Gir98,Asp98]) che, sfruttando certe restrizioni sulle modalita’ di formazioni dei box, possiede una eliminazione dei tagli elementare. Piu’ in particolare, il risultato di [ACM00] e’ ottenuto mostrando che alcuni lambda-termini tipizzabili nel sistema semplice possono essere decorate mediante box di EAL. Si tratta di una decorazione altamente non uniforme, che cerca di inserire box solo laddove siano davvero necessari per assicurare la tipizzabilita’ in EAL.
L’analisi di decorazioni non uniformi per studiare proprieta’ di riduzione non e’ nuovo nella comunita’ di LL. In [DJS95] veniva proposta un’immersione (non uniforme) ottimale (nel numero di box) della logica intuizionista in LL, che permette, tra le altre cose, un’analisi della parte lineare di un programma funzionale molto piu’ precisa di quella possibile con la traduzione uniforme. La procedura per la derivazione dei box di EAL e’ stata completamente automatizzata in [CM01], dove e’ presentato un algoritmo di inferenza di tipo di EAL per i termini del lambda-calcolo senza tipi. La tecnica proposta permette di ottenere in modo uniforme, data una dimostrazione intuizionista, tutte le possibili decorazioni in EAL. Inoltre, si tratta di una tecnica che puo’ essere facilmente estesa a LL, fornendo quindi una diversa soluzione al problema affrontato in [DJS95]. Si puo’ infatti usare la tecnica di [CM01] per ritrovare le decorazioni ottimali di [DJS95], ma, anche, si possono definire ulteriori o diversi criteri di ottimalita’, per i quali le soluzioni sono trovate in modo uniforme sfruttando tecniche di programmazione lineare.
2. Costruzione di lambda-modelli
Negli ultimi anni la scena semantica e’ stata dominata dalla game semantics ([AJM00],[HO94]), che ha permesso la costruzione di modelli fully abstract di PCF, e si e’ dimostrata molto efficace nel fornire modelli sia di linguaggi sequenziali che della logica lineare. Anche strumenti e tecniche derivati dalla LL, tuttavia, costituiscono una valida alternativa alla game semantics per la costruzioni di modelli fully abstract e fully complete per lambda-calcoli tipizzati. In particolare, la recente tecnica della Realizzabilita’ Lineare [AL99, AL00] permette di costruire modelli di Partial Equivalence Relations su algebre combinatorie lineari.
In [AL99, AL00] e` stato definito un modello di PER fully complete per il frammento del sistema F corrispondente ai tipi di ML. La dimostrazione di full completeness sfrutta in modo essenziale l’analisi dell’implicazione intuizionista fornita da LL. In [AL01] sono studiati modelli di PER fully abstract rispetto a teorie massimali del lambda-calcolo tipato semplice con un numero finito di costanti di base. In un lavoro di Abramsky e Longley [ALo99], la tecnica della linear realizability e` stata recentemente utilizzata per definire un modello fully abstract per PCF, alternativo al game model di [AJM00].
Una linea di ricerca parallela - che e` emersa proprio dall'analisi delle dimostrazioni di full completeness e full abstraction di modelli di giochi e di PER - e` quella dell'assiomatizzazione dei modelli. In [Abr00,AL00a] sono stati individuati assiomi su modelli di vari lambda-calcoli che garantiscono la full completeness/full abstraction dei modelli stessi. Tali assiomi sono espressi come condizioni sulla categoria lineare soggiacente il modello di giochi o di PER.
Anche nel contesto della game semantics “classica” tecniche derivate dalla LL sono state sfruttate per ottenere modelli di particolari tipi di riduzione. Diversi ricercatori, in particolare, hanno esplorato la possibilita’ di utilizzare la game semantics per ottenere modelli fully abstract del lambda-calcolo puro. Con una qualche sorpresa, hanno mostrato [DFH99] che nella categoria dei giochi tutti gli oggetti riflessivi (cioe’ tutti i lambda-modelli estensionali) hanno la stessa teoria. Inoltre, in [DF00] e’ mostrato che ci sono solo due lambda-teorie possibili indotte da modelli non-estensionali: la teoria che identifica due termini sse questi hanno lo stesso albero di Boehm, e quella li identifica sse questi hanno lo stesso albero di Levy-Longo. Dunque sfruttando i giochi si possono ottenere modelli fully-abstract solo per strategie di testa su lambda-modelli puri. In [Dig01,OD02] sono stati costruiti, utilizzando due diversi paradigmi, due modelli fully-abstract ed universali per il lambda calcolo con una strategia lazy. Questi risultati sono stati ottenuti introducendo una nozione di monotonia all'interno dei giochi e definendo cosi' una nuova categoria di modelli.

Testo inglese

Like all the conceptually rich fields, Linear Logic (LL) attracted interest not only as a formal system per se, but also as a tool to investigate old and well-known problems from novel perspectives. We will focalize here on two such uses of LL, the first with a distinct syntactic aim, the other with a semantic flavor. Interestingly, both are applications of LL to the understanding of lambda-calculus, a cornerstone of our interpretation of computation as symbol rewriting. The technical starting point of both applications is the linear decomposition of the intuitionistic implication A=>B as !Ao->A. This uniform encoding explains an intuitionistic implication (that is, a computable function) as composed of a duplication (or deletion) action (!) on the arguments followed by a linear implication (o->). LL makes available primitive operators for dealing with actions (duplication, deletion) that in the standard approach are only present at the meta-level. These explicit operators can then be exploited (i) to control the way proofs (functional programs) are built and executed; or (ii) to construct sophisticated mathematical models for functional languages. These are, essentially, the two frameworks we will consider in the sequel.
1. Annotating intuitionistic proofs to control their reduction properties
Girard’s uniform embedding cited above gives a rough (but very effective) way to delimit those parts of a proof that may need to be duplicated or erased during its reduction (computation) – the boxes. The operation of duplication and/or erasing is a one-shot, instantaneous operation in the standard LL approach. However, it was soon discovered that there are "distributed notations" for boxes allowing for incremental duplication. In particular, [GAL92] showed that the optimal reduction of lambda-terms a` la Levy-Lamping [Lev78, Lam90] could be interpreted as cut-elimination in "box-free" proof-nets (PN). In these structures, the box "global" information is replaced by "local" information -- that is additional nodes -– expressing both sharing and bookkeeping information. Sharing information (fans) are used to control duplication; bookkeeping information (brackets and croissants) are used to mark the boundaries of the boxes and to dynamically re-compute them. Several variants of this techniques are known, differing in the way this information is maintained, and thus in the reduction rules and their properties (e.g. [Asp95, GMM96, GMM01, AG98]). The study of the actual complexity of these techniques -- especially when applied to the shared reduction of lambda-terms -- has received much attention in the last years, in a series of results by Asperti, Lawall and Mairson culminated in [AM98]: It is possible to give typed lambda-terms for which the complexity of the problem of reduction to normal form is provably non Kalmar elementary in the size of the terms, and, still, the terms may be reduced to normal form by shared reduction with only a polynomial number of beta (family) reduction steps. In [ACM00] it is further proved that the result remains true even for terms that do not need the complex distributed bookkeeping information which is necessary in general. The main tool used in that paper has been Elementary Affine Logic (EAL), a subsystem of LL (see [Gir98] and [Asp98]) which, by suitable restrictions on the way boxes may be formed, enjoys Kalmar-elementary cut-elimination. The result of [ACM00] is obtained by showing that certain simply typable lambda-terms (that is, intuitionistic proofs) can be decorated with EAL boxes. This is not a uniform decoration, acting on formulas, like Girard’s one. Instead, it is an ad hoc procedure trying to put boxes only when they are necessary for EAL-typability.
The investigation of non-uniform decorations to study reduction properties was not new in the LL community. In [DJS95] an optimal (in the number of boxes) proof-by-proof embedding of IL into LL is proposed, allowing an analysis of the linear part of functional programs more precise than the one given by the uniform translation. The procedure to infer EAL-boxes was fully automated in [CM01], where an EAL-type inference algorithm for simple typed terms is presented. The proposed technique allows to obtain, given an intuitionistic proof, all possible EAL-decorations in a uniform way. Moreover, the technique can be easily extended to LL, thus giving a different solution to the problem addressed in [DJS95]. Indeed, one could use the techniques in [CM01] to find all the optimal decorations of [DJS95], but also, using simple linear programming tools, to define different criterions of optimality for which solutions are found in a uniform way.
2. Building lambda-models
During the last ten years the semantical scene has been mainly dominated by game semantics ([AJM00],[HO94]) which allowed the construction of fully abstract models of PCF, and has been extremely successful in modeling both sequential languages and linear logic. Other tools and techniques derived from LL, though, are a valid alternative to game semantics to define fully complete and fully abstract models for several typed lambda-calculi. In particular, the recently introduced technique of Linear Realizability [AL99, AL00] allows the definition of models exploiting Partial Equivalence Relations over linear combinatory algebras.
In [AL99, AL00] it is defined a fully complete PER-model for the fragment of System F corresponding to ML-types. The proof of full completeness exploits essentially the finer linear analysis of the intuitionistic implication given by LL -- in the same way this analysis allowed to obtain fully abstract models for PCF and other languages with constructs for state and control. In [AL01] are studied fully abstract PER-models for maximal theories of the simply typed lambda-calculus with a finite number of base constants, and also for an infinitary version. In a paper by Abramsky and Longley [ALo99], the technique of linear realizability has been recently used to define a fully abstract model for PCF – an alternative construction to the standard game model of [AJM00].
A parallel research direction emerged from the analysis of the proofs of full completeness and full abstraction of both game and PER models. By studying these proofs, it became clear that an axiomatization of such concepts was possible. In [Abr00,AL00a] are introduced axioms for models of several lambda-calculi; these axioms are sufficient for the full completeness / full abstraction of those models, and are expressed as conditions over the linear category underlying the game (or PER) model.
Finally, even in the context of “classical” game semantics we could usefully exploit techniques derived from LL, to obtain models of particular reduction strategies. Several researchers, in particular, explored the possibility of using game semantics to obtain fully abstract models for the pure lambda calculus. Somewhat surprisingly, however, they proved [DFH99] that all reflexive objects, i.e. all extensional lambda-models, in the category of games, have the same theory. Furthermore, in [DF00] they have shown that there are only two possible lambda theories induced by non-extensional game models: the theory which identifies two terms iff they have the same Boehm-tree, and the theory which identifies two terms iff they have the same Levy-Longo tree. This implies that games can provide fully-abstract models only for head-reduction strategies on pure lambda terms. In [Dig01],[OD02] moreover, two different paradigms are used to define two fully abstract and universal models for the lambda-calculus with a lazy reduction strategy. These results are obtained by adding a monotonicity notion to the games, and obtaining in this way a new category of models.

[Abr00] S. Abramsky, "Axioms for Definability and Full Completeness", in Proof, Language and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C. Stirling and M. Tofte, eds., MIT Press, 2000, 55--75.
[Abr02] S. Abramsky, "A Structural Approach to Reversible Computation", POPL 2002.
[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.
[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).
[AL99] S.Abramsky, M.Lenisa. Fully Complete Models for ML Polymorphic Types, Technical Report ECS-LFCS-99-414, LFCS, University of Edinburgh, October 1999 (available at http://www.dimi.uniud.it/~lenisa/Papers/Soft-copy-ps/lfcs99.ps.gz).
[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.
[AL00a] S. Abramsky, M. Lenisa "Axiomatizing Fully Complete Models for ML Polymorphic Types", MFCS'2000 Conference Proceedings M. Nielsen, B. Rovan eds., Springer LNCS vol. 1893, 2000, pp. 141-151.
[AL01] Abramsky S., M. Lenisa. "Fully Complete Minimal PER Models for the Simply Typed Lambda-calculus", CSL'2001, LNCS 2142, 2001, pp. 443-457.
[ALo99] S. Abramsky, J. Longley, Realizability Models Based on History-free Strategies", draft, 1999.
[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.
[Asp98] Andrea Asperti. Light Affine Logic. In Proc. of LICS98.
[CM01] Coppola P. and Martini S. Typing lambda terms in elementary logic with linear constraints, in TLCA01, LNCS 2044, pp. 76—90, Springer, 2001.
[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.
[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.
[GAL92] Gonthier G., Abadi M., L'evy J-J, Linear logic without boxes, 7th LICS, 223-234, IEEE Press, 1992.
[Gir98] Jean-Yves Girard. Light linear logic. Information and Computation, 204(2):143-175, 1998.
[GMM96] S. Guerrini, S. Martini, and A. Masini, ``Coherence for sharing proof-nets'', Proceedings of RTA-96, Seventh Conf. on Rewriting Techniques and Appl., Springer, Berlin, LNCS 1103, 215-- 229.
[GMM01] S. Guerrini, S. Martini, and A. Masini, ``Proof nets, garbage, and computation'', Theoretical Computer Science. vol. 253(2) (2001), pp. 185-237.
[HO94] M. Hyland and C. H. L. Ong, Observational full abstraction for PCF: dialogue games and innocent strategies, 1994.
[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.
[OD02] L. Ong and Di Gianantonio Pietro. Games characterizing Levy-Longo trees. In ICALP '02, LNCS, to appear, Sprinter-Verlag, 2002.

Testo italiano

Come abbiamo anticipato in 2.4, programmiamo di lavorare su due (ampie) questioni, che discutiamo nel seguito.
1. Annotazione di dimostrazioni intuizioniste per controllare le loro proprieta’ durante la riduzione.
Abbiamo gia’ discusso in 2.4 i risultati ottenuti sulla Logica Elementare Affine (e Lineare), EAL, vista come strumento per caratterizzare lambda-termini con complessita’ di riduzione limitata. In particolare, in [CM01] viene dato un algoritmo per l’inferenza di tipi in EAL per lambda-termini puri. Se un termine ha un tipo in EAL, la sua riduzione e’ garantita avvenire all’interno della classe elementare (una classe enorme, si veda il seguito) e soprattutto, al nostro punto di vista, senza necessita’ di usare l’oracolo se viene usato l’algoritmo di Lamping. Si indaghera’ l’esistenza di tipi principali in tale contesto, un problema per il quale già si hanno alcuni promettenti risultati preliminari. 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). Studieremo inoltre EAL piu’ in profondita’ come logica. Abbiamo gia’ dei risultati preliminari non pubblicati sulla sua semantica delle fasi. Useremo queste nozioni per ottenere risultati di decidibilita’ sia per il frammento classico che per quello intuizionista implicazionale.
Nonostante il suo interesse dal punto di vista della riduzione ottimale, la classe elementare e’ un ambiente troppo grande dal punto di vista della complessita’. Indagheremo pertanto classi piu’ piccole e interessanti, la piu’ importante delle quali e’ chiaramente la classe polinomiale. Applicheremo le nostre tecniche ai vari frammenti polinomiali noti di LL, quali la Light Logic, sia nella versione lineare che in quella affine [Gir98, Asp98], la Soft Soft Linear Logic di Lafont [Laf01], o gli altri sistemi che nel frattempo diventeranno disponibili. L’estensione appare assai complessa, dal momento che i (forti) vincoli sintattici su queste logiche e la contemporanea presenza di piu’ modalita’ richiedono modifiche essenziali all’apparato tecnico. Anche in questo caso, studieremo queste logiche anche dal punto di vista semantico, con l’obiettivo di definire una nozione di modello e, con l’ausilio di questa, stabilire risultati di (in)decidibilita’, proprieta’ del modello finito, ecc.
E’ chiaro che queste questioni specifiche di ricerca sono parte di una prospettiva piu’ ambiziosa di lungo periodo, condivisa con altri siti di questo progetto. La caratterizzazione di misure intrinseche di complessita’ per i programmi funzionali, espresse in termini di concetti funzionali primitivi (e non mediante un riferimento diretto ad un modello d’esecuzione standard basato sulla macchina di Turing), rimane un argomento di ricerca tanto elusivo quanto difficile ed interessante. Riteniamo che lo studio di frammenti di logiche limitate in tempo possa gettare nuova luce e fornire nuovi strumenti per l’attacco a questo problema.
Un ultimo argomento di lavoro sara’ piu’ applicativo e riguardera’ direttamente la riduzione ottimale. 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. Investigheremo la possibilita’, pertanto, di arricchire il linguaggio puramente logico di EAL/LAL. Intendiamo aggiungere naturali, booleani, liste e le relative operazioni, e cercare di 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.
2. Costruzione di lambda-modelli
Le tecnologie per la costruzione e l’analisi di modelli che si sono descritte in 2.4 saranno oggetto di sviluppo e approfondimento. Si intende proseguire la ricerca sui modelli di PER per lambda-calcoli tipati, sia nella direzione di definizione di nuovi modelli fully complete / fully abstract, sia nella direzione assiomatica. In particolare, un problema aperto molto interessante e difficile e` quello di estendere il risultato di full completeness in [AL99, AL00] a classi di tipi del sistema F che vanno oltre i tipi polimorfi di ML. Inoltre si intendono studiare modelli di PER per lambda-calcoli, anche non tipati, con varie teorie. Infine, si intendono esplorare possibili applicazioni dei modelli cosi’ definiti. 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 [AL99,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.
Per quanto riguarda, infine, i game models, intendiamo sviluppare e sfruttare i giochi con nozione con d'ordine, introdotti in [Dig01,OD02], al fine di costruire modelli fully-abstract per diverse strategie di riduzione, non ancora trattate in maniera soddisfacente nell'ambito della teoria dei giochi. In particolare si vuol costruire un modello fully abstract per il lambda calcolo non tipizzato con una stategia di riduzione call by value.

Testo inglese

As we anticipated in 2.4, we plan to work on two different (broad) issues, that we will discuss in the following.
1. Annotating intuitionistic proofs to control their reduction properties
We already discussed in 2.4 the results obtained on Elementary Linear (and Affine) Logic (EAL) as a tool to characterize lambda-terms with a limited reduction complexity. In particular, in [CM01] algorithms are given for type inference in EAL for type-free lambda-terms. If a term has a type in EAL, its reduction is guaranteed to happen inside the elementary class (a huge class, see below) and without oracle if Lamping’s algorithm is used. We will investigate the existence of principal types in this framework, a problem for which we have some promising preliminary results.
The algorithms we considered allow only lambda terms contracting at most variables. We want, first, to provide extensions of the previous work, relaxing such constraint and allowing type inference of lambda terms contracting non trivial sub-terms. Such an extension would enlarge the set of lambda terms reducible using Lamping's abstract algorithm. We also plan to study more closely EAL as a logic. We already have preliminary unpublished work on its phase semantics. We plan to use these notions to obtain decidability results both for the classical and the intuitionistic (implicational) fragment.
Despite its interest from the optimal reduction perpective, the elementary class is a too vast environment from a complexity point of view. We plan therefore to look closely to smaller and interesting classes, the most important being clearly the polynomial one. Therefore, we will try to apply our technology to polynomial fragments of LL, such as Light Logic in the linear (LLL) or the affine variety (LAL) [Gir98, Asp98], Soft Soft Linear Logic of Lafont [Laf01], and the other fragments which could become available. The extension appears by no means trivial, since the (strong) syntactic constraints on these logic and the presence of several modalities call for essential modification. Again, we plan to study these logics also from the semantic point of view, with the aim to establish results like (un-) decidability, finite model property, etc.
It is clear that these specific research issues are parts of a more ambitious, long-term perspective, that we share with other sites of this proposal. The characterization of intrinsic complexity measures for functional programs, expressed in terms of primitive functional concepts (and not by direct reference to a standard, Turing machine model of execution), remains a subject as elusive as difficult and interesting. We believe that the study of time-bounded logical fragments could shed light and provide new tools for this problem.
A last subject of study will be mostly applicative and will concern directly optimal reduction. Criticism of optimal reduction can be raised on the ground that, after ten years since the availability of Lamping’s algorithm, no real scale comparison of its performance is available. One of the reasons for this is that real comparison should be conducted on benchmarks, while benchmarks used for functional languages make heavy use of additional data-structures, usually non available in the few optimal reducers built so far. BOHM (the optimal reducer developed in Bologna by Asperti) is a notable exception, but it lacks the possibility to change initial representation, or to avoid altogether the oracle. We plan, therefore, to investigate the possibility of enriching the purely logical language of EAL/LAL. We want to add naturals, booleans, lists and their operations and try to extend minimal decoration techniques to such a language. This would be a prototype implementation of a functional programming languages using Lamping's abstract algorithm and extended with the euristics derived from our own work on EAL. This prototype could be compared with other implementations using the benchmarks available in the literature.
2. Building lambda-models
We will develop and expand the techniques developed for the construction and the analysis of models (described in 2.4). We will work on the research on PER models for typed lambda-calculi, both to define new fully complete / fully abstract models, and to deepen our axiomatic understanding of them. In particular, a very interesting, difficult, open problem is the extension of the full completeness result of [AL99, AL00] to type classes more expressive than those of ML-polymorphism. Moreover, we will study PER models for (typed and untyped) lambda-calculi with several theories. Finally, we will explore possible applications of the models we define. Indeed, a very promising research direction is to use PER models to give semantic proofs of decidability for theories. In particular, PER models based on combinatory algebras for reversible computations [AL99,AL00,AL01,Abr02] (e.g., the algebras of partial involutions), can be exploited to obtain semantic decidability proofs (alternative to the syntactic proofs by Loader and Padovani) for observational equivalences on simply typed lambda-calculus and on unary PCF.
As for game models, we will further study and develop the concept of games with order notion, introduced in [Dig01,OD02}, with the aim to define fully-abstract models for several reduction strategies not yet satisfactory treated using classical game notions. In particular, we want to build a fully abstract model for the untyped lambda-calcolus with a call-by-value reduction strategy.

Nº	Anno di acquisizione	Descrizione
		Testo italiano	Testo inglese
1.
2.
3.
4.
5.

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