Testo italiano

Teoria della Concorrenza, Linguaggi di Ordine Superiore e Strutture di Tipi.

Testo inglese

Theory of Concurrency, Higher Order and Types (CHORTIE)

MONTANARI	UGO
(cognome)	(nome)
Università degli Studi di PISA	Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI
(università)	(facoltà)
K05B	Dipartimento di INFORMATICA
(settore scient.discipl.)	(Dipartimento/Istituto)

ugo@di.unipi.it
(E-mail)

HONSELL	FURIO
(cognome)	(nome)

Professore ordinario	20/08/1958	HNSFRU58M20D969M
(qualifica)	(data di nascità)	(codice di identificazione personale)

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

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

K05B

Testo italiano
LOGICAL FRAMEWORKS ; TEORIA DEI TIPI ; SINTASSI ASTRATTA DI ORDINE SUPERIORE ; METODI COALGEBRICI ; LAMBDA CALCOLO ; PROGRAMMAZIONE CONCORRENTE CON VINCOLI ; LINGUAGGI DI COORDINAMENTO ; SCICUREZZA ; AUTOMI PER SISTEMI IN TEMPO REALE

Testo inglese
LOGICAL FRAMEWORKS ; TYPE THEORY ; HIGHER ORDER ABSTRACT SYNTAX ; COALGEBRAIC METHODS ; LAMBDA CALCULUS ; CONCURRENT CONSTRAINED PROGRAMMING ; COORDINATION LANGUAGES ; SECURITY ; REALTIME AUTOMATA

Testo italiano

Laurea in Matematica presso l'Universita` di Pisa (1981), Diploma in Matematica presso la Scuola Normale Superiore di Pisa (1983). Professore ordinario (K05B) presso l'Universita` di Udine dal 1990. Ha ricoperto posti di ricerca e/o di ruolo presso il Dipartimento di Informatica dell'Universita` di Torino (Ricercatore 1993-1995), presso la Edinburgh University (Research Fellow in Computer Science 1996-1998), Universita` di Udine (profesore associato K05B 1989-1990). Responsabile di unita` nei progetti della CE: HCM Lambda Calcul Type', EC SCIENCE MASK, ESPRIT WG TYPES. Membro di comitato di programma e ``invited speaker'' per varie conferenze internazionali. Membro dell' ``editorial board'' della rivista internazionale MSCS. Membo permanente dell' IFIP WG 2.2. Interessi di ricerca: semantica dei linguaggi di programmazione, lambda calcolo, logiche dei programmi, teorie dei tipi, logical frameworks, metodi logici, topologici e categoriali in informatica. contributi di ricerca: teroia degli insiemi non ben fondati, modelli del lambda calcolo, logical frameworks, lambda cacloli di oggetti.

Testo inglese

Laurea in Mathematics (1981, Pisa University), Diploma In Matematica (1983,Scuola Normale Superiore, Pisa). Full professor in Computer Science at Udine University since 1990. Research and academic postions previously held at Torino University (Ricercatore in Computer Science 1983-1985), Edinburgh University (Research Fellow in Computer Science 1986-1988), Udine University (Associate Professor in Computer Science 1989-1990). Site Leader of EC HCM Lambda Calcul Type', EC SCIENCE MASK, ESPRIT WG TYPES. PC member and invited speaker to international
conferences. Member of the the editorial board of MSCS. Member of the IFIP WG 2.2. Research interests: semantics of programming languages, program logics, lambda-calculus, type theory, logical frameworks, logical topological and categorical methods in informatics. Research contributions: non-wellfounded set theory, models and theories of lambda calculus, logical frameworks, lambda calculus of objects.

1. HONSELL F.; HONSELL F.; PLOTKIN G.; "A framework for Defining Logics" , Rivista: Journal of ACM , Volume: 40(1) , pp.: 143-184 , (1993) .
2. FISHER K.; HONSELL F.; MITCHELL J.; "A Lambda Calculus of Objects and Method Specification" , Rivista: Nordic Journal of Computing , Volume: 1 , pp.: 3-37 , (1994) .
3. HONSELL F.; MICULAN M.; SCAGNETTO I.; "pi-calculus in (Co)Inductive Type Theory" , Rivista: Theoretical Computer Science , pp.: 42 , (1998) in corso di pubblicazione .
4. HONSELL F.; LENISA M.; MONTANARI U.; PISTORE U. "Final Semantics for the pi-calculus" , Rivista: PROCOMET'98,Chapman & Hall , pp.: 225-243 , (1998) .
5. DI GIANANTONIO P.; HONSELL F.; LIQUORI L.; "A Lambda Calculus of Objects with Self-Inflicted Extension" , Rivista: ACM-SIGPLAN OOPSLA-98 , Volume: 333(10) , pp.: 166--178 , (1998) .

Nº	Cognome	Nome	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
						1999	2000
1	HONSELL	FURIO	MATEMATICA E INFORMATICA	Prof. ordinario	K05B	11	8
2	ALESSI	FABIO	MATEMATICA E INFORMATICA	Ricercatore	K05B	11	8
3	GABBRIELLI	MAURIZIO	MATEMATICA E INFORMATICA	Prof. associato	K05B	11	6
4	MAZZANTI	STEFANO	MATEMATICA E INFORMATICA	Ricercatore	K05B	8	6
5	PERON	ADRIANO	MATEMATICA E INFORMATICA	Ricercatore	K05B	11	8

1.10.2 Personale universitario di altre Università

Nº	Cognome	Nome	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
						1999	2000

1.10.3 Titolari di assegni di ricerca

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

1.10.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.	CIAFFAGLIONE	ALBERTO	MATEMATICA E INFORMATICA	1998	12
2.	FRANCO	GIANLUCA	MATEMATICA E INFORMATICA	1995	8
3.	SCAGNETTO	IVAN	MATEMATICA E INFORMATICA	1997	14

1.10.5 Personale a contratto da destinare a questo specifico programma

Nº	Qualifica	Costo previsto	Mesi uomo
1.	Dottorato in Informatica	30	11

1.10.6 Personale extrauniversitario dipendente da altri Enti

Nº	Cognome	Nome	Dipart./Istituto	Qualifica	Mesi uomo
1.	LENISA	MARINA	LFCS-Edinburgh	Research fellow	6
2.	LIQUORI	LUIGI	ENS-Lyon	attache' de recherche	6
3.	MICULAN	MARINO	INFN - Trieste	Tecnologo	6

Testo italiano

Teoria e sperimentazione di ambienti interattivi generati da Logical Frameworks basati sulla Teoria dei Tipi, per assistere nell'utilizzo di metodi formali. Sviluppo e studio di sistemi formali per la specifica, l'analisi e la verifica di sistemi concorrenti, linguaggi di coordinazione e lambda calcoli di oggetti

