Adriana Compagnoni

Higher-order subtyping and its decidability (2008)

Session types describe the interactions between two parties within multi-party communications. They constitute a communication protocol in the sense that the order and type of interactions between...

Role-based Access Control for Boxed (2008)

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

Abstract BASS: Boxed Ambients with Safe Sessions ∗ (2008)

Pablo Garralda, Adriana Compagnoni

We define BASS, a typed boxed ambients calculus with safe sessions. Sessions offer the possibility of using the same channel to transmit information of different types in a prescribed order. A...

FGUC 2004 Preliminary Version Typechecking Safe Process Synchronization (2008)

Typed Operational Semantics for Higher Order (2008)

Session types describe the interactions between two parties within multi-party communications. They constitute a communication protocol in the sense that the order and type of interactions between...

Under consideration for publication in J. Functional Programming 1 Correspondence Assertions for Process Synchronization in Concurrent Communications∗ (2008)

Bounded operator abstraction is a language construct relevant to object oriented programming languages and to ML2000, the successor to Standard ML. In this paper, we introduce Fω ≤,avariantofFω...

Eduardo Bonelli, Adriana Compagnoni, Elsa Gunter, E. Bonelli, A. Compagnoni, E. Gunter

High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types (Honda et al., 1998). However, a number of examples suggest that session...

An Object Calculus with Algebraic Rewriting (2007)

Adriana Compagnoni, Maribel Fernández

. In trying to use Abadi and Cardelli's object calculi as a foundation for a programming language the addition of algebraic data types arises naturally. This paper defines such an extension,...

Edinburgh EH9 3JZ, U. K. (2007)

Edinburgh EH9 3JZ, U. K. (2007)

We present a first-order linearly typed assembly language, HBAL, that allows the safe reuse of heap space for elements of di#erent types. The linear types discipline ensures a single pointer...

Multisession session types for a distributed calculus (2007)

We present a first-order linearly typed assembly language, HBAL, that allows the safe reuse of heap space for elements of di#erent types. The linear types discipline ensures a single pointer...

Eduardo Bonelli, Adriana Compagnoni

Abstract. Session types are a means of statically encoding patterns of interaction between two communicating parties. This paper explores a distributed calculus with session types in which a number...

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

Correspondence assertions for process synchronization in concurrent communications (2005)

A typed assembly language for non-interference (2005)

Replace this file with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be found at the ENTCS Macro Home Page.

Ricardo Medel, Adriana Compagnoni, Eduardo Bonelli

Abstract. Non-interference is a desirable property of systems in a multilevel security architecture, stating that confidential information is not disclosed in public output. The challenge of studying...

Correspondence assertions for process synchronization in concurrent communications (2005)

