Research activity in 2001
The research topic of the group is to build abstract models for reasoning about the semantics of programming languages, and then to develop formal tools, based on the semantics, for proving properties of programs. In particular, the semantics techniques are developed for paradigmatic languages based on the lambda calculus, modelling different kinds of computation. The research activity of the group in 2001 follows essentially the line of investigating the use of logical tools for modelling properties of programs. Some of the developed tools start from the Linear Logic, inside both the TMR project "Linear Logic" and the progetto cofinanziato MURST "Logica Lineare e dintorni"). A short presentation of the 2001 publications follows.
In [1] a new presentation of the Affine Linear Logic (LAL) is given. This formalisation allows a monolitical treatment of the proof-nets, and solves some open questions about the logical system.
An interesting tool for studying the semantics of programming languages is the system of intersection types, in its various variants. The semantics of intersection types can be expressed in domain theory, but until now, this system lack of a clear logical foundation. In [2] we give such a foundation, and the relationship between this new logic and the implicative and additive fragment of the intuitionistic logic is clearly stated. The paper [3] is an example of the use of intersection types for the semantics investigation of properties of programs, in fact they are used for characterising convergent terms in the Object Calculus proposed by Abadi and Cardelli. The paper [4] is a comparison of different operational semantics for lambda calculus, using as tool different variants of Bohm trees. The publication [5] is a LNCS volume, containing the proceedings of the "7th Italian Conference on Theoretical Computer Science", which held in Torino in October 2001, co-chaired by Simona Ronchi Della Rocca and Antonio Restivo.
2001 Publications
[1] A. Asperti and L. Roversi. Intuitionistic light affine logic. ACM Transactions on Computational Logic, 3(1):1 -- 39, January 2002.
[2] S. Ronchi Della Rocca and Roversi L. Intersection logic. In Proc. of CSL'01, volume 2142 of LNCS, pages 414-428. Springer-Verlag, 2001.
[3] Ugo de' Liguoro. Characterizing convergent terms in object calculi via intersection types. In TLCA'01, LNCS 2044, pages 315-328. Springer, 2001.
[4] Dezani-Ciancaglini M., Giovannetti E., From Bohm's Theorem to Observational Equivalences: an Informal Account, BOTH’01, ENTCS, Elsevier, pages 85-118, 2001.
[5] A.Restivo, S. Ronchi Della Rocca, and L. Roversi (Editors). Theoretical Computer Science - 7th Italian Conference, ICTCS 2001, Torino, Italy, October 4-6, 2001, Proceedings. LLNCS2202.
