Mariangiola Dezani-ciancaglini

From B"ohm's Theorem to Observational Equivalences: an Informal Account 1 (2008)

This paper is an introduction to intersection type disciplines, with the aim of illustrating their theoretical relevance in the foundations of-calculus. We start by describing the well-known results...

Role-based Access Control for Boxed (2008)

Abstract There are essentially two ways of looking at the computational behaviours of *- terms. One consists in putting the term within a context (possibly of *-calculus extensions) and observing...

Adriana Compagnoni, Elsa L. Gunter, Mariangiola Dezani-ciancaglini

Ronchi Della Rocca on the occasion of their sixtieth birthdays Our society is increasingly moving towards richer forms of information exchange where mobility of processes and devices plays a...

IOS Press AConvex Powerdomain over Lattices: its Logic and-Calculus (2008)

Fabio Alessi, Mariangiola Dezani-ciancaglini, Ugo De Liguoro

Abstract. To model at the same time parallel and nondeterministic functional calculi we de ne a powerdomain functor P such that it is an endofunctor over the category of algebraic lattices. P is...

Bounded Session Types for Object Oriented Languages ⋆ (2008)

Mariangiola Dezani-ciancaglini, Elena Giachino, Sophia Drossopoulou, Nobuko Yoshida

Abstract. Earlier work explored the introduction of session types into object oriented languages. Following the session types literature, two parties would start communicating, provided the types...

Encoding CDuce in the Cπ-calculus (2008)

Mariangiola Dezani-ciancaglini, Daniele Varacca

Abstract. We present a type faithful encoding of CDuce into the Cπ-calculus. These calculi are two variants of, respectively, the λ-calculus and the π-calculus, characterised by rich typing and...

INTERSECTION AND REFERENCE TYPES DEDICATED TO HENK BARENDREGT ON THE OCCASION OF HIS 60TH BIRTHDAY (2008)

Mariangiola Dezani-ciancaglini, Ronchi Della Rocca

Abstract. Aim of this paper is to understand the interplay between intersection and reference types. Putting together the standard typing rules for intersection types and reference types leads to...

Inverse Limit Models as Filter Models (2008)

Fabio Alessi, Mariangiola Dezani-ciancaglini, Furio Honsell

Natural intersection type preorders are the type structures which agree with the plain intuition of intersection type constructor as set-theoretic intersection operation and arrow type constructor as...

The M³ Paradigm - Types and Type Inference for Ambient and Process Mobility (2008)

Mario Coppo, Mariangiola Dezani-ciancaglini, Elio Giovannetti

A new kind of ambient calculi is presented, where the open capability is replaced by direct mobility of naked processes, while the associated type systems are algorithmic in the sense that they...

Amalgamating Sessions and Methods in Object Oriented Languages with Generics. Theoretical Computer Science (2008)

Sara Capecchi, Mariangiola Dezani-ciancaglini, Sophia Drossopoulou, Elena Giachino

We suggest an amalgamation of communication based programming (centred on sessions) and object oriented programming, whereby sessions between concurrent threads are amalgamated with methods. In our...

Global Progress in Dynamically Interleaved Multiparty Sessions (2008)

Lorenzo Bettini, Marco De Luca, Mariangiola Dezani-ciancaglini, Nobuko Yoshida

Abstract. A multiparty session forms a unit of structured interactions among many participants which follow a prescribed scenario specified as a global type signature. This paper develops, besides a...

Böhm’s Theorem (2008)

Stefano Guerrini, Adolfo Piperno, Mariangiola Dezani-ciancaglini

