|
|
|
|
DIPARTIMENTO DI INFORMATICA |
|
|
|
|
|
|
|
Research Report Year 2003
Computer Science
|
|
Last and first name |
Position |
|
|
Ronchi della Rocca Simona |
Full Professor |
|
|
de'Liguoro Ugo |
Associate Professor |
|
|
Roversi Luca |
Associate Professor |
|
|
Severi Paula |
Postdoctoral Researcher |
- Research activity in 2003
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 2003 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 the 2002-MIUR project "PROTOCOLLO"
(from PROof TO COmputation through Linear Logic). The research has
been organized in three lines.
1) Logical Semantics.
The logical semantics is based on a type assignment system, assigning
types to terms of the considered language. Types are built using the
“intersection” constructor. Under some conditions, the type assignment
system can induce a denotational model, where the meaning of a term
is given by the set of types that can be assigned to it. The type
assignment system is a useful tool for reasoning in a finitary way
about the denotation of terms.
In [1] we address the problem of formal reasoning about mobile code. We consider an Ambient Calculus, where process syntax includes constructs for sequential programming. For the sake of concreteness, and because of practical relevance, we consider objects using message exchange to implement method invocation and overriding. The contribution of the paper is a type assignment system, obtained by combination of systems for MA and for the Sigma-calculus. We exploit in the mobility framework a typical feature of the intersection type discipline for object calculi, namely late typing of self. The proposed system is then checked against standard properties of related systems, establishing type invariance a completeness theorems.
In [2] we investigate logical semantics of the first order Sigma-calculus. An assignment system of predicates to first order typed terms of the OB1 calculus is introduced. We define retraction models for that calculus and an interpretation of terms, types and predicates into such models. The assignment system is then proved to be sound and complete w.r.t. retraction models.
The lazy evaluation of the lambda-calculus, both in call-by-name and in call-by-value setting, is studied in [5]. Starting from a logical descriptions of two topological models of such calculi, a pre-order relation on terms, stratified by types, is defined, which grasps exactly the two operational semantics we want to model. Such a relation can be used for building two fully abstract models.
2) Models for Computations with limited complexity.
Elementary Affine Logic (EAL) is a variant of the Linear Logic characterizing
the computational power of the elementary bounded Touring machines.
The EAL Type Inference problem is the problem of automatically assign
to terms of lambda-calculus EAL formulas as types. In [3] this problem
is proved to be decidable, and an algorithm is showed, building, for
every lambda-term, either a negative answer or a finite set of type
schemata, from which all and only its typings can be derived, through
suitable operations.
3) Discriminationg problems inside lambda calculus.
In [4] we propose an extension of lambda calculus for which the Berarducci
trees equality coincides with observational equivalence, when we observe
rootstable or rootactive behavior of terms. In one direction the proof
is an adaptation of the classical Böhm out technique. In the
other direction the proof is based on confluence for strongly converging
reductions in this extension.
[1] Franco Barbanera and Ugo de'Liguoro.
Type Assignement for Mobile Objects. In COMETA'03, ENTCS series. Elsevier,
2003
[2] Steffen van Bakel and Ugo de'Liguoro.
Logical Semantics for the First Order Sigma-Calculus.
In ICTCS'03, volume 2841 of LNCS, pages 202-215. Springer-Verlag, 2003.
[3] Paolo Coppola and Simona Ronchi Della Rocca. Principal typing
for elementary affine logic. In Hofmann M., editor, Typed Lambda Calculi
and Applications: 6th International Conference (TLCA 2003), volume
2701 of Lecture Notes in Computer Science, pages 90-104, Berlin, 2003.
Springer-Verlag. [4] M. Dezani-Ciancaglini, P. Severi, and F.-J. de Vries. Infinitary
lambda calculus and discrimination of Berarducci trees. Theoretical
Computer Science, 298(2):275-302, 2003.
[5] Luca Paolini and Simona Ronchi Della Rocca. Lazy logical semantics.
Electronic Notes in Theoretical Computer Science, 2003. Project leader: Simona Ronchi Della Rocca (national coordinator and
responsible for the site of Torino) Kind of grant: MIUR
|
|
[Information] [People] [Research] [Ph.D.] [Education] [Library] [Search] |
|
|
|
|
Administrator: wwwadm[at]di.unito.it |
Last update:
May 05, 2004
|
|
|
|