Foundation of Session Types (2009)
Castagna, Giuseppe, Dezani-Ciancaglini, Mariangiola, Giachino, Elena, Padovani, Luca
Sessions are a common and widespread mechanism of interaction in distributed architectures. Two processes wanting to interact establish a connection on a common public channel. In this connection...
Foundation of Session Types (2009)
Castagna, Giuseppe, Dezani-Ciancaglini, Mariangiola, Giachino, Elena, Padovani, Luca
Sessions are a common and widespread mechanism of interaction in distributed architectures. Two processes wanting to interact establish a connection on a common public channel. In this connection...
Typed Iterators for XML (2008)
XML transformations are very sensitive to types: XML types describe the tags and attributes of XML elements as well as the number, kind, and order of their sub-elements. Therefore, operations, even...
Castagna, Giuseppe, Dezani-Ciancaglini, Mariangiola, Giachino, Elena, Padovani, Luca
We present a streamlined theory of session types based on a simple yet general and expressive formalism whose main features are semantically characterized and where each design choice is semantically...
Castagna, Giuseppe, Dezani-Ciancaglini, Mariangiola, Giachino, Elena, Padovani, Luca
We present a streamlined theory of session types based on a simple yet general and expressive formalism whose main features are semantically characterized and where each design choice is semantically...
Michele Bugliesi, Giuseppe Castagna, École Normale Supérieure
Boxed Ambients are a variant of Mobile Ambients that result from dropping the open capability, and introducing new primitives for ambient communication. The new model of communication is faithful to...
Semantic Subtyping for the π-Calculus (2008)
Giuseppe Castagna, Rocco De Nicola, Daniele Varacca
Subtyping relations for the #-calculus are usually defined in a syntactic way, by means of structural rules. We propose a semantic characterisation of channel types and use it to derive a subtyping...
Commitment and confinement for the Seal calculus (2007)
The Seal calculus is a distributed process calculus in which locations and movement of computational entities are explicit. The calculus is targeted at secure distributed applications over large...
Sous-Typage Et Programmation Orientée à Objets (2007)
this paper, simple records suffice. We do not give the definition of the encoding. Just remember that all the terms and types written below are encodable in &.
Unifying overloading and λ-abstraction: λ{} (2007)
In this short note we present a minimal system to deal with overloaded functions with late binding, in which λ-abstractions are seen as a special case of overloaded functions with just one code. We...
Type-Safe Compilation of Covariant Specialization: A Practical Case (2007)
John Boyland, Giuseppe Castagna
Despite its lack of type safety, some typed object-oriented languages use covariant specialization for methods. In this work, we show how one may modify the semantics of languages that use covariant...
Coviarance and Contravariance : Conflict without a Cause (2007)
In type theoretic research on object-oriented programming the "covariance versus contravariance issue" is a topic of continuing debate. In this short note we argue that covariance and...
C Duce: a white paper (working document) (2007)
Véronique Benzaken, Giuseppe Castagna, Alain Frisch
In this paper, we present the functional language C Duce, discuss some design issues, and show its adequacy for working with XML documents. Peculiar features of C Duce are a powerful pattern...
Veronique Benzaken, Giuseppe Castagna, Alain Frisch
In this paper, we present the functional language C Duce, discuss some design issues, and show its adequacy for working with XML documents. Peculiar features of C Duce are a powerful pattern...
Type-based xml projection (2006)
Véronique Benzaken, Giuseppe Castagna, Dario Colazzo, Kim Nguyên
XML data projection (or pruning) is one of the main optimization techniques recently adopted in the context of main-memory XML query-engines. The underlying idea is quite simple: given a query Q over...
A full pattern-based paradigm for XML query processing (2005)
Véronique Benzaken, Giuseppe Castagna, Cédric Miachon
Abstract. In this article we investigate a novel execution paradigm—ML-like pattern-matching— for XML query processing. We show that such a paradigm is well adapted for a common and frequent set...
Information flow security for xml transformations (2003)
Véronique Benzaken, Marwan Burelle, Giuseppe Castagna
Abstract. We provide a formal definition of information flows in XML transformations and, more generally, in the presence of type driven computations and describe a sound technique to detect...
Information flow security for xml transformations (2003)
Véronique Benzaken, Marwan Burelle, Giuseppe Castagna
Abstract. We provide a formal definition of information flows in XML transformations and, more generally, in the presence of type driven computations and describe a sound technique to detect...
CDuce: An XML-Centric General-Purpose Language (2003)
Véronique Benzaken, Giuseppe Castagna, Alain Frisch
We present the functional language CDuce, discuss some design issues, and show its adequacy for working with XML documents. Distinctive features of CDuce are a powerful pattern matching, first class...
CDuce: an XML-centric general-purpose language (2003)
Vronique Benzaken, Giuseppe Castagna, Alain Frisch
Abstract. We present the functional language C Duce, discuss some design issues, and show its adequacy for working with XML documents. Distinctive features of C Duce are a powerful pattern matching,...
The Seal Calculus Revisited: contextual equivalence and bisimilarity (2003)
Giuseppe Castagna, Francesco Zappa Nardelli
We present a new version of the Seal Calculus, a calculus of mobile computation. We study observational congruence and bisimulation theory, and show how they are related.
Alain Frisch, Giuseppe Castagna, Véronique Benzaken
Usually subtyping relations are defined either syntactically by a formal system or semantically by an interpretation of types in an untyped denotational model. In this work we show how to define a...
Information Flow Security in Boxed Ambients (2002)
Silvia Crafa, Michele Bugliesi, Giuseppe Castagna
We study the problem of secure information flow for Boxed Ambients in terms of noninterference. We develop a sound type system that provides static guarantees of absence of unwanted flow of...
Michele Bugliesi, Giuseppe Castagna
Secure Safe Ambients (SSA) are a typed variant of Safe Ambients [9] whose type system allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type...
Subtyping and Matching for Mobile Objects (2001)
Michele Bugliesi, Giuseppe Castagna, Silvia Crafa
In [BCC00], we presented a general framework for extending calculi of mobile agents with object-oriented features, and we studied a typed instance of that model based on Cardelli and Gordon's...
Reasoning about Security in Mobile Ambients (2001)
Michele Bugliesi, Giuseppe Castagna, Silvia Crafa
The paper gives an assessment of security for Mobile Ambients, with specific focus on mandatory access control (MAC) policies in multilevel security systems. The first part of the paper reports on...
Michele Bugliesi, Giuseppe Castagna, Silvia Crafa
Boxed Ambients are a variant of Mobile Ambients, that result from (i) dropping the open capability and (ii) providing new primitives for ambient communication while retaining the constructs in and...
Secure Safe Ambients and JVM Security (Abstract) (2000)
Michele Bugliesi, Giuseppe Castagna
) Michele Bugliesi Dipartimento di Informatica Universita Ca' Foscari di Venezia michele@dsi.unive.it http://www.dsi.unive.it/ michele Giuseppe Castagna C.N.R.S. Laboratoire d'Informatique,...
Michele Bugliesi, Giuseppe Castagna
We describe a general model for integrating object-oriented features in calculi of mobile agents. We then study two complementary instances of the model based, respectively, on subjective and...
Seal: A Framework for Secure Mobile Computations (1999)
. The Seal calculus is a distributed process calculus with localities and mobility of computational entities called seals. Seal is also a framework for writing secure distributed applications over...
Mobile Computations and Hostile Hosts (1999)
This paper scratches the surface of the problem of classifying the attacks that a mobile computation can be subjected to in an open network. The discussion is based on a simplified version of the...
Dependent Types With Subtyping and Late-Bound Overloading (1999)
We present a calculus with dependent types, subtyping and late-bound overloading. Besides its theoretical interest this work is motivated by several practical needs that range from the definition of...
Dependent Types With Subtyping and Late-Bound Overloading (1999)
We present a calculus with dependent types, subtyping and late-bound overloading. Besides its theoretical interest this work is motivated by several practical needs that range from the definition of...
Towards a Calculus of Secure Mobile Computations (1998)
The Seal calculus is a calculus of mobile computations designed for programming secure distributed applications over large scale open networks. The calculus is a distributed variant of the...
A Calculus of Secure Mobile Computations (1998)
The seal-calculus is a distributed process calculus in which locations and movement of computational entities are explicit. The calculus is targeted at secure distributed applications over large...
Parasitic Methods: An Implementation of Multi-Methods for Java (1997)
John Boyland, Giuseppe Castagna
In an object-oriented programming language, method selection is (usually) done at run-time using the class of the receiver. Some object-oriented languages (such as CLOS) have multi-methods which...
Sous-Typage Et Programmation Orientée à Objets (1997)
Giuseppe Castagna, Ecole Jeunes, Chercheurs Gdr Programmation
this paper, simple records suffice. We do not give the definition of the encoding. Just remember that all the terms and types written below are encodable in &.
Instance Variables Specialization in Object-Oriented Programming (1996)
One of the most bothering restrictions of statically typed objectoriented languages is that the type of mutable instance variables, cannot be specialized in a subclass. This restriction is in...
Programmation Modulaire Avec Surcharge Et Liaison Tardive (1996)
Mara-Virginia Aponte, Giuseppe Castagna
Introduction Les systemes de modules a la SML [Mac85, MTH90] sont tres generaux et puissants. Ils permettent un decoupage modulaire des programmes et la definition de transformations (appelees...
Covariance and contravariance: Conflict without a cause (1995)
In type-theoretic research on object-oriented programming, the issue of “covarianceversus con-travariance ” is atopicof continuing debate. In this short notewe argue that covariance and...
Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, Jonathan Eifrig, Scott F. Smith, Valery Trifonov, ...
Giving types to binary methods causes significant problems for object-oriented language designers and programmers. This paper offers a comprehensive description of the problems arising from typing...
Integration of Parametric and "ad Hoc" Second Order Polymorphism in a Calculus With Subtyping (1995)
.In this paper we define an extension of F [CG92] to which we add functions that dispatch on different terms according to the type they receive as argument. In other words, we enrich the explicit...
A Calculus for Overloaded Functions with Subtyping (1995)
Giuseppe Castagna, Giorgio Ghelli, Giuseppe Longo
We present a simple extension of typed -calculus where functions can be overloaded by putting different "branches of code" together. When the function is applied, the branch to execute is...
A Calculus For Overloaded Functions With Subtyping (1995)
In type-theoretic research on object-oriented programming, the issue of ``covariance versus contravariance'' is a topic of continuing debate. In this short note we argue that covariance and...
A Calculus for Overloaded Functions with Subtyping (1995)
Giuseppe Castagna, Giorgia Ghelli, Giuseppe Longo
We present a simple extension of typed -calculus where functions can be overloaded by putting different "branches of code" together. When the function is applied, the branch to execute is...
Gary T. Leavens, Benjamin Pierce, Giuseppe Castagna, Kim Bruce, Kim Bruce, ...
data types, modules, packages; F.3.1 [Logics and Meanings of Programs ] Specifying and Verifying and Reasoning about Programs --- logics of programs; F.3.2 [Logics and Meanings of Programs ] Studies...
A Meta-Language for Typed Object-Oriented Languages (1995)
. In [3] we defined the &-calculus, a simple extension of the typed -calculus to model typed object-oriented languages. To develop a formal study of type systems for object-oriented languages we...
A Calculus for Overloaded Functions with Subtyping (Extended Abstract) (1995)
Giuseppe Castagna, Giorgio Ghelli, G. Longo
We present a simple extension of typed -calculus where functions can be overloaded by adding different "pieces of code". In short, the code of an overloaded function is formed by several...
Decidable Bounded Quantification (1994)
Giuseppe Castagna, Benjamin C. Pierce
The standard formulation of bounded quantification, system F , is difficult to work with and lacks important syntactic properties, such as decidability. More tractable variants have been studied, but...
Decidable Bounded Quantification (1994)
Giuseppe Castagna, Benjamin C. Pierce
The standard formulation of bounded quantification, system F , is difficult to work with and lacks important syntactic properties, such as decidability. More tractable variants have been studied, but...
Foundations of Object-Oriented Languages - 2nd Workshop report (1994)
Giuseppe Castagna, Gary T. Leavens, Gary T. Leavens
data types, modules, packages; F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning about Programs --- logics of programs; F.3.2 [Logics and Meanings of Programs] Semantics...
Covariance and Contravariance: Conflict without a Cause (1994)
In type theoretic research on object-oriented programming the "covariance versus contravariance issue" is a topic of continuing debate. In this short note we argue that covariance and...
... : integrating parametric and "ad hoc" second order polymorphism (Extended Abstract) (1993)
In the last years several object-oriented database systems have come to life. However among them there is a lack of statically strongly typed languages. This is a very important deficiency especially...
A Semantics for a Stratified λ&-Early: A Calculus with Overloading and Early Binding (1993)
Giuseppe Castagna, Giorgio Ghelli, Giuseppe Longo
The role of λ-calculus as core functional language is due to its nature as "pure" theory of functions. In the present approach we use the functional expressiveness of typed λ-calculus and...
A Meta-Language for Typed Object-Oriented Languages (1993)
In [12] we defined the &-calculus, a simple extension of the typed -calculus to model typed object-oriented languages. This paper is the continuation or, rather, the companion of [12] since it...