The technical significance of Böhm’s Theorem [Böhm, 1968] suffices to deserve it a prominent place in any monograph on the theory of the λ-calculus [Barendregt, 1984, Hindley and Seldin, 1986,...

of the domain equation D = P([D! D]?). We derive from the algebras of P the logic (2007)

Fabio Alessi, Mariangiola Dezani-ciancaglini, Ugo De Liguoro, Of D

Abstract. To model at the same time parallel and non-deterministic functional calculi we define a powerdomain functor P such that it is an endofunctor over the category of algebraic lattices. P is...

Italy, (2007)

Alessandro Berarducci, Mariangiola Dezani-ciancaglini

Recent work on infinitary versions of the lambda calculus has shown that the infinite lambda calculus can be a useful tool to study the unsolvable terms of the classical lambda calculus. Working in...

Intersection Types,-models, and Bohm Trees (2007)

Mariangiola Dezani-ciancaglini, Adolfo Piperno

This paper is an introduction to intersection type disciplines, with the aim of illustrating their theoretical relevance in the foundations of-calculus. We start by describing the well-known results...

1 (2007)

Abstract. The distinction between the conjunctive nature of non-determinism as opposed to the disjunctive character of parallelism constitutes the motivation and the starting point of the present...

IOS Press A Subtyping for Extensible, Incomplete Objects To Helena Rasiowa: in memoriam (2007)

Viviana Bono, Michele Bugliesi, Mariangiola Dezani-ciancaglini, Luigi Liquori

Abstract. We extend the type system for the Lambda Calculus of Objects [16] with a mechanism of width subtyping and a treatment of incomplete objects. The main novelties over previous work are the...

3 (2007)

Ali S. Aoun, Mariangiola Dezani-ciancaglini, Seref Mirasyedioglu, Franco Barbanera, Franco Barbanera

Parallelism and non-determinism are fundamental concepts in the process algebra theory. Combining them with-calculus can enlighten the theory of higher-order process algebras. In recent papers an...

Types for Trees (2007)

Steffen Van Bakel, Franco Barbanera, Mariangiola Dezani-ciancaglini

We introduce a type assignment system which is parametric with respect to five families of trees obtained by evaluating -terms (Bohm trees, L'evy-Longo trees, ...). Then we prove, in an (almost)...

Imperial College, (2007)

Characterising Strong Normalisation, Steffen Van Bakel, Mariangiola Dezani-ciancaglini

We characterise the strongly normalising terms of a composition-free calculus of explicit substititions (with or without garbage collection) by means of an intersection type assignment system. The...

b Fer-Jan de Vries (2007)

Mariangiola Dezani-ciancaglini, Paula Severi

c;3

2 (2007)

Sophia Drossopoulou, Ferruccio Damiani, Mariangiola Dezani-ciancaglini, Paola Giannini

Abstract. Re-classication changes at run-time the class membership of an object while retaining its identity. We suggest language features for object re-classication, which could extend an...

2 (2007)

Sophia Drossopoulou, Ferruccio Damiani, Mariangiola Dezani-ciancaglini, Paola Giannini

Abstract. Re-classication changes at run-time the class membership of an object while retaining its identity. We suggest language features for object re-classication, which could extend an...

IOS Press A Subtyping for Extensible, Incomplete Objects To Helena Rasiowa: in memoriam (2007)

Viviana Bono, Michele Bugliesi, Mariangiola Dezani-ciancaglini, Luigi Liquori

Abstract. We extend the type system for the Lambda Calculus of Objects [16] with a mechanism of width subtyping and a treatment of incomplete objects. The main novelties over previous work are the...

WOOD’03 Preliminary Version Can Addresses be Types? (a case study: objects with delegation) (2007)

Christopher Anderson, Franco Barbanera, Mariangiola Dezani-ciancaglini, Sophia Drossopoulou

We adapt the aliasing constraints approach for designing a flexible typing of evolving objects. Types are singleton types (addresses of objects, as a matter of fact) whose relevance is mainly due to...

Re-classification and Multi-threading: Fickle_MT (2007)

Ferruccio Damiani, Mariangiola Dezani-Ciancaglini, Paola Giannini

Ferruccio Damiani + Universit a di Torino Corso Svizzera 185 damiani@di.unito.it Mariangiola Dezani-Ciancaglini # Universit a di Torino Corso Svizzera 185 dezani@di.unito.it Paola Giannini Universit...

Security Types for Dynamic Web Data (2007)

Dezani-Ciancaglini, Mariangiola, Ghilezan, Silvia, Pantovic, Jovanka, Varacca, Daniele

We describe a type system for the Xdpi calculus. An Xdpi-network is a network of locations, where each location consists of both a data tree (which contains scripts and pointers to nodes in trees at...

Security Types for Dynamic Web Data (2007)

Dezani-Ciancaglini, Mariangiola, Ghilezan, Silvia, Pantovic, Jovanka, Varacca, Daniele

We describe a type system for the Xdpi calculus. An Xdpi-network is a network of locations, where each location consists of both a data tree (which contains scripts and pointers to nodes in trees at...

On Progress for Structured Communications (2007)

Mariangiola Dezani-ciancaglini, Ugo De Liguoro, Nobuko Yoshida

Abstract. We propose a new typing system for the π-calculus with sessions, which ensures the progress property, i.e. once a session has been initiated, typable processes will never starve at session...

Asynchronous Session Types and Progress for Object-Oriented Languages (2007)

Mariangiola Dezani-ciancaglini, Nobuko Yoshida

Abstract. A session type is an abstraction of a sequence of heterogeneous values sent over one channel between two communicating processes. Session types have been introduced to guarantee consistency...

Mariangiola Dezani-ciancaglini, Dimitris Mostrous, Nobuko Yoshida, Sophia Drossopoulou

Abstract. A session takes place between two parties; after establishing a connection, each party interleaves local computations with communications (sending or receiving) with the other. Session...

Mariangiola Dezani-ciancaglini, Dimitris Mostrous, Nobuko Yoshida, Sophia Drossopoulou

Abstract. A session takes place between two parties; after establishing a connection, each party interleaves local computations with communications (sending or receiving) with the other party....

Mariangiola Dezani-ciancaglini, Dimitris Mostrous, Nobuko Yoshida, Sophia Drossopoulou

Abstract. A session takes place between two parties; after establishing a con-nection, each interleaves local computations and communications (sending or receiving) with the other. Session types...

A Behavioural Model for Klop’s Calculus (2006)

Mariangiola Dezani-ciancaglini, Makoto Tatsuta

Replace this file withprentcsmacro.sty for your meeting, or withentcsmacro.sty for your meeting. Both can be

Under consideration for publication in Math. Struct. in Comp. Science Boxed Ambients with Communication Interfaces † (2006)

Pablo Garralda, Eduardo Bonelli, Adriana Compagnoni, Mariangiola Dezani-ciancaglini, P. Garralda, E. Bonelli, ...

an ambient calculus with a flexible communication policy. Traditionally, typed ambient calculi have a fixed communication policy determining the kind of information that can be exchanged with a...

Under consideration for publication in Math. Struct. in Comp. Science Types for Ambient and Process Mobility † (2006)

A new kind of ambient calculus is presented, where the open capability is replaced by direct mobility of generic processes. The calculus comes equipped with a labelled transition system in which...

Mariangiola Dezani-ciancaglini, Dimitris Mostrous, Nobuko Yoshida, Sophia Drossopoulou

Abstract. A session takes place between two parties; after establishing a connection, each party interleaves local computations with communications (sending or receiving) with the other. Session...

A Distributed Object-Oriented Language with Session Types (2005)

Mariangiola Dezani-ciancaglini, Nobuko Yoshida, Alexander Ahern, Er Ahern, Sophia Drossopoulou

In the age of the world-wide web and mobile computing, programming communication-centric software is essential. Thus, programmers and program designers are exposed to new levels of complexity, such...

A Distributed Object-Oriented Language with Session Types (2005)

Mariangiola Dezani-ciancaglini, Nobuko Yoshida, Alexander Ahern, Er Ahern, Sophia Drossopoulou

In the age of the world-wide web and mobile computing, programming communication-centric software is essential. Thus, programmers and program designers are exposed to new levels of complexity, such...

A Distributed Object-Oriented Language with Session Types (2005)

Mariangiola Dezani-ciancaglini, Nobuko Yoshida, Alexander Ahern, Er Ahern, Sophia Drossopoulou

In the age of the world-wide web and mobile computing, programming communication-centric software is essential. Thus, programmers and program designers are exposed to new levels of complexity, such...

A Distributed Object-Oriented Language with Session Types (2005)

Mariangiola Dezani-ciancaglini, Nobuko Yoshida, Alexander Ahern, Er Ahern, Sophia Drossopoulou

In the age of the world-wide web and mobile computing, programming communication-centric software is essential. Thus, programmers and program designers are exposed to new levels of complexity, such...

A Mobility Calculus with Local and Dependent Types (2005)

Federico Cozzi, Mariangiola Dezani-ciancaglini, Elio Giovannetti, Rosario Pugliese

Abstract. We introduce an ambient-based calculus that combines ambient mobility with process mobility, uses group names to collect ambients with homologous features, and exploits co-moves and runtime...

A Mobility Calculus with Local and Dependent Types (2005)

Federico Cozzi, Mariangiola Dezani-ciancaglini, Elio Giovannetti, Rosario Pugliese

Abstract. We introduce an ambient calculus that combines ambient mobility with process mobility, uses group names to group ambients with homologous features, and exploits co-moves and runtime type...

Boxed Ambients with Communication Interfaces (2004)

Eduardo Bonelli, Adriana Compagnoni, Mariangiola Dezani-ciancaglini, Pablo Garralda

We define BACI (Boxed Ambients with Communication Interfaces), an ambient calculus allowing a liberal communication policy. Each ambient carries its local view of the topic of conversation (the type...

Type Preorders and Recursive Terms (2004)

Fabio Alessi, Mariangiola Dezani-ciancaglini

We show how to use intersection types for building models of a #-calculus enriched with recursive terms, whose intended meaning is of minimal fixed points. As a by-product we prove an interesting...

Dynamic and Local Typing for Mobile Ambients (2004)

Mario Coppo, Mariangiola Dezani-ciancaglini, Elio Giovannetti, Rosario Pugliese

An ambient calculus with both static and dynamic types is presented, where the latter ones represent mobility and access rights that may be dynamically consumed and acquired in a controlled way....

On Re-classification and Multi-threading (2004)

Ferruccio Damiani, Mariangiola Dezani-Ciancaglini, Paola Giannini

this paper we consider re-classification in the presence of multi-threading. To this aim we define a multi-threaded extension of the language MT . We define an operational semantics and a type and...

Boxed Ambients with Communication Interfaces (2004)

Eduardo Bonelli, Adriana Compagnoni, Mariangiola Dezani-ciancaglini, Pablo Garralda

Abstract. We define BACI (Boxed Ambients with Communication Interfaces), an ambient calculus allowing a liberal communication policy. Each ambient carries its local view of the topic of conversation...

Two behavioural lambda models (2003)

Intersection types for explicit substitutions (2003)

Abstract. We build a lambda model which characterizes completely (persistently) normalizing, (persistently) head normalizing, and (persistently) weak head normalizing terms. This is proved by using...

Stéphane Lengr, Pierre Lescanne, Dan Dougherty, Mariangiola Dezani-ciancaglini, Steffen Van Bakel

We present a new system of intersection types for a composition-free calculus of explicit substitutions with a rule for garbage collection, and show that it characterizes those terms which are...

Intersection Types for Explicit Substitutions (2003)

Stéphane Lengrand, Pierre Lescanne, Dan Dougherty, Mariangiola Dezani-Ciancaglini, Steffen Van Bakel

We present a new system of intersection types for a composition-free calculus of explicit substitutions with a rule for garbage collection, and show that it characterizes those terms which are...

Can Addresses be Types? (a case study: objects with delegation) (2003)

Christopher Anderson, Franco Barbanera, Mariangiola Dezani-ciancaglini, Sophia Drossopoulou

We adapt the aliasing constraints approach for designing a flexible typing of evolving objects. Types are singleton types (addresses of objects, as a matter of fact) whose relevance is mainly due to...

Alias and Union Types for Delegation (2003)

Christopher Anderson, Franco Barbanera, Mariangiola Dezani-ciancaglini

Abstract — We adapt the aliasing constraints approach for designing a flexible typing of evolving objects. Types are singleton types (addresses of objects, as a matter of fact) or finite...

Two Behavioural Lambda Models (2003)

Intersection Types and Computational Rules (2003)

We build two inverse limit lambda models which characterize completely sets of terms having similar computational behaviour. More precisely for each one of these sets of terms there is a...

Fabio Alessi Franco, Franco Barbanera, Mariangiola Dezani-ciancaglini

The invariance of the meaning of a #-term by reduction/expansion w.r.t. the considered computational rules is one of the minimal requirements one expects to hold for a #-model. Being the intersection...

The Semantics of Entailment Omega (2002)

Dezani-Ciancaglini, Mariangiola, Meyer, Robert K., Motohama, Yoko

This paper discusses the relation between the minimal positive relevant logic B $_{+}$ and intersection and union type theories. There is a marvelous coincidence between these very differently...

Characterising Strong Normalisation for Explicit Substitutions (2002)

Steffen Van Bakel, Mariangiola Dezani-ciancaglini

Abstract. We characterise the strongly normalising terms of a composition-free calculus of explicit substitutions (with or without garbage collection) by means of an intersection type assignment...

Semantic Subtyping (2002)

Mariangiola Dezani-ciancaglini, Alain Frisch, Elio Giovannetti, Yoko Motohama

a,1

Characterising Strong Normalisation for Explicit Substitutions (2002)

Characterising Strong Normalisation, Steffen Van Bakel, Mariangiola Dezani-ciancaglini

We characterise the strongly normalising terms of a composition-free calculus of explicit substitutions (with or without garbage collection) by means of an intersection type assignment system. The...

A Type Inference Algorithm for Secure Ambients (2002)

Franco Barbanera, Mariangiola Dezani-ciancaglini, Ivano Salvo, Vladimiro Sassone

We consider a type discipline for the Ambient Calculus that associates ambients with security levels and constrains them to be traversed by or opened in ambients of higher security clearance only. We...

Refined Effects for Reclassification: Fickle_III (2001)

Ferruccio Damiani, Mariangiola Dezani-Ciancaglini, Sophia Drossopoulou, Paola Giannini

This paper is organized as follows: In Section 2 we introduce III informally using an example. In Sections 3, 4, and 5 we outline III : the syntax, operational semantics, typing rules, and we state...

A Lambda Model Characterizing Computational Behaviours of Terms (2001)

Lambda Models Characterizing Computational Behaviours of Terms (2001)

We build a lambda model which characterizes completely (persistently) normalizing, (persistently) head normalizing, and (persistently) weak head normalizing terms.