Ricardo Medel, Adriana Compagnoni, Eduardo Bonelli, La Plata (argentina

High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types [HVK98]. However, a number of examples suggest that session types fall...

Abstract (2005)

Non-interference is a desirable property of systems in a multilevel security architecture, stating that confidential information is not disclosed in public output. The challenge of studying...

A typed assembly language for non-interference (2005)

Ricardo Medel, Adriana Compagnoni, Eduardo Bonelli

Abstract. Non-interference is a desirable property of systems in a multilevel security architecture, stating that confidential information is not disclosed in public output. The challenge of studying...

Contents (2005)

Pablo Garralda, Eduardo Bonelli, Adriana Compagnoni

We define BACI (Boxed Ambients with Communication Interfaces), an ambient calculus with a flexible communication policy. Traditionally, typed ambient calculi have a fixed communication policy...

Information flow analysis for a typed assembly language with polymorphic stacks (2005)

Eduardo Bonelli, Adriana Compagnoni, Ricardo Medel

Abstract. We study secure information flow in a stack based Typed Assembly Language (TAL). We define a TAL with an execution stack and establish the soundness of its type system by proving...

Information flow analysis for a typed assembly language with polymorphic stacks (2005)

Eduardo Bonelli, Adriana Compagnoni, Ricardo Medel

Abstract. We study secure information flow in a stack based Typed Assembly Language (TAL). We define a TAL with an execution stack and establish the soundness of its type system by proving...

Typechecking Safe Process Synchronization (2004)

Bonelli, Eduardo, Compagnoni, Adriana, Gunter, Elsa

Session types describe the interactions between two parties within multi-party communications. They constitute a communication protocol in the sense that the order and type of interactions between...

Anti-Symmetry of Higher-Order Subtyping and Equality by Subtyping (2004)

Compagnoni, Adriana, Goguen, Healfdene

This paper shows that the subtyping relation of a higher-order lambda calculus, F-omega

Correspondence Assertions for Process Synchronization in Concurrent Communications (2004)

Bonelli, Eduardo, Compagnoni, Adriana, Gunter, Elsa

High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types (Honda et al., 1998). However, a number of examples suggest that session...

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

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

Draft- Not for distribution Contents (2004)

Eduardo Bonelli, Adriana Compagnoni, Ricardo Medel

Abstract (2004)

Eduardo Bonelli, Adriana Compagnoni, Elsa Gunter, Eduardo Bonelli, Elsa Gunter, Adriana Compagnoni

Session types describe the interactions between two parties within multi-party communications. They constitute a communication protocol in the sense that the order and type of interactions between...

High-Order Subtyping And Its Decidability (2003)

Compagnoni, Adriana

We define the typed lambda calculus F-omega-meet, a natural generalization of Girard's system F-omega with intersection types and bounded polymorphism. A novel aspect of our presentation is the use...

Heap bounded assembly language (2003)

Correspondence Assertions for Process Synchronization in Concurrent Communications (2003)

Abstract. We present a first-order linearly typed assembly language, HBAL, that allows the safe reuse of heap space for elements of different types. Linear typing ensures the single pointer property,...

Heap bounded assembly language (2003)

High-level speci cation of patterns of communications such as protocols can be modeled elegantly by means of session types [14]. However, a number of examples suggest that session types fall short...

Heap bounded assembly language (2003)

Abstract. We present a first-order linearly typed assembly language, HBAL, that allows the safe reuse of heap space for elements of different types. Linear typing ensures the single pointer property,...

Subtyping Dependent Types (2000)

Abstract. We present a first-order linearly typed assembly language, HBAL, that allows the safe reuse of heap space for elements of different types. Linear typing ensures the single pointer property,...

David Aspinall, Edinburgh Eh Jz, Adriana Compagnoni

The need for subtyping in type-systems with dependent types has been realized for some years. But it is hard to prove that systems combining the two features have fundamental properties such as...

Abstract (2000)

The need for subtyping in type-systems with dependent types has been realized for some years. But it is hard to prove that systems combining the two features have fundamental properties such as...

Anti-Symmetry of Higher-Order Subtyping (1999)

Anti-Symmetry of Higher-Order Subtyping (1999)

. This paper shows that the subtyping relation of a higherorder lambda calculus, F ! , is anti-symmetric. It exhibits the rst such proof, establishing in the process that the subtyping relation is a...

Subtyping for Object Type Constructors (1999)

This paper shows that the subtyping relation of a higher-order lambda calculus, F ! , is anti-symmetric. It exhibits the first such proof, establishing in the process that the subtyping relation is a...

Dominic Duggan, Adriana Compagnoni

Object type constructors have been introduced as an approach to adding container object types to a language with type inference. Useful subtyping for object type constructors requires a flexible...

Subject reduction and minimal types for higher order subtyping (1997)

Decidability of Higher-Order Subtyping via Logical Relations (1997)

We define the typed lambda calculus F ω ∧ , a natural generalization of Girard’s system F ω with intersection types and bounded polymorphism. A novel aspect of our presentation is the use of...

Typed Operational Semantics for Higher Order Subtyping (1997)

This paper uses logical relations for the first time to study the decidability of typechecking and subtyping. The result is proved for F ! , a language with higher-order subtyping and bounded...

Typed Operational Semantics for Higher Order Subtyping (1997)

Bounded operator abstraction is a language construct relevant to object oriented programming languages and to ML2000, the successor to Standard ML. In this paper, we introduce F ! , a variant of F !...

Decidable Higher Order Subtyping (1997)

Bounded operator abstraction is a language construct relevant to object oriented programming languages and to ML2000, the successor to Standard ML. In this paper, we introduce F ! , a variant of F !...

Subject reduction and minimal types for higher order subtyping (1997)

This paper establishes the decidability of typechecking in F ω ∧ , a typed lambda calculus combining higher-order polymorphism, subtyping, and intersection types. It contains the first proof of...

Decidable Higher Order Subtyping (1997)

Type systems with subtyping have also arisen from the study of lambda-calculi with intersection types at the University of Torino [26, 6]. Most of this work has been carried out in the setting of...

Typed operational semantics for higher order subtyping. Draft. Available at http://www.dcs.ed.ac.uk/home/abc (1997)

Abstract This paper establishes the decidability of typechecking in F! ^ , a typed lambda calculus combining higher-order polymorphism, subtyping, and intersection types. It contains the first proof...