Area Scientifico Disciplinare:

• Scienze Matematiche

Testo italiano

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

Testo inglese

MONTANARI	UGO
(cognome)	(nome)

Universita' degli Studi di PISA	Facolta' di SCIENZE MATEMATICHE FISICHE e NATURALI
(università)	(facoltà)

K05B	DIP. INFORMATICA
(settore scient.discipl.)	(Dipartimento/Istituto)

ugo@di.unipi.it
(email)

HONSELL	FURIO
(cognome)	(nome)

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

Universita' degli Studi di UDINE	Facolta' di SCIENZE MATEMATICHE FISICHE e NATURALI
(università)	(facoltà)

K05B	DIP. MATEMATICA E INFORMATICA
(settore scient.discipl.)	(Dipartimento/Istituto)

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

K05B

Testo italiano

Testo inglese

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 del ``editorial board'' della rivista internazionale MSCS. Membo permanente del 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 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
						1 ANNO	2 ANNO
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
						1 ANNO	2 ANNO

1.10.3. Titolari di assegni di ricerca:

Nº	COGNOME	NOME	DIPARTIMENTO/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	DIPARTIMENTO/ISTITUTO	ANNO DEL TITOLO	MESI UOMO
1.	CIAFFAGLIONE	ALBERTO	MATEMATICA E INFORMATICA		12
2.	FRANCO	GIANLUCA	MATEMATICA E INFORMATICA		8
3.	SCAGNETTO	IVAN	MATEMATICA E INFORMATICA		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	ENTE	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 basati su Type Theoretic Logical Frameworks, per assistere nell'utilizzo di metodi formali. Sviluppo e studio di sistemi formali per la specifica, l'analisi e la verifica di Lambda Calcoli di oggetti, sistemi concorrenti, linguaggi di coordinazione.

Testo inglese

Testo italiano

Testo inglese

Theory, applications, and experiments 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 ]. One of the most interesting possibilities offered by type theory when it used as as a specification language for formal systesm is that of using Higher Order Abstract Syntax (HOAS) in the specification of the object syntax and its operational semantics. HOAS, in fact, allows to express the syntax and the operational semantics of formal calculi involving operators on variables, names,
and locations in a uniform and algebraic way. HOAS is therefore extremely valuable both as a formalism for capturing certain context sensitive aspects of syntax and operational semantics, and for setting a standard on how scope and alpha conversion should be handled in formal systems. Pragmatically HOAS allows to delegate to the system all the concerns over alpha-conversion, scope and substitution. Another interesting possibility offered by these Logical Frameworks is to allow/urge 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 extremely natural and beneficial for practical use in mechanized formal reasoning. However, such reforrmualtions are often difficult toachieve.
A case in point concerns the higher order process and nominal calculi e.g. [blu,spi] which have been recently introduced for verification of protocols, and analysis of authentication, and security issues. Because of the complex nature of the operators on variables and names, such systems would greatly benefit form HOAS anlyses and Logical framework based proof development environments would be particularly suited to them. However, up to now, very little experiment has been carried out with them along these lines.
The Udine group has international reputation in tailoring formal systems for Type Theoretic Logical Frameworks [NDDL,ML].
A problematic theoretical issue 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 induction principles and other axioms in Higher Order Intuitionistic Type Theories. Some of these principles are precisely those which where introduced in [HMS] for carrying out successfully metatheoreitc reasoning in Logical Frameworks over systems presented in HOAS. Indipendently but simultaneously also G.Plotkin et al., and A.Pitts et al. have used ideas based on functor categories for structuring mathematically syntax of systems involving binders or for suggesting new frameworks for HOAS. There seeems interesting work to be done in comparing the axiomatic methodology of {HMS] with the functor theoretic approach.

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

Since the paper [FHM] by Fisher-Honsell-Mitchell, there has been growing interest in calculi for objects, i.e. on 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. By so doing we can in fact capitalize on the extensive theoretical work that has been carried out over the
years in lambda calculus because of its principled and mathematically tractable syntax and semantics. In [FHM] a lambda calculus of objects has been introduced together with a sound type assignment system which allows to check statically if errors of the kind ``message-not-understood'' will not arise at run time. This calculus formalizes a small delegation-based language which contains both
lambda calculus and object primitives for creating, updating, and sending messages to objects. Since then a number of extensions, or variants of the original language and type system, have been investigated by many researchers in this prop[osal, including Liquori[BBDL98,Liq98], 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)

In recent years [BMMR] [Rut96], there has been growing interest on coalgebraic and coinducitve methods in connection with the specification of operational semantics of programming languages. Such methods provide in fact powerful proof principles for reasoning on the infinite behaviour of programs, processes, and objects of higher order datatypes (e.g. exact reals}. Especially when such methods are used in connection with techniques based on logical relations, they allow to reason on such infinite objects in a mathematically principled and highly structured way, just by considering their 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 sometime [HL95,Len96,HLMP98], especially in set theoretic categories based on non-wellfounded sets. The whole area of syntactically based operational methods, however, appears to be full of yet unresolved general questions.
S. Mazzanti [Ma95,Ma97] has been investigating the old, but surprisingly not yet completely resolved, problem of characterizing iterative functions on data types for many years.
F.Honsell, M.Lenisa [HL98b] and F.Alessi [ABBR95] have been investigating various metric and ordered categories of domains for the past ten years. There are still many open questions especially with respect to the completeness of such categories and the possibility of providing coinductive characterizations of observational equalities. An important and general problem is also that of studying the possibility of embedding metric spaces in effective domains.

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

