A Fully Abstract Model for (2008)
Abstract. Aim of this paper is to develop a filter model for a calculus with mobility and higher-order value passing. We will define it for an extension of the Ambient Calculus in which processes can...
Stone dualities allow to describe special classes of topological spaces by means of (possibly finitary) partial orders. Typically, these partial orders are given by the topology, a basis for it, or a...
A Calculus of Evolving Objects (2008)
M. Dezani-Ciancaglini, P. Giannini, O. Nierstrasz
The demands of developing modern, highly dynamic applications have led to an increasing interest in dynamic programming languages and mechanisms. Not only must applications evolve over time, but the...
Compositional Characterisations of λ-terms using Intersection Types ⋆ (2007)
M. Dezani-ciancaglini, F. Honsell, Y. Motohama
We show how to characterise compositionally a number of evaluation properties of λ-terms using Intersection Type assignment systems. In particular, we focus on termination properties, such as strong...
A Complete Characterization of Complete Intersection-Type Preorders (2007)
M. Dezani-Ciancaglini, Intersection-type Preorders, F. Honsell, F. Alessi
this paper we solve completely the characterization problem as far as the three canonical set-theoretical semantics for intersection-types: the inference semantics, the simple semantics [Scott 1975]...
A Complete Characterization of Complete Intersection-Type Preorders (2007)
Intersection-type Preorders, M. Dezani-ciancaglini, F. Honsell, F. Alessi, ...
this paper we solve completely the characterization problem as far as the three canonical set-theoretical semantics for intersection-types: the inference semantics, the simple semantics [Scott 1975]...
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...
Compositional Characterisations of λ-terms using Intersection Types (2005)
M. Dezani-ciancaglini, F. Honsell, Y. Motohama
We show how to characterise compositionally a number of evaluation properties of #-terms using Intersection Type assignment systems. In particular, we focus on termination properties, such as strong...
Tailoring Filter Models (2004)
F. Alessi, F. Barbanera, M. Dezani-ciancaglini
Conditions on type preorders are provided in order to characterize the induced filter models for the #-calculus and some of its restrictions. Besides, two examples are given of filter models in which...
A Calculus of Bounded Capacities (2003)
F. Barbanera, M. Bugliesi, M. Dezani-ciancaglini, V. Sassone
Abstract. Resource control has attracted increasing interest in foundational research on distributed systems. This paper focuses on space control and develops an analysis of space usage in the...
A Calculus of Bounded Capacities (2003)
F. Barbanera, M. Bugliesi, M. Dezani-ciancaglini, V. Sassone
Abstract. Resource control has attracted increasing interest in foundational research on distributed systems. This paper focuses on space control and develops an analysis of space usage in the...
A Calculus of Bounded Capacities (2003)
F. Barbanera, M. Bugliesi, M. Dezani-ciancaglini, V. Sassone
Abstract. Resource control has attracted increasing interest in foundational research on distributed systems. This paper focuses on space control and develops an analysis of space usage in the...
A Calculus of Bounded Capacities (2003)
F. Barbanera, M. Bugliesi, M. Dezani-ciancaglini, V. Sassone
Abstract. Resource control has attracted increasing interest in foundational research on distributed systems. This paper focuses on space control and develops an analysis of space usage in the...
A Calculus of Bounded Capacities (2003)
F. Barbanera, M. Bugliesi, M. Dezani-ciancaglini, V. Sassone
Resource control has attracted increasing interest in foundational research on distributed systems. This paper focuses on space control and develops an analysis of space usage in the context of an...
Intersection Types and Lambda Theories (2002)
Dezani-Ciancaglini, M., Lusin, S.
We illustrate the use of intersection types as a semantic tool for showing properties of the lattice of lambda theories. Relying on the notion of easy intersection type theory we successfully build a...
Intersection Types and Lambda Theories (2002)
M. Dezani-Ciancaglini, S. Lusin
We illustrate the use of intersection types as a semantic tool for showing properties of the lattice of l-theories. Relying on the notion of easy intersection type theory we successfully build a...
Filter Models and Easy Terms (2001)
F. Alessi, M. Dezani-Ciancaglini, F. Honsell
We illustrate the use of intersection types as a tool for synthesizing -models which exhibit special purpose features. We focus on semantical proofs of easiness. This allows us to prove that the...
A Complete Characterization of Complete Intersection-Type Theories (2000)
Dezani-Ciancaglini, M., Honsell, F., Alessi, F.
We characterize those intersection-type theories which yield complete intersection-type assignment systems for lambda-calculi, with respect to the three canonical set-theoretical semantics for...
Security types for mobile safe ambients (2000)
M. Dezani-ciancaglini, I. Salvo
Abstract. The Ambient Calculus and the Safe Ambient Calculus have been recently successfully proposed as models for the Web. They are based on the notions of ambient movement and ambient opening....
A complete characterization of the complete intersection-type theories (2000)
M. Dezani-ciancaglini, F. Honsell, F. Alessi
We characterize those intersection-type theories which yield complete intersection-type assignment systems for l-calculi, with respect to the three canonical set-theoretical semantics for...
The minimal relevant logic and the call-by-value lambda calculus (1999)
S. Van Bakel, M. Dezani-ciancaglini, Y. Motohama
The minimal relevant logic B+, seen as a type discipline, includes an extension of Curry types known as the intersection type discipline. We will show that the full logic B+ gives a type assignment...
The minimal relevant logic and the call-by-value lambda calculus (1999)
S. Van Bakel, M. Dezani-ciancaglini, Y. Motohama
The minimal relevant logic B+, seen as a type discipline, includes an extension of Curry types known as intersection type discipline. We show that the full logic B+ gives a type assignment system...
The minimal relevant logic and the call-by-value lambda calculus (1999)
S. Van Bakel, M. Dezani-ciancaglini, Y. Motohama
The minimal relevant logic B+, seen as a type discipline, includes an extension of Curry types known as the intersection type discipline. We will show that the full logic B+ gives a type assignment...
The Minimal Relevant Logic and the Call-by-Value Lambda Calculus (1999)
S. Van Bakel, M. Dezani-ciancaglini, U. De'Liguoro, Y. Motohama
The minimal relevant logic B+, seen as a type discipline, includes an extension of Curry types known as the intersection type discipline. We will show that the full logic B+ gives a type assignment...
The minimal relevant logic and the call-by-value lambda calculus (1999)
S. Van Bakel, M. Dezani-ciancaglini, Y. Motohama
The minimal relevant logic B+,seenasatype discipline, includes an extension of Curry types known as intersection type discipline. We show that the full logic B+ gives a type assignment system which,...
A Simple Calculus of Exception Handling (1995)
Philippe De Groote, M. Dezani-ciancaglini, G. Plotkin (eds
. We introduce a simply-typed -calculus ( ! exn ) featuring an ML-like exception handling mechanism. This calculus, whose type system corresponds to classical logic through the Curry-Howard...