Parte I
MINISTERO DELL'UNIVERSITA` E DELLA RICERCA SCIENTIFICA E TECNOLOGICA
DIPARTIMENTO AFFARI ECONOMICI
PROGRAMMI DI RICERCA SCIENTIFICA DI RILEVANTE INTERESSE NAZIONALE
RICHIESTA DI COFINANZIAMENTO
(DM n. 811 del 3 dicembre 1998)
PROGETTO DI UNA UNITA` DI RICERCA - MODELLO B
Anno 1999 - prot. ???? (attribuito dal sistema)

1.1 Programma di Ricerca di tipo: interuniversitario

Area Scientifico Disciplinare Scienze Matematiche (100%)

1.2 Durata del Programma di Ricerca : 24 mesi

1.3 Titolo del Programma di Ricerca (bilingue):
Teoria della Concorrenza, Linguaggi di Ordine Superiore e Strutture di Tipi

1.4 Coordinatore Scientifico del Programma di Ricerca:
Montanari Ugo
Universita` Pisa, Scienze MFN
K05B, Dipartimento Informatica

1.5 Responsabile Scientifico dell'Unita` di Ricerca
Furio Honsell
Professore Ordinario, K05B, 20/08/1958,
Universita` Udine, Scienze MFN
Dipartimento Matematica e Informatica
0432558467, 0432558499, honsell@dimi.uniud.it

1.6 Settori scientifico-disciplinari interessati dal Programma di Ricerca:
K05B

1.7 Parole chiave (al piu' 6)
Logical Frameworks, Higher Order Abstract Syntax, Lambda Calculi of Objects,
Coalgebraic Methods
Coordination languages, concurrent constraint programming,
verification, security.

1.8 Curriculum scientifico del Responsabile Scientifico dell'Unita` di
Ricerca: (max. 10 righe, bilingue)

Laurea in Mathematics (1981, Pisa), Diploma In Matematica (1983,Scuola
Normale Superiore, Pisa) Science (1988, Edinburgh), full professor
since 1990. Research and academic postions previously held in Torino
and Edinburgh. 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, foundations of
informatics. Research contributions: non-wellfounded set
theory, models and theories of lambda calculus, logical frameworks
base on typed theory, lambda calculus of objects.