Testo inglese

Theory and experiment of interactive proof development environments, for assisting in the use of formal methods, based on Type Theoretical Logical Frameworks. Investigation of formal systems for the specification, analysis and verification of concurrent systems, coordination languages and lambda calculi of objects.

Testo italiano

Teoria, applicazioni e sperimentazione di ambienti interattivi generati da Logical Frameworks basati sulla teoria dei tipi (F.Honsell, F.Alessi, M.Miculan, I.Scagnetto,A.Ciaffaglione)

Dalla fine degli anni 80 sono state condotte molte ricerche ed esperimenti su ambineti interattivi computerizzati per derivaioni formali basati sulla teoria dei tipi (e.g. [HHP,COQ] TYPES WG ). La teoria dei tipi offre molti vantaggi come Logical Framework, ovvero come linguaggio di specifica per sistemi formali. In primo luogo permette di utilizzare la Sintassi Astratta di Ordine Superiore (HOAS) nella specifica della sintassi e della semantica operazionale dei linguaggi oggetto. Questo fa si che molti operatori di legame su variabili e nomi possano essere espressi in modo uniforme e algebrico. L'HOAS risulta quindi molto utile sia come metaformalismo
per esprimere aspetti sintattici dipendenti dal contesto, sia come standard per quanto concerne il trattamento dell'alpha conversione e dello ``scope''. Ma i Logical Frameworks permettono/costringono anche l'utente a formulare il proprio sistema in Deduzione Naturale (NDS) in modo da rendere esplicita la dipendenza tra assunzioni e conclusioni, ovvero la relazione di conseguenza logica utilizzata. Sia l'HOAS che l'NDS pertanto suggeriscono la possibilita` di riformulare il sistema oggetto in modo piu` astratto, meno legato ai dettagli di una particolare presentazione e piu` appropriato per il ragionamento formale assistito dal computer. Queste riformulazioni sono pero` spesso abbastanza problematiche. Ricadono in questa classe i sistemi per ragionare su processi (di ordine superiore quali) [MPW,AG,Bou]. A causa della natura complessa dei loro operatori di legame questi sistemi pero` beneficerebbero notevolmente da un'analisi in termini di HOAS o dall'esistenza di ambienti interattivi per essi. Fino ad oggi pero` tali sistemi non sono stati studiati in questo senso. Il gruppo di Udine ha una noptevole esperienza nel campo della specifica di sistemi formali in Logical Frameworks [HM,AHMP,HLMP,MMS]. Uno degli aspetti poiu` problematici riguardanti l'uso di sistemi in HOAS concerne il fatto che anche nei Logical Frameworks piu` potenti, quali [COQ], non e` possibile sviluppare adeguatamente la metateoria dei sistemi oggetto. Una possibile via d'uscita assiomatica a questo problema e` stata proposta dai ricercatori di questo gruppo in [HMS]. Recentemente Hofmann [Hof] ha mostrato come sia possibile usare modelli di prefasci per dimostrare la consistenza di alcuni assiomi di [HMS]. Anche Plotkin [MPS] e Pitts [GP] hanno recentemente utilizzato idee suggerite dalle categorie di funtori per la trattazione matematica della sintassi di linguaggi con operatori di legame. Lo studio delle correlazioni tra l'approcio assiomatico di [HMS] e quello categoriale sembra molto promettente.

Lambda calcoli di oggetti (F.Honsell, L.Liquori)