Concurrent constraint programming (ccp) [SRP901 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 the notions of communication and synchronization can be formalized logical terms, one can obtain in a rather straightforward way a proof-theory [BGMP97] and analysis tools [FGMP93] for ccp. Recently ccp has been extended for real-time applications (by introducing a notion of clock and suitable primitives) [SJG94,BGM97], 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 semantic models can be used to study existing languages.

Real time automata (A.Peron)

Testo italiano

K. Fisher, F. Honsell, J. Mitchell
A Lambda Calculus of Objects and Method Specification
Nordic Journal of Computing, Vol. 1, pp. 3-37, 1994.

F.Honsell, M. Lenisa, U. Montanari, and M. Pistore
Final Semantics for the pi-calculus
Programming Concepts and Methods PROCOMET'98,Chapman & Hall, 1998. p.225-243

• [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
  
• [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
  
• [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.
  
• [FGMP] 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.
  
• [FGMP] M. Falaschi, M. Gabbrielli, K. Marriott and C. Palamidessi;
  Confluence in Concurrent Constraint Programming. Theoretical Computer Science, 183, pp. 281-315, 1997.
  
• [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.
  
• [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]
  
• [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 inglese

Testo italiano

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 experiments of proof development environments based on Type Theoretic Logical Frameworks
  
• Lambda Calculi of objects
  
• Categorical and Logical Analysis of Coinduction and other semantical problems
  
• 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, possibly, give a more detailed work plan.

Theory, applications, and experiments of proof development environments 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 of other such calculi e.g. the spi calculus [AM] and the blue calculus [Bou]. Both designers and users of these calculi should therefore benefit from our type theoretical investigations and implementations. Ultimately these 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 induction-recursion-coinduction principles to overcome the limitations of type theory when dealing with HOAS. Our approach, as pioneered on [MMS], is that of introducing suitable axiom packages. 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. This approach allows us to maintain the transparency of the encoding and keeps the matheamtical sovrastrucutre low. However it raises the issue of proving the consistency of the axioms. 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 axioms systems 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 and the set-thoeretical one of Pitts. Applications of the presheaf technique to proofs of adequacy will also be explored.
We expect to carry out some significant case studies using COQ [COQ] not only on comunication protocol verification, and the metathoery of higher order process calculi, but also on exact real number computation, which is an area which can benefit also form computer assistenca in its formal developments.
The detailed workplan is as follows:
First year: Develop more encodings in HOAS of funcional calculi and, possibly higher order, process calculi such as the spi calculus of 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 about contexts for 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 including some on the metathoery 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 a very powerful extension, 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 nad 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 ofobjects 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 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-theoreitc 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 in higher order languages.
We intend to continue the investigate the fine strucutre of domain models of higher order programming languages such as lambda calculus, with the purpose of deriving new coinductive characterizations of coinduction prnciples.
A number of specific and diverse related semantical and problems ranging from the correspndence between ordered and metric semantics to the characterization of properties using type assignment systems will be also addressed.
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. Develop more case studies in final semantics and in coagebraic and descriptions of coinduction principles e.g. using the categorical notion of relator for achieving generality in providing coalgebraic accounts of set-theoretic coinduction principles. Study closure relations as a tool for characterizing the iterative behaviour of non
determinsitic programs.
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 general principles and more case studies in partializing metric domains.
In the 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.
II Year
In the 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. We are also interested in investigating the logical counterpart of suitable classes of synchronous automata. The logical theory of binary tree systolic automata has been recently exploited 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. We intend to prove that the modal counterpart of the first order fragment of that theory is a proper extension of Propositional Linear Temporal Logic which preserve the property of elementar decidability.

Nº	Anno di acquisizione	Descrizione
		Testo italiano	Testo inglese

Voce di spesa	Spesa			Descrizione
	M£	$	Euro	Testo italiano	Testo unglese
Materiale inventariabile	20	11224	10329	hard disks, PC workstations, libri, stampanti	hard disks, PC workstations, printers
Grandi Attrezzature
Materiale di consumo e funzionamento	8	4489	4132	contratti di manutenzione, fotocopie, telefono, spedizioni e posta, cancelleria	maintenance contracts, telephone, photocopies, mail
Spese per calcolo ed elaborazione dati	2	1122	1033	account centro di calcolo	Computer Centre accounts
Personale a contratto	30	16835	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	25253	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	3928	3615	seminari di visitatori, organizzazione convegni	seminars fees of visiting professors, scholars and scientists, organization of small workshops

4.1.1. Altro:

4.2.1. Altro:

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