1.9 Pubblicazioni scientifiche piu` significative del Responsabile
Scientifico dell'Unita` di Ricerca
(massimo 5, le piu` recenti e pertinenti il programma)

R. Harper, F. Honsell, G. Plotkin:
A framework for Defining Logics.
Journal of ACM,Vol. 40, No. 1, (1993), 143-184.

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. Miculan, I. Scagnetto.
pi-calculus in (Co)Inductive Type Theory
aparira` su Theoretical Computer Science.

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

P.Di Gianantonio, F.Honsell, and L.Liquori
A Lambda Calculus of Objects with Self-Inflicted Extension
ACM-SIGPLAN OOPSLA-98, Vol 33, Number 10, October 1998, pp 166--178, ACM Press.

1.10 Risorse umane impegnabili nel Programma dell'Unita` di Ricerca

1.10.1 Personale universitario dell'Universita` sede dell'Unita` di Ricerca

Cognome Nome Dip. qualifica settore mesi uomo
Alessi Fabio DIMI RC K05B 11+8
Gabbrielli Maurizio DIMI PA K05B 11+8
Honsell Furio DIMI PO K05B 11+8
MAzzanti Stefano DIMI RC K05B 11+8
Peron Adriano DIMI RC K05B 11+8

1.10.2 Personale universitario di altre Universita`

1.10.3 Titolari di borse ex L.398/89 art.4 (post-dottorato e specializzazione)

Cognome Nome Dip. Anno del titolo mesi uomo

1.10.4 Titolari di borse per Dottorati di Ricerca

Cognome Nome Sede amm. Dip. ciclo mesi uomo
Ciaffaglione Alberto Udine DIMI 14 4+4
Franco Gianluca Udine DIMI 12 4+4
Scagnetto Ivan Udine DIMI 13 6+8

1.10.5 Personale a contratto da destinare a questo specifico programma

qualifica costo previsto mesi uomo
assegnista 30 11

1.10.6 Personale extrauniversitario dipendente da altri Enti

Cognome Nome ente qualifica mesi uomo
Lenisa Marina LFCS-Edinburgh Research Fellow 3+8
Liquori Luigi ENS-Lyon attache de recherche 3+8
Miculan Marino INFN-Trieste tecnologo 3+3

Parte II
2.1 Titolo specifico del programma svolto dall'Unita` di Ricerca:

2.2 Base di partenza scientifica (max. 1 pag.)

represent programs

2.3 Descrizione del programma e dei compiti dell'Unita` di Ricerca (max 2 pagg.)

Theory, applications, and experiments of Logical Frameworks based on Type Theory
Lambda Calculi of objects
Categorical Analysis of Coinduction
Semantic models and verification methodologies for coordination languages
Real time automata

Theory, applications, and experiments of Logical Frameworks based
on Type Theories (F.Honsell, F.Alessi, M.Miculan, I.Scagnetto,
A.Ciaffaglione)

BACKGROUND Since the late eighties 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 (e.g. binders, restriction ops., ``new name'' ops.,
assignments) 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 alpha conversion should be handled in formal
systems. Pragmatically HOAS allows to delegate to the system all the
concerns over alpha-conversion and substitution. However, even in
powerful Logical Frameworks such as COQ, metatheoretic reasoning on
HOAS is limited. Another interesting possibility offered by these
Logical Frameworks is that they basically urge the user to present his
system in a natural deduction style, thereby making explicit the
dependency between assumptions and conclusions. This suggests
formulations of logical systems which are extremely natural for
practical use in mechanized formal reasoning. The Udine group has a
world eputation in tailoring formal systems for such Logical
Frameworks [NDDL,ML]. On a more pragmatic basis although there has
been a growing use of higher order process calculi such as the
[blue,spi] for verification of protocols, authentication, security,
little experiment has been carried out with the proof assitants derived form these Logical Frameworks.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. Such principles are
precisely those which seem necessary for carrying out successfully
metatheoreitc reasoning in Logical Frameworks over logical systems and
other calculi presented in Higher Order Abstract Syntax (HOAS). For
instance some of the principles introduced in [MMS] for developing the
metathoery of the pi-calculus are among these. 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.

OBJECTIVES

Develop a general theory for representing nominal calculi and other
higher order process calculi in HOAS. Develop a system of Metalogical
principles forreasoning on systems presented in HOAS. Carry out large
case studies using COQ on Exact real number computation, comunication
protocol verification, and the metathoery of higher order process calculi.
Investigate the theory of presheaf models for coinductive type theories
in the style of Hofmann, and explore its applications to Logical Frameworks
based on HOAS, such as consistency or adequacy.

First year: Develop more encodings in HOAS of funcional calculi and,
possibly higher order, process calculi such as the spi calculus of
Abadi et al. and the blue calculus of Boudal et al. Carry outfurther
formal theory developments for such systems. We hope to be able to
develop a general metathoery for reasoning about contexts for such
systems, which combine a complex binding structure with mechanisms for
``new'' name generation. Ultimately this should provide a comforatbale
proof developoment environment for verfying suh applications such as
protocol and security verification.Prove formally the consistency of
the axioms introduced in [MMS] using presheaf models.

Second year: It is likely that we will have to extend existing type
theoretic metalanguages with new induction-recursion-coinduction
principles. Our approach, as pioneered on [MMS], is that of
introducing suitable axiom packages. This approach allows us to
maintain the transparency of the encoding and keeps the matheamtical
sovrastrucutre low. This approach however raises the problem of
proving the consistency the axioms. Intuitively simple reflection
arguments are enough. 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 introduced abova. We plan to explore functor category models
of type theory in this respect, trying to prove the consistency of a
general and uniform proof environment for higher order nominal
calculi.Investigate the technique based on presheafs for provinig
adequacy of encodings.

REFERENCES

[HHP] R. Harper, F. Honsell, G. Plotkin:
A framework for Defining Logics.
Journal of ACM,Vol. 40, No. 1, (1993), 143-184.

[MMS] F. Honsell, M. Miculan, I. Scagnetto.
pi-calculus in (Co)Inductive Type Theory
aparira` su Theoretical Computer Science.

[MPW]

[Hof] M.Hofmann: Semantical Analysis of higher order abstract syntax
to appear in LICS'99

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

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 to create, update, and send
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 project, including Liquori[BBDL98,Liq98], and many
typing disciplines which now cover subtypes and incomplete objects
have been considered.

OBJECTIVES

We want to carry on the investigation of significant extensions of the
original lambda calculus of objects along the lines of [DGHL98]. In
[DGHL] Di Gianantonio Honsell and Liquori introduced a strengthening
of the original type system 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 direction. Not only, one can strengthen the type system;
one can 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 study 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 on
[LLL]. Currently Liquori at ENS of Lyon is studying 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.

1st year Complete the theoretical investigation of the type system
introduced in [DGHL98], and pursue the investigation of
Obj+a.

2nd year Design a general framework language for lambda calculi of
objects.

REFERENCES

[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 Proc. of the 4th ACM Conference on Computer and
Communications Security, pp. 36-47, ACM Press. Extended version in
Information and Computation 148(1) pp. 1-70, 1999. Academic Press.

[Bou] G. Boudol: The pi-calculus in direct style Proc. of POPL 97,
pp. 228-241, 1997, ACM Press. Extended version in Higher-Order and
Symbolic Computation Vol 11, pp. 177-208, 1998

[BBDL98]V.Bono, M.Bugliesi, M.Dezani and L.Liquori: A Subtyping for
Extendible, Incomplete Objects. Fundamenta Informaticae. to appear

[DGHL98] 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.

[Liq98] 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.

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

BACKGROUND

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 problem of
characterizing iterative functions on data types..

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.

OBJECTIVES

It is still unclear how operational (final semantics) relates to
inital semantics apart form very simple languages; or 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. We intend to
investigate such issues and in particular to study the expressive
power 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.

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 with the purpose of
deriving new coinductivecharacterizations of coinduction prnciples.

1st 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.

2nd 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.

REFERENCES

es [ABBR95] 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.

[HL95] F. Honsell, M. Lenisa; Final semantics for untyped lambda calculus,
TLCA'95, Springer LNCS 902, 1995.

[HL95] M. Lenisa; Final semantics for a higher order concurrent
language, CAAP'96, Springer LNCS 1059. 1996

[BMRR] B.Jacobs et al. : Proc. 1st Wkshp. on coalgebraic methods in
CS, ENTCS 11, 1998.

[HL98b]F. Honsell, M. Lenisa
Semantical Analysis of Perpetual Strategies in lambda-calculus
to appear in Theoretical Computer Science 213 , 1998.

[HLMP98] 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.

[Rut96] J.J.M.M. Rutten: Universal coalgebra: a theory of systems, CWI
CS-R9652,1996.

[Len98] Marina Lenisa A Coinductive Logical System for Bisimulation
Equivalence of Circular Objects, to appear in ETAPS '99

[Len98] Marina Lenisa Themes in Final Semantics Ph.D. Thesis TD-6/98,
March 1998. Dipartimento di Informatica, Universit� di Pisa.

[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.

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

BACKGROUND

The group in Udine has specific competence also in the field of coordination
languages. In particular, in the last few years we have studied
semantic models and proof-theory for concurrent constraint programming
(ccp) [FGMP7,BGMP97] and for timed extensions of ccp [BGM97].
Furthermore, we have studied the expressive power of these extensions
by formally comparing them to the original language [BGM97]. The results
obtained in these works could be useful for studying some recent
coordination languages. In fact, several proposal in this field are
based on the Linda paradigm which has some similarities with ccp.

OBJECTIVES

As far as coordination languages, the group in Udine will study semantic
models and verification methodologies for some existing 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 ccp and to investigate
possible integrations of the two paradigms. We also plan to use logic
based techniques for dealing with security issues in the context of
coordination languages which support process mobility.

1st year:

2nd year:

REFERENCES

[BGMP97]
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.

[BGM97]
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.

[FGMP97]
M. Falaschi, M. Gabbrielli, K. Marriott and C. Palamidessi.
\newblock Confluence in Concurrent Constraint Programming.
Theoretical Computer Science, 183, pp. 281-315, 1997.

Real time automata (A.Peron)

BACKGORUND

OBJECTIVES

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.

1st year:

2nd year:

REFERENCES

[MP9?] A. Monti and A. Peron, Systolic Tree omega-Languages: The
Operational and the Logical View, Theoretical Computer Science, to appear.

[APP] 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.

[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.

2.4 Descrizione delle attrezzature gia` disponibili ed utilizzabili per
la ricerca proposta

2.5 Descrizione della richiesta di Grandi attrezzature (GA)

Parte III
3.1 Costo complessivo del Programma dell'Unita` di Ricerca (in milioni di lire)

Voce di spesa spesa descrizione
Materiale inventariabile 20 hardware, libri
Grandi Attrezzature
Materiale di consumo 7 telefono, posta, fotocopie
Spese per calcolo ed elaborazione dati 10 account e manutenzione
Personale a contratto 30 assegnista per 1 anno
Servizi esterni
Missioni 53 convegni, collaborazione scientifica
Altro 10 invitati e seminari

Costo complessivo del Programma dell'Unita` di Ricerca
130
Costo minimo per garantire la possibilita` di verifica dei risultati
110
Fondi disponibili (RD)
12,25
Fondi acquisibili (RA)
25,25
Cofinanziamento richiesto al MURST
96,5

Parte IV

4.1 Risorse finanziarie gia` disponibili all?atto della domanda e utilizzabili
a sostegno del Programma (tutte le cifre vanno espresse in milioni)

QUADRO RD

Provenienza anno di ass. importo disp. nome Resp. Naz.
Universita` 1999
Dipartimento 1993 in poi
MURST(ex 40%) 1995-1996
CNR
Unione Europea 1998
Altro
TOTALE

4.1.1 Altro (dettagliare origine ed importi)

4.2 Risorse finanziarie acquisibili in data successiva a quella della
domanda e utilizzabili a sostegno del programma nell'ambito della durata
prevista (tutte le cifre vanno espresse in milioni)

QUADRO RA

Provenienza anno della domanda stato di appr. disponibilita`
Universita` 1999 C
Dipartimento
CNR
Unione Europea
Altro
TOTALE

Nota: A=in fase di presentazione; B=accettato; C=in fase di negoziazione;
D=contratto stipulato; E=finanziato; F=disponibile in caso di accettazione
della domanda

4.2.1 Altro (dettagliare origine ed importi)

4.3 Certifico la dichiarata disponibilita` e l'utilizzabilita` dei fondi di
cui ai punti 4.1 e 4.2:

Firma

(per la copia da depositare presso l'Ateneo e per l'assenso alla diffusione
via Internet delle informazioni riguardanti i programmi finanziati e la loro
elaborazione necessaria alle valutazioni; legge del 31.12.96 n. 675 sulla
"Tutela dei dati personali")

Firma

Data

Cognome	Nome	Dip.	qualifica	settore	mesi uomo
Alessi	Fabio	DIMI	RC	K05B	11+8
Gabbrielli	Maurizio	DIMI	PA	K05B	11+8
Honsell	Furio	DIMI	PO	K05B	11+8
MAzzanti	Stefano	DIMI	RC	K05B	11+8
Peron	Adriano	DIMI	RC	K05B	11+8

Cognome	Nome	Sede amm.	Dip.	ciclo	mesi uomo
Ciaffaglione	Alberto	Udine	DIMI	14	4+4
Franco	Gianluca	Udine	DIMI	12	4+4
Scagnetto	Ivan	Udine	DIMI	13	6+8

Cognome	Nome	ente	qualifica	mesi uomo
Lenisa	Marina	LFCS-Edinburgh	Research Fellow	3+8
Liquori	Luigi	ENS-Lyon	attache de recherche	3+8
Miculan	Marino	INFN-Trieste	tecnologo	3+3

Voce di spesa	spesa	descrizione
Materiale inventariabile	20	hardware, libri
Grandi Attrezzature
Materiale di consumo	7	telefono, posta, fotocopie
Spese per calcolo ed elaborazione dati	10	account e manutenzione
Personale a contratto	30	assegnista per 1 anno
Servizi esterni
Missioni	53	convegni, collaborazione scientifica
Altro	10	invitati e seminari

Costo complessivo del Programma dell'Unita` di Ricerca	130
Costo minimo per garantire la possibilita` di verifica dei risultati	110
Fondi disponibili (RD)	12,25
Fondi acquisibili (RA)	25,25
Cofinanziamento richiesto al MURST	96,5

Provenienza	anno di ass.	importo disp.	nome Resp. Naz.
Universita`	1999
Dipartimento	1993 in poi
MURST(ex 40%)	1995-1996
CNR
Unione Europea	1998
Altro
TOTALE

Provenienza	anno della domanda	stato di appr.	disponibilita`
Universita`	1999	C
Dipartimento
CNR
Unione Europea
Altro
TOTALE

Parte I

Parte II

Theory, applications, and experiments of Logical Frameworks based on Type Theories (F.Honsell, F.Alessi, M.Miculan, I.Scagnetto, A.Ciaffaglione)

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

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)

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

Real time automata (A.Peron)

Parte III

Parte IV