Sin dalla pubblicazione di [FHM] di Fisher,Honsell e Mitchell, vi e` stato molto interesse per i lambda calcoli di oggeti, ovvero per lambda calcoli con primitive per manipolare oggetti. L'utilita` nel rappresentare in un lambda calcolo un concetto risiede nel fatto che cio` permette di avere una comprensione concettulae migliore del concetto in questione ed una sua trattazione operazionale piu` astratta. Il lambda calcolo di oggetti in [FHM] formalizza un linguaggio ad oggetti ``delegation-based'' che contiene sia il lambda calcolo che primitive per creare, modificare e aggiornare oggetti. In [FHM] e` stato inoltre proposto un sistema di tipi che permette di prevenire staticamente errori del tipo ``messaggio non compreso''. Da allora un gran numero di estensioni e varianti di tale calcolo sono state proposte in letteratura per trattare sottotipi e oggetti incompleti, [BBDL,Liq]. C'e` ancora molto da fare pero` per sviluppare una teoria quadro per i lambda calcoli di oggetti.

Analisi categoriale della coinduzione, analisi algebrica dell'iterazione e analisi della struttura fine di varie categorie di domini (F.Honsell, M.Lenisa, S.Mazzanti, F.Alessi, A.Ciaffaglione)

Recentemente i metodi coinduttivi e coalgebrici per la specifica della semantica operazionale dei linguiaggi di programmazione hanno riscosso notevole successo e interesse [BMMR,Rut]. Questi metodi forniscono infatti principi elementari ma potenti per ragionare sul comportamento infinito di programmi, processi ed altri tipi di dati di ordine superiore. Specialmente quando vengono usati in combinazione con tecniche basate su relazioni logiche, essi permettono una trattazione strutturata degli oggetti infiniti attraverso le loro rappresentazion sintattiche, mantenendo dunque limitata la sovrastruttura matematica necessaria. Honsell e Lenisa da molti anni studiano la Semantica Finale, un particolare approccio categoriale alla coinduzione, specialmente in categorie di insiemi [HL95,Len96,HLMP,Len98a,Len98b]. Molte sono ancora le questioni aperte in questo ambito pero`. Mazzanti [ma95,Ma97] studia da anni il problema della caratterizzazione della semantica di costrutti iterativi su tipi di dati. La sua linea di indagine e`attualmente basata sugli operatori di chiusura. Honsell, Lenisa[HL98] e Alessi [ABBR] studiano da molti anni varie categorie di domini ordinati e metrici per la semantica dei linguaggi di programmazione. Vi sono ancora molti problemi aperti in questo ambito soprattutto per quanto concerne la completezza di tali categorie e la possibilita` di ottenere descrizioni coinduttive di equivalenze osservazionali. Un importante problema e` anche quello di``parzializzare'' domini metrici mediante domini effettivi ordinati.

Modelli semantici e metodologie di verifica per linguaggi di coordinamento (M.Gabbrielli)

La programmazione concorrente con vincoli (ccp) [SRP] e' un paradigma di programmazione asincrono nel quale la memoria, diversamente all'interpretazione classica , e' vista come un ``vincolo''. Dato che i vincoli e le operazioni di sincronizzazione e comunicazione possono essere espressi in termini logici, e' possibile ottenere in modo relativamente semplice metodologie di verifica [BGMP] e di analisi [FGMP93]. Recentemente sono state studiate estensioni di ccp per applicazioni real-time (introducendo una nozione di clock ed opportuni costrutti) [SJG,BGM], per applicazioni distribuite (sostituendo la memoria globale con una collezione di memorie locali) ed infine per permettere la rimozione di informazione dalla memoria (usando nozioni basate su logica lineare). Tutte queste estensioni sono interessanti nel contesto dei linguaggi di coordinamento. sia come spunto per nuove proposte, sia perche' i relativi modelli semantici possono essere utilizzati per studiare alcuni dei linguaggi esistenti.

Automi per sistemi in tempo reale(A.Peron)

Sono state proposte in anni recenti varie classi di automi adatti a modellare sistemi in tempo reale. Il confronto fra classi differenti di automi viene fatto tradizionalmente basandosi sul potere espressivo, proprieta' di decidibilita',d e, piu' recentemente, sulla capacita' di esprimere sintetiche descrizioni. Inoltre, sono state tradizionalmente stabilite delle forti connessioni tra la teoria degli automi e le logiche per la specifica di sistemi in tempo reale. In questo contesto, interessati alla logica degli automi sistolici ad albero binario introdotta in [MP] e usata in [MPP] per definire una teoria (decidibile) monadica del secondo ordine su strutture con un numero infinito di domini temporali lineari approssimabili. La teoria in questione consente di esprimere in modo naturale quelle proprieta' dei sistemi in tempo reale che fanno riferimento a scale temporali diverse.

Testo inglese

Theory, applications, and experiment of proof development environments based on type theoretic Logical Frameworks (F.Honsell, F.Alessi, M.Miculan, I.Scagnetto, A.Ciaffaglione)

Since the late '80's there has been extensive research and experiment in using proof development environments based on intuitionistic type theory for computer assisted formal reasoning (see e.g. [HHP,COQ] TYPES WG ). When taken as a Logical Framework, i.e. as a specification language for formal systesm, type theory offers many advantages. First it allows for Higher Order Abstract Syntax (HOAS) to be used in the specification of the object syntax and its operational semantics; thereby allowing to express binding operators on variables, names, and locations in a uniform and algebraic way. HOAS is in fact extremely valuable both as a formalism for capturing certain context sensitive aspects of syntax, and for setting a standard on how scope and alpha conversion should be handled in formal systems. But Logical Frameworks allow/urge also the user to present his system in a natural deduction style (NDS), thereby making explicit the dependency between assumptions and conclusions, i.e. the consequence relations involved. Both HOAS and NDS suggest reformulations of the original logical systems which are much closer to the semantics, free form the irrelevant details of a specific presentation and more appropriate in mechanized formal reasoning. However, such reforrmualtions are often difficult to obtain.
A case in point concerns (higher order) process and nominal calculi e.g. [MPW,AG,Bou]. Because of the complex nature of the operators on variables and names which they feature, these systems could greatly benefit form HOAS analyses and Logical Framework based proof development environments. However, up to now, very little has been carried out in this direction.
The Udine group has a solid experience in tailoring formal systems for Type Theoretic Logical Frameworks (see e.g. [HM,AHMP,HLMP,MMS]).
A problematic theoretical issue concerning HOAS is the following: even in powerful Logical Frameworks such as COQ, metatheoretic reasoning on HOAS is limited. In [HMS] the researchers in this proposal have outlined a viable axiomatic methodology to overcome these drawbacks. Recently M.Hofmann in [Hof] has shown how suitable presheaf models can be used to prove consistency of some of those axioms. Also G.Plotkin et al.[FPT], and A.Pitts et al. [GP] have used recently ideas based on functor categories for structuring mathematically the syntax of systems involving binders. There seeems to be a lot to be done in comparing the methodology of [HMS] with the functor theoretic approach.

Lambda calculi of Objects (F.Honsell, L.Liquori)

Since the publication of [FHM] by Fisher, Honsell and Mitchell, there has been growing interest in calculi for objects, i.e. in lambda calculi extended with primitives for defining and manipulating objects, see e.g.[AC]. The ultimate goal in embedding new programming concepts in a lambda-calculus setting is to achieve a better conceptual understanding and a more abstract and general operational treatment of the concept under consideration. We can in fact capitalize on the extensive successful theoretical work that has been carried out in lambda calculus because of its principled and mathematically tractable syntax and semantics. The lambda calculus of objects of [FHM] formalizes a small delegation-based language which contains both lambda calculus and object primitives for creating, updating, and sending messages to objects. In [FHM] also a sound type assignment system was given, which allows to check statically if errors of the kind ``message not understood'' will not arise at run time. A number of extensions, or variants of the original language and type system, have been investigated by many researchers in this proposal, including Liquori [BBDL,Liq], and many typing disciplines which deal e.g. with subtypes and incomplete objects have been considered. Much remains to be done however in developing a general frameork for lambda calculi of objects.

Categorical analysis of coinduction, algebraic analysis of
iteration and fine analysis of categories of domains (F.Honsell, M.Lenisa, S.Mazzanti, F.Alessi, A.Ciaffaglione)

Recently [BMMR,Rut], there has been much interest on coalgebraic and coinducitve methods for the specification of operational semantics of programming languages. Such methods provide powerful proof principles for reasoning on the infinite behaviours of programs, processes, and objects of higher order datatypes (e.g. exact reals). Especially when used in connection with techniques based on logical relations, they allow to reason on infinite objects in a mathematically principled and structured way, just by considering syntactical representations, thereby keeping the mathematical sovrastructure to a minimum. Honsell and Lenisa have been investigating Final Semantics, a particular categorical approach to coinduction, for quite some time [HL95,Len96,Len98a,Len98b,HLMP], especially in set theoretic categories based on hypersets. The whole area of operationally based semantics, however, appears to be full of yet unresolved general questions.
S. Mazzanti [Ma95,Ma97] has been investigating for many years the old, but surprisingly not yet completely solved, problem of characterizing the semantics of iterative constructs on data types. His current line of approach is that of using closure operations on preorders.
F.Honsell, M.Lenisa [HL98b] and F.Alessi [ABBR] have been investigating various metric and ordered categories of domains used in the semantics of programming languages, for many years. There are still many important open questions in this area especially with respect to the completeness of such categories and the possibility of providing coinductive characterizations of observational equalities. An important unresolved problem is also that of embedding metric spaces in effective domains.

Semantic models and verification methodologies for coordination
languages (M.Gabbrielli)

Concurrent constraint programming (ccp) [SRP] is an asynchronous (concurrent) programming paradigm where the classical notion of store-as-valuation is replaced with the notion of store-as-constraint. Since constraints and the notions of communication and synchronization can be formalized logical terms, one can obtain in a rather straightforward way a proof-theory [BGMP] and analysis tools [FGMP93] for ccp. Recently ccp has been extended for real-time applications (by introducing a notion of clock and suitable primitives) [SJG,BGM], for distributed computing (by replacing the global store with several local stores) and for allowing removal of information from the store (by using a linear logic setting). All these extensions are relevant in the context of coordination languages since they can inspire new proposals and their semantics models can be used to study existing languages.

Real time automata (A.Peron)

Various classes of timed and synchronous automata have been proposed which are capable of modelling real time systems. Different classes of automata are usually compared with respect to their expressive power, the decidability of some basic properties and, more recently, "succinctness" of their representation of real time systems. Moreover, strong connections have been shown between automata and logical theories for the specification of real time systems. In particular, the logical theory of binary tree systolic automata, introduced in [MP], has been recently exploited in [MPP] for defining a decidable monadic second order theory over an infinite number of coarsable linear temporal domains. That theory allows to naturally express properties of real time systems which refer to times of different temporal granularity.

K. Fisher, F. Honsell, J. Mitchell

• [ABBR] Alessi, Baldan P. Bellè G. Rutten J.: Solutions of Functorial and Non-Functorial Metric Domain Equations, MFCS'95 Electronic Notes in Computer Science, Abstract available in Theoretical Computer Science 152, pp.321-332.
  
• [AC] M. Abadi, L. Cardelli: A Theory of Objects Springer Verlag, 1996.
  
• [AHMP98] Arnon Avron, Furio Honsell, Marino Miculan, and Cristian Paravano: Encoding Modal Logics in Logical Frameworks. Studia Logica, 60,(1), 1998.
  
• [AG] M. Abadi, A. Gordon: A Calculus for Cryptographic Protocols: The Spi Calculus.Information and Computation 148(1) pp. 1-70, 1999. Academic Press.
  
• [BGM] F.S. de Boer, M. Gabbrielli, and M.C. Meo. Semantics and expressive power of a timed concurrent constraint language. In G. Smolka. editor, Proc. Third Int'l Conf. on Principles and Practice of Constraint Programming (CP 97), Lecture Notes in Computer Science. Springer-Verlag, 1997.
  
• [BGMP] F.S. de Boer, M. Gabbrielli, E. Marchiori and C. Palamidessi: Proving Concurrent Constraint Programs Correct. Transactions on Programming Languages and Systems (TOPLAS), 19(5): 685-725, ACM Press, 1997.
  
• [BMRR] B.Jacobs et al. : Proc. 1st Wkshp. on coalgebraic methods in CS, ENTCS 11, 1998.
  
• [Bou] G.Boudol: The pi-calculus in direct style. Higher-Order and
  Symbolic Computation Vol 11, pp. 177-208, 1998
  
• [BBDL]V.Bono, M.Bugliesi, M.Dezani and L.Liquori: A Subtyping forExtendible, Incomplete Objects. Fundamenta Informaticae. to appear
  
• The COQ proof assistant reference manual - INRIA TYPES WG
  
• [DGHL] P.Di Gianantonio, F.Honsell, and L.Liquori: A Lambda Calculus of Objects with Self-Inflicted Extension In Proc. of ACM-SIGPLAN OOPSLA-98, Vol 33, Number 10, October 1998, pp 166--178, ACM Press.
  
• [DFP] R. De Nicola, G. Ferrari, R.Pugliese. Klaim: a Kernel Language for Agents Interaction and Mobility. IEEE Transactions on Software Engineering,
  24(5):315-330, IEEE Computer Society Press, 1998.
  
• [FGMP93] M. Falaschi, M. Gabbrielli, K. Marriott and C. Palamidessi: Compositional analysis of concurrent constraint languages. In Proc. Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 93), pages 210-221. IEEE Computer Society Press, 1993.
• [FGMP97] M. Falaschi, M. Gabbrielli, K.Marriott and C. Palamidessi: Confluence in Concurrent Constraint Programming. Theoretical Computer Science, 183, pp. 281-315, 1997.
• [FPT] M.Fiore, G.PLotkin, D.Turi: Abstract Syntax and Variable Binding, to appear in LICS'99.
  
• [Gel] D. Gelernter: Generative Communication in Linda. ACM TOPLAS 7(1), 1985.
  
• [GP] J.Gabbay, A.Pitts: A new approach to abstract syntax involving binders, to appear in LICS'99.
  
• [Hof] M.Hofmann: Semantical Analysis of higher order abstract syntax
  to appear in LICS'99
  
• [HHP] R. Harper, F. Honsell, G. Plotkin: A framework for Defining Logics.
  Journal of ACM,Vol. 40, No. 1, (1993), 143-184.
  
• [HL95] F. Honsell, M. Lenisa; Final semantics for untyped lambda calculus, TLCA'95, Springer LNCS 902, 1995.
  
• [HL98]F. Honsell, M. Lenisa: Semantical Analysis of Perpetual Strategies in lambda-calculus to appear in Theoretical Computer Science 213 , 1998.
  
• [HLMP] F. Honsell, M. Lenisa, U. Montanari, and M. Pistore Final Semantics for the pi-calculus, Programming Concepts and Methods PROCOMET'98, D. Gries et al. eds., Chapman & Hall, 1998.
  
• [HM] F.Honsell, M.Miculan: A natural Deduction approach to Dynamic Logic. Springer LNCS 1158, 1996.
  
• [MMS] F. Honsell, M. Miculan, I. Scagnetto: pi-calculus in (Co)Inductive Type Theory aparira` su Theoretical Computer Science.
  
• [Len96] M. Lenisa; Final semantics for a higher order concurrent language, CAAP'96, Springer LNCS 1059. 1996
  
• [Len98a] Marina Lenisa: Themes in Final Semantics Ph.D. Thesis TD-6/98, March 1998. Dipartimento di Informatica, Università di Pisa.
  
• [Len98b] Marina Lenisa: A Coinductive Logical System for Bisimulation Equivalence of Circular Objects, to appear in ETAPS '99
  
• [Liq] L.Liquori : On Object Extension. In ECOOP-98, Springer LNCS 1445, pp 498 522, 1998.
  
• [LLL] Lang, F. and Lescanne, P. and Liquori, L.: A Framework for Defining Object Calculi" ENS Lyon RR 1998-51, 1998.
  
• [Ma95] Mazzanti S.: Succint Iterative Characterizations of Primitive Computable Unary Functions, Information Processing Letters 56, pp. 315-319, 1995.
  
• [Ma97] S. Mazzanti: Iterative characterizations of computable unary functions: a general method, Mathematical Logic Quarterly 43 (1997) 29-38.
  
• [MP98] A. Monti and A. Peron: A Logical Characterization of Systolic Languages, Proceedings International Symposium on Theoretical Aspects of Computer Science (STACS'98), LNCS 1373, pp. 466--476, 1998.
  
• [MP9?] A. Monti and A. Peron: Systolic Tree omega-Languages: The Operational and the Logical View, Theoretical Computer Science, to appear.
  
• [MPP] A. Montanari, A. Peron and A. Policriti: Theories of omega-layered metric temporal structures: Expressiveness and Decidability, Logic Journal of the IGPL, 1999, to appear.
  
• [MPW] R.Milner, J.Parrow, D.Walker. A calculus of mobile processes. Inforamtion and Computation, 100(1):1-77, 1992.
  
• [Rut] J.J.M.M. Rutten: Universal coalgebra: a theory of systems, CWI CS-R9652,1996.
  
• [SJG] V.A. Saraswat, R. Jagadeesan, and V. Gupta: Foundations of
  Timed Concurrent Constraint Programming. In S. Abramsky editor, Proc. of the Ninth IEEE Symposium on Logic in Computer Science, pages 71--80. IEEE Computer Press, July 1994.
  
• [SRP] V.A. Saraswat, M. Rinard, and P.Panangaden: Semantic Foundation of Concurrent Constraint Crogramming. In Proc. Eighteenth ACM Symposium on Principles of Programming Languages, pages 333-353. ACM Press, 1991.

Testo italiano

Come e` sato fatto nella presentazione della base di partenza scientifica, distingueremo l'attivita` di ricerca dell'unita` di Udine in 5 filoni:

• teoria, applicazioni e sperimentazione di ambienti interattivi generati da Logical Frameworks basati sulla teoria dei tipi,
• Lambda Calcoli di oggetti,
• analisi categoriale della coinduzione, analisi algebrica dell'iterazione e analisi della struttura fine di varie categorie di domini,
• modelli semantici e metodologie di verifica per linguaggi di coordinamento,
• Automi per sistemi in tempo reale.

Per ciascuno di questi filoni discuteremo gli obiettivi generali e daremo il piano di lavoro specifico suddividendolo nei due anni.

Teoria, applicazioni e sperimentazione di ambienti interattivi generati da Logical Frameworks basati sulla teoria dei tipi (F.Honsell, F.Alessi, M.Miculan, I.Scagnetto, A.Ciaffaglione)

I calcoli di processi (di ordine superiore), recentemente introdotti per laspecifica e verifica di protocolli, come ad esempiolo spi calcolo [AG] e il blu calcolo [Bou], non sono stati fino ad oggi rappresentati in Logical Frameworks basati sulla teoria dei tipi, ne' analizzati dal punto di vista della HOAS. Sviluppando la metodologia che abbiamo introdottdo in [HMS] per l'archetipo di tali calcoli, ovvero il pi-calcolo di Milner et al. [MPW], noi intendiamo codificare tali sistemi in HOAS, e sperimentare con gli ambienti interattivi generati da queste codifiche in COQ [COQ]. Sia gli utilizzatori che gli ideatori di tali sistemi dovrebbero beneficiare di questi analisi analisi sintattiche astratte e delle implementazioni da esse generate. Tali calcoli hanno infatti sintassi piuttosto idiosincratiche e sono piuttosto difficili da manipolare senza sussidi automatizzati. Questi esperimenti dovrebbero condurre alla costruzione di un ``workbench'' assitito dal computer, basato su COQ, per l'analisi e la verifica della sicurezza nei protocolli di comunicazione. Questi esperimenti dovrebbero anche aiutarci pero` a delineare una metodologia generale per rappresentare e ragionare su ``nominal calculi'' e calcoli di processi in HOAS. Per poter sviluppare nei Logical Framework anche la metateoria di questi sistemi , dovremo pero` estendere la teoria dei tipi con nuovi assiomi e/o principi di induzione/ricorsiva e coinduzione. Solo cosi` si potranno infatti superare le limitazioni intrinseche delle teorie dei tipi nella trattare la metateoria di sistemi in HOAS. Questo approccio assiomatico, originariamente adoperato in [HMS] ci permette di mantenere trasparente la codifica e allo stesso tempo di contenere la complessita` della sovrastruttura matematica. Il nostro obiettivo ultimo, in questo ambito, e` quello di definire un sistema consistente di principi metalogici per ragionare su sistemi arbitrari inHOAS. Questo approccio pero` necessita` di accurate analisi semantiche per dimnostrare la consistenza del tutto. Recentemente Hofmann [Hof] ha dimostrato come utilizzare categorie di funtori per modellare teorie dei tipi intuizionistiche e ha suggerito che tali modelli possano essere usati per dimostrare la consistenza di tutti gli assiomi di [HMS]. Intendiamo sviluppare nei dettagli queste dimostrazioni di consistenza e studiare la semantica delle teorie dei tipi nelle categorie di prefasci di Hofmann. Vorremmo anche confrontare il nostro approccio assiomatico all'analisi sintattica di linguaggi con operatori di legame, a quello categoriale di Plotkin [FPT] e a quello insiemistico di Pitts [GP]. Intendiamo sviluppare dei ``case studies'' di notevoli dimensioni in COQ, non solamente nella verifica di protocolli, e nella metateoria dei calcoli di processi di ordine superiore, ma anche nella computazione esatta sui reali. Quest'ultima sembra essere un'area che possa beneficiare notevolmente dall'uso di assitenti comuterizzati. Gli obiettivi specificisono:
Primo anno: Intendiamo sviluppare numerose codifiche in HOAS di calcoli funzionali e di processi di ordine superiore quali lo spi calcolo, il blu calcolo ed il nu calcolo. Intendiamo svolgere ulteriori esempi di sviluppo in COQ della metateoria di sistemi in HOAS, quali FOL e il lambda calcolo. Cio` dovrebbe permetterci di rifinire il sistema di assiomi per ragionare su contesti in HOAS. Intendiamo inoltre dimostrare la consistenza di tutti gli assiomni in [HMS] mediante modelli di prefasci.
Secondo anno: Intendiamo esplorare ulteriormente i modelli di prefasci per teorie dei tipi e dimostrare la consitenza di tutti gli assiomi della teoria generale dei contesti in HOAS. Intendiamo anche studiare una metodologia per dimostrare l'adeguatezza delle codifiche, basata su questi modelli. Intendiamo inoltre condurre ampi case studies in COQ di derivazione formale della metatoria dei calcoli di processi di ordine superiore e di loro applicazioni.

Lambda calcoli di oggetti (F.Honsell, L.Liquori)

Vogliamo proseguire l'indagine sulle estensioni del lambda calcolo di oggetti di [FHM], lungo le linee di [DGHL]. In [DGHL] Di Gianantonio, Honsell and Liquori hanno introdotto un sistema di tipi piu` potente di quello originale che permette agli oggetti di estendere se stessi. Questo possibilita` sembra molto interessante anche per le sue possibili applicazioni ad altri linguaggi ad oggetti quali Java Ma vi sono molte altre possibili estensioni del sistema di [FHM]. Oltre a rafforzare il sistema di tipi, si puo` estendere il linguaggio garantendo a metodi e messaggi lo status di oggetti diprima classe. Si possono considerare sistemi di tipi espliciti, o un linguaggio con le sostituzioni esplicite invece del lambda calcolo. Si possono considerare inoltre varianti imperative di tutti questi calcoli. E` chiaro che non c'e` ancora ``il'' lambda calcolo di oggetti. E` nostra intenzione cercare di sviluppare una tale teoria quadro per calcoli di oggetti dove ambientare e studiare tutte le possibili varianti di [FHM]. A tal fine intendiamo trarre ispirazione da [DGHL] e dalla recente attivita` di Liquori all'ENS-Lyon [LLL]. In[LLL] viene presentato infatti un ``framework'' generale, Obj+a, per la semantica operazionale di linguaggi di oggetti con particolare attenzione agli aspetti funzionali e imperativi. Piu` specificamente il programma e`:
Primo anno :completare l'indagine teorica del sistema di tipi introdotto in [DGHL], e proseguimento dello sviluppo di Obj+a.
Secondo anno: definizione di un framework generale per il lambda calcoli di oggetti.

Analisi categoriale della coinduzione, analisi algebrica dell'iterazione e analisi della struttura fine di varie categorie di domini (F.Honsell, M.Lenisa, S.Mazzanti, F.Alessi, A.Ciaffaglione)

ci sono numerosi problemi aperti in queste aree. In primo luogo e` ancora da chiarire, eccetto che nel caso di alcuni semplici linguaggi, in che modo la semantica operazionale (finale) si correli alla semantica iniziale, e come e perche' sia possibile in alcuni casi, e non in altri, ottenere delle buone descrizioni coinduttive di semantiche operazionali interessanti. Anche lo stesso problema di come si rapportino i vari approcci categoriali alla coinduzione, ovvero coalgebre, ``span'' di morfismi aperti, fibrazioni, e` ancora aperto. Cosi` come lo e` quello di determinare quanto fedelmente ciascuno di questi approcci riesca a catturare la generalita` della coinduzione insiemistica. Intendiamo affrontare tutti questi problemi e studiare in particolare il potere espressivo e l'ambito di applicabilita`dell'approccio coalgebrico alla coinduzione e alle funzioni coiterative. Intendiamo studiare, al riguardo, come esprimere coalgebricamente vari principi di coinduzione generalizzati basati ad esempio su : bisimulazioni a meno, bisimulazioni non uniformi, bisimulazioni n-arie. Vogliamo studiare anche come estendere il paradigma coalgebrico ai funtori misti. Particolare attenzione verra` dedicata allo studio dell'ambito di applicabilita` di categorie insiemistiche concrete. L'interesse di cio` deriva dal fatto che in tali categorie la sovrastruttura matematica e` ridotta. Sempre nello spirito di studiare principi dimostrativi matematicamente elementari basati sulla sintassi, ma questa volta nella direzione delle relazioni logiche, intendiamo studiare una generalizzazione delle relazioni logiche capace di rendere conto del processo di ``data refinement'' nei linguaggi di ordine superiore. Gli operatori di chisura su preordini saranno studiati sia dal punto di vista della teoria dei grafi sia da quello della teoria delle categorie, al fine di caratterizzare la semantica di costrutti iterativi per programmi non determinsitici e con comportamenti infiniti. Intendiamo inoltre continuare lo studio della struttura fine dei modelli di linguaggi di ordine superiore, quali il lambda calcolo, allo scopo di individuare nuovi principi di coinduzione. Verranno anche affrontati un certo numero di problemi specifici e diversificati realtivi alla semantica matematica dei linguaggi di programmazione. Ad esempio verra` studiata la corrispondenza tra semantica metrica e semantica ordinata, e sarannostudiati sistemi di tipo per catturare proprieta` computazionali. Il programma specifico e`:
Primo anno: Intendiamo sviluppare la teoria matematica delle relazioni prelogiche. Queste sono una generalizzazione delle relazioni logiche chiuse pero` per composizione. Intendiamo inoltre sviluppare altri esempi di descrizioni coalgebriche di principi di coinduzione insiemisitici. Usando varie nozioni categoriali, quali quella di relatore, ad esempio, dovremmo poter raggiungere una certa generalita`. Intendiamo studiare operatori di chiusura su preordini dal punto di vista della teoria dei grafi per specificare la semantica di costrutti iterativi.
Secondo anno: Intendiamo continuarel'indagine dell potere espressivo e dell'ambito di applicazione della Semantica Finale. Intendiamo sviluppare piu` esempi di caratterizzazioni coinduttive di equivalenza osservazionali, specialmente per quanto riguarda linguaggi e calcoli di ordine superiore che manipolano nomi. Intendiamo studiare gli operatori di chiusura dal punto di vista categoriale. Intendiamo infine studiare numerosid esempi su come ``parzializzare'' domini metrici al fine di individuare possibili criteri generali.

Modelli semantici e metodologie di verifica per linguaggi di coordinamento (M.Gabbrielli)

Vari linguaggi di coordinamento esistenti sono basati sul paradigma ``Linda'', nel quale i processi comunicano mediante un unico ``spazio delle tuple''. Recentemente la formulazione originale di Linda [Gel85] e' stata estesa per trattare applicazioni distribuite ed per modellare la mobilita' di processi [DFP98]. Si studieranno quindi i nuovi aspetti semantici che sorgono nel contesto di tali estensioni, con particolare attenzione alle metodologie di verifica ed alle problematiche di sicurezza. Il programma specifico e`:
Primo anno: Si studieranno modelli semantici per alcuni linguaggi di coordinamento proposti recentemente e basati su estensioni del paradigma ``Linda''. Dato che tale paradigma ha varie caratteristiche in comune con la programmazione concorrente con vincoli (ccp), si cerchera' di adattare ad esso i modelli semantici (fully abstract) precedentemente sviluppati per estensioni temporizzate di ccp [BGM97]. Inoltre si studiera' il potere espressivo delle varie estensioni di Linda proposte, con particolare riguardo alle primitive aggiunte per descrivere mobilita' di processi. Infine si analizzera' la possibilita' di integrare programmazione concorrente con vincoli e linguaggi basati su Linda.
Secondo anno: Si studieranno metodologie di verifica per linguaggi di coordinamento basati su Linda che supportino la mobilita' di processi. In particolare si considereranno tecniche basate sulla logica temporale per affrontare problematiche di sicurezza.

Automi per sistemi in tempo reale(A.Peron)

Si e' interessati ad individuare modelli di automi in grado di fornire descrizioni sintetiche di sistemi in tempo reale. Oggetto dello studio sara' l'influsso sulla complessita' della specifica dei diversi modi di esprimere il tempo e le condizioni temporali in varie classi di automi temporizzati (e.g. Timed automata, Timed Communicating automata etc.). Si intende introdurre anche una classe di automi capaci di reagire alla lettura di un simbolo con una sequenza possibilmente non unitaria di transizioni. (L'estensione trova ragione nella necessita' di rappresentare semplicemente led sequenze di transizioni istantanee dei sistemi reattivi sincroni.) Si vuole verificare se anche questa caratteristica influenza la complessita' della descrizione. Si vogliono studiare, inoltre, tecniche di ritemporizzazione. Per quanto concerne la relazione tra automi e logica, si intende introdurre il corrispettivo del frammento al primo ordine della logica degli infiniti domini approssimabili definita in [MPP99]. Ci si attende che questa logica modale sia una estensione (propria) della ben nota Propositional Linear Temporal Logic e sia anche la controparte logica della classe dei linguaggi accettati da automi sistolici ad albero e definibili al primo ordine. Inoltre, si affrontera' il problema di individuare una caratterizzazione logica di automi sincroni di potere espressivo maggiore a quelli considerati. Il programma specifico e` Primo anno: Si studiera' la complessita' della rappresentazione di varie classi di automi temporizzati e si fornira' la caratterizzazione modale del frammento al primo ordine della logica definita in [MPP99].
Secondo anno: Si introdurranno automi temporizzati con sequenze istantanee di transizioni e si studieranno, per questo modello, tecniche di raffinamento. Si studieranno caratterizzazioni logiche per altre classi di automi sincroni.

Testo inglese

As we did above in illustrating the background to our proposed research, we shall illustrate the specific research activitiy proposed by the group in Udine by dividing it into 5 main areas, namely:

• theory, applications, and experiment of proof development environments based on type theoretic Logical Frameworks
  
• Lambda Calculi of objects
  
• categorical analysis of coinduction, algebraic analysis of
  iteration and fine analysis of categories of domains
  
• semantic models and verification methodologies for coordination languages
  
• real time automata.
  

For each of the above we will discuss the broad objectives of the proposed research and give a more detailed work plan.

Theory, applications, and experiments of proof development environment based on type theoretic Logical Frameworks

Little experiment in type theoretic Logical Frameworks, has been carried out so far for (higher order) process calculi for protocol specification and verification. Building on our recent successful treatment in [HMS] of the archetype of such calculi, i.e. the pi-calculus of Milner et al [MPW], we intend to develop and experiment with HOAS implemetations in COQ [COQ] of other such calculi e.g. the spi calculus [AM] and the blue calculus [Bou]. Due to the complex nature of the binding operators featured by these systems, both designers and users of such systems should benefit from our type theoretical investigations of the syntax and our implementations. Ultimately these experiments should lead to a comforatbale computer assisted workbench, based on Coq, for protocol and security verification. These experiments should lead also to the design of a general methodology for representing and reasoning on nominal calculi and other higher order calculi in HOAS.
In order to be able to carry out the necessary metatheoretic reasoning, however it is likely that we will have to extend existing type theoretic metalanguages with new axioms and induction-recursion-coinduction principles. Type theory has, in fact, a limited power in supporting metatheoretic reasoning over systems in HOAS. Our approach, as pioneered on [MMS], is that of introducing suitable axiom packages. This allows us to maintain the transparency of the encoding and keeps the matheamtical sovrastrucutre low. Our ultimate goal in this respect is to define a consistent and complete axiom system of metalogical principles for reasoning on arbitrary systems presented in HOAS. However so doing we will have to deal with the issue of consistency of the overall system. Recently Hoffman [Hof] has showed how functor categories can be fuitfully put to use in modeling Intuitionsitic Type Theories and hinted at how such models could be used to prove consistency of non-standard induction principles and axiom systems such as the ones we introduce. We intend therefore to develop full consistency proofs for our axioms systesm using presheaf models in the style of Hofmann. We would like also to compare our axiomatic approach to reasoning on languages, with bindings and other operators on variables and names, to the categorical one of Plotkin [FPT]and the set-thoeretical one of Pitts [GP]. Applications of the presheaf technique to proofs of adequacy will be explored also.
We expect to carry out some significant case studies using COQ not only on comunication protocol verification, and the metathoery of higher order process calculi, but also on exact real number computation. This is an area which can benefit greatly from computer assistence in its formal developments.
The detailed workplan is as follows:
First year: Develop more encodings in HOAS of functional calculi and, possibly higher order, process calculi such as the spi calculus, the blue calculus and the nu-calculus. Carry out more formal metatheoretic developments for such systems and other systems in HOAS such as FOL and lambda calculus. We hope thus to be able to finalize our metatheoretic axioms for reasoning on contexts over systems in HOAS. Prove formally the consistency of the axioms introduced in [MMS] using presheaf models.
Second year: We plan to explore further functor category models of type theory and prove the consistency of all our axioms for contexts in HOAS. We intend to investigate these models also for streamlining proofs of adequacy.
Some large case studies on the metatheory and applications of higher order process calculi will be carried out.

Lambda calculi of Objects

We want to carry on the investigation of significant extensions of the original lambda calculus of objects of [FHM] along the lines of [DGHL]. In [DGHL] Di Gianantonio, Honsell and Liquori introduced a strengthening of the original type system of that calculus which allows objects to extend themselves upon receiving a message. This is an interesting possibility, which has potential applications to practical object oriented languages sush as Java. But extensions of the original lambda calculus of objects can go in various other directions. Not only, one can strengthen the type system. One can also extend the language so as to allow methods and messages to be first class objects; one can consider explicitly typed versions of the system, or replace the lambda calculus with a calculus of explicit substitutions. Furthermore one can introduce imperative versions of all these. It is apparent that there is no general lambda calculus of objects yet. One of the most important research problems in this area is to try to introduce and develop a framework language where to accomodate all these variants. It is our intention to try to develop such a general framework of objects, building both on [DGHL] and the current work that Liquori is doing at ENS-Lyon [LLL]. In [LLL] Liquori studies a general framework, Obj+a, for the foundation of operational (small step) semantics of object-based languages with an emphasis on functional and imperative issues.
More specifically our work plan is as follows:
First year: complete the theoretical investigation of the type system introduced in [DGHL], and pursue the investigation of Obj+a.
Second year: design a general framework language for lambda calculi of objects.

Categorical analysis of coinduction, algebraic analysis of iteration and fine analysis of categories of domains (F.Honsell, M.Lenisa, S.Mazzanti, F.Alessi, A.Ciaffaglione)

There are many open problems in this area. First of all it is still unclear, apart form very simple languages, how operational (final) semantics exactly relates to inital semantics, and why and how can we get good coinductive characterizations of interesting semantical equivalences. Even the problem of how do the various categorical approaches to coinduction (e.g. coalgebras, span of open maps, fibrations) relate to one another and how much can they capture of the generality of set theoretic coinduction is still far form being settled. We intend to investigate such issues and in particular to study the expressive power and scope of the coalgebraic approach to coinduction and coiterative functions. In particular we intend to consider how to express various generalized coinduction principles based on e.g. bisimulation up-to principles, non uniform bisimulations, n-ary bisimulations. We intend to address also the problem of how to extend the coalgebraic paradigm to mixed functors. We shall also pursue our investigation of the scope of final semantics in elementary set-theoretic categories.
Still in the spirit of syntactically based proof principles, but more in the line of logical relations, we intend also to develop a theory of generalized logical relations suitable for accounting the process of data refinement inhigher order languages. Closure relations on preorders will be investigated both in the style of graph theory and in the style of category theory, to construct a semantics of iterative constructs for non terminating and non deterministic programming. We intend to continue the investigation of the fine strucutre of domain models of higher order programming languages such as lambda calculus, with the purpose of deriving new coinduction prniciples. A number of related specific semantical problems will be also addressed, e.g.: the correspndence between ordered and metric semantics, and the characterization of properties using type assignment systems. More specifically the workplan in this area is the following:
First year: we intend to develop the mathematical theory of prelogical relations, a suitable genralizations of logical relations, closed under composition. Develop more case studies in final semantics and in coagebraic descriptions of coinduction principles, using categorical notions, such as that of relator, for achieving generality. Study closure operators on preorders in the style of graph theory in order to construct a semantics of iterative constructs for non terminating and non deterministic programming.
Second year: We intend to continue with the investigation of the scope and expressive power of Final Semantics. Develop more case studies in coinductive characterizations of operational equivalences, especially in connection with higher order languages and calculi, possibly involving names. Investigate closure operators categorically. Investigate general principles and more case studies in partializing metric domains.

Semantic models and verification methodologies for coordination languages (M.Gabbrielli)

Several existing coordination languages are based on the ``Linda'' paradigm, where processes communicate via a unique global ``tuple space'' on which a few primitive operations are defined. Recently the original formulation of Linda [Gel] has been extended to deal with distributed applications and to model mobility of processes [DFP]. We plan to investigate the new semantic and proof-theoretic issues which arise in the context of these extensions, with a particular attention to security related problems.
First year: we will study semantic models for some existing coordination languages based on extensions of the ``Linda'' paradigm. Since such a paradigm is similar to concurrent constraint programming (ccp), we plan to base our study on previous results we obtained for timed ccp [BGM97]. We will also investigate the expressive power of several existing extensions of Linda, and in particular we will consider the primitives which have been introduced for describing mobile agents. Finally we will consider possible integrations of ccp with Linda based coordination languages.
Second year: we will concentrate on verification methodologies for Linda based languages for mobile computing. In particular we will study techniques based on temporal logics for dealing with security issues.

Real time automata (A.Peron)

Our investigation will focus on various classes of timed and synchronous automata aimed at evaluating, under suitable criteria, their ability of describing real time systems. A criterion of evaluation will be "succinctness" of description. Harel and Drusinsky proved that (finite state) automata endowed with parallelism and communication features allow an exponential saving when compared with usual sequential finite state automata. In the same line, we shall consider whether different ways of representing time and different ways of expressing temporal constraints in varoius classes of automata (e.g. Timed automata, Timed Communicating automata etc.) affect the complexity of the specification. We want also to introduce automata able to read a symbol and to react by taking sequences of transitions (instead of one only transition, as usual). (This extension is motivated by the need of easily modeling instantaneous reactions in synchronous formalisms.) We want to investigate whether this new feature affects the complexity of the specification. For this extension we shall study retiming techniques. As far as the connection between automata and logic, we are also interested in investigating the logical counterpart of suitable classes of synchronous automata. We want to introduce the modal counterpart of the first order fragment of the logic of infinitely coarsable temporal domains in [MPP]. This modal counterpart is expected to be a (proper) extension of the well known Propositional Linear Temporal Logic as well as the (modal) logic counterpart of the class of first order definable languages accepted by systolic binary tree automata. Finally, we shall investigate the problem of defining a logic characterisation of other (more expressive) classes of synchronous automata.
First year: we shall study succinctness of different classes of timed automata and we shall provide the modal characterisation of the first order
fragment of the logic of infinitely coarsable temporal domains in [MPP99].
Second year: we shall introduce automata with instantaneous firing of sequences of transitions and we shall study, for this model, retiming techniques. We shall investigate the problem of defining a logic characterisation of other (more expressive) classes of synchronous automata.

Nº	Anno di acquisizione	Descrizione
		Testo italiano	Testo inglese
1.	1995	SUN - Sparc Station 20	UN - Sparc Station 20
2.	1998	PC Scenic Celsius 2000 - Siemens	PC Scenic Celsius 2000 - Siemens
3.	1998	PC Pentium 200 MMX	PC Pentium 200 MMX
4.	1998	PC Pentium 200 MMX	PC Pentium 200 MMX
5.	1998	PC Pentium 200 MMX	PC Pentium 200 MMX

Voce di spesa	Spesa		Descrizione
	M£	Euro	Testo italiano	Testo unglese
Materiale inventariabile	20	10329	hard disks, PC workstations, libri, stampanti	hard disks, PC workstations, printers
Grandi Attrezzature
Materiale di consumo e funzionamento	8	4132	contratti di manutenzione, fotocopie, telefono, spedizioni e posta, cancelleria	maintenance contracts, telephone, photocopies, mail
Spese per calcolo ed elaborazione dati	2	1033	account Centro di Calcolo	Computer Centre accounts
Personale a contratto	30	15494	un assegnista di ricerca (con titolo di dottorato di ricerca) per un anno da dedicare allo studio della teoria e alla sperimentazione di Logical Frameworks	one year post-doctoral research assistant to work on thoery and applications of logical frameworks
Servizi esterni
Missioni	45	23241	partecipazione ai principali convegni del settore, e.g. LICS,CONCUR,ICALP,ETAPS,CSL, etc; partecipazione a workshops tematici e visite brevi presso universita` e centri di ricerca in Europa e Nord America; visite brevi presso altre unita` del progetto	particpation to international conferences in the area e.g.: LICS, ICALP, ETAPS, CONCUR, CSL, etc; Particpation to workshops and short visits to universities and research centres in Europe and North America; short visits to other sites of the project
Altro	7	3615	seminari di visitatori; organizzazione convegni	seminars fees for visiting professors, scholars and scientists; organization of small workshops

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

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