Type inference for variant object types (2009)
Michele Bugliesi, Foscari Venezia
Existing type systems for object calculi [1] are based on invariant subtyping. Subtyping invariance is required for soundness of static typing in the presence of method overrides, but it is often in...
Information Flow Security in Boxed Ambients Abstract (2009)
Silvia Crafa, Michele Bugliesi, École Normale Supérieure
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...
Abstract Object Calculi with Dynamic Messages (2009)
Michele Bugliesi, Silvia Crafa
Dynamic messages, as proposed in [Nis98], are first-class expressions that may occur as messages within programs: being first-class, they may dynamically be bound to program variables, and evaluated...
J. LOGIC PROGRAMMING 1993:12:1-199 1 MODULARITY IN LOGIC PROGRAMMING (2008)
Michele Bugliesi, Evelina Lamma, Paola Mello
\Lambda The research on modular logic programming has evolved along two different directions during the past decade. Various papers have focused primarily on the problems of programming-in-the-large....
IOS Press A Subtyping for Extensible, Incomplete Objects To Helena Rasiowa: in memoriam (2008)
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...
Oriented Constructs, Type Structure (2008)
Viviana Bono, Michele Bugliesi, Silvia Crafa
Finding typed encodings of object-oriented into procedural or functional programming sheds light on the theoretical foundations of object-oriented languages and their specific typing constructs and...
Michele Bugliesi, Foscari Venezia
tem allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type system is its ability to capture both explicit and implicit process and ambient...
Abstract Matching [for] the Lambda Calculus of Objects ⋆ (2008)
Viviana Bono, Michele Bugliesi
A relation between recursive object types, called matching, has been proposed [8] to provide an adequate typing of inheritance in class-based languages. This paper investigates the role of this...
Abstract Object Calculi in Linear Logic (2008)
Michele Bugliesi, Giorgio Delzanno, Luigi Liquori, Maurizio Martelli
Several calculi of objects have been studied in the recent literature, that support the central features of object-based languages: messages, inheritance, dynamic dispatch, object update and...
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...
Silvia Crafa, Michele Bugliesi, École Normale Supérieure
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, Marco Giunti
The use of types to control the behavior of processes in the pi-calculus is a long known and well established technique. The idea was first introduced by Pierce and Sangiorgi in their seminal work on...
Existing type systems for object calculi [2] are based on invariant subtyping. Subtyping invariance is required for soundness of static typing in the presence of method overrides, but it is often in...
Abstract Communication and Mobility Control in Boxed Ambients ⋆ (2008)
Michele Bugliesi, Silvia Crafa, Massimo Merro, Vladimiro Sassone
primitives acting across ambient boundaries. The expressiveness of the new communication model is achieved at the price of communication interferences whose resolution requires synchronisation of...
Abstract Space-Aware Ambients and Processes ⋆ (2008)
Franco Barbanera, Michele Bugliesi, Vladimiro 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...
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...
Type inference for variant object types (2007)
Existing type systems for object calculi [1] are based on invariant subtyping. Subtyping invariance is required for soundness of static typing in the presence of method overrides, but it is often in...
Type inference for variant object types (2007)
Michele Bugliesi, Foscari Venezia
Existing type systems for object calculi [1] are based on invariant subtyping. Subtyping invariance is required for soundness of static typing in the presence of method overrides, but it is often in...
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...
Object calculi with dynamic messages (2007)
Michele Bugliesi, Silvia Crafa
Dynamic messages, as proposed in [Nis98], are rst-class expressions that may occur as messages within programs: being rst-class, they may dynamically be bound to program variables, and evaluated to...
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...
Type inference for variant object types (2007)
Existing type systems for object calculi [1] are based on invariant subtyping. Subtyping invariance is required for soundness of static typing in the presence of method overrides, but it is often in...
Type inference for variant object types (2007)
Existing type systems for object calculi [1] are based on invariant subtyping. Subtyping invariance is required for soundness of static typing in the presence of method overrides, but it is often in...
Dynamic types for authentication (2007)
Michele Bugliesi, Riccardo Focardi, Matteo Maffei
We propose a type and effect system for authentication protocols built upon a tagging scheme that formalizes the intended semantics of ciphertexts. The main result is that the validation of each...
Reliable and Efficient Computational Geometry Via Controlled Perturbation (2006)
Mehlhorn, Kurt, Osbild, Ralf, Sagraloff, Michael, Bugliesi, Michele, Preneel, Bart, Sassone, Vladimir, ...
Most algorithms of computational geometry are designed for the Real-RAM and non-degenerate input. We call such algorithms idealistic. Executing an idealistic algorithm with floating point arithmetic...
A Faster Deterministic Algorithm for Minimum Cycle Bases in Directed Graphs (2006)
Hariharan, Ramesh, Telikepalli, Kavitha, Mehlhorn, Kurt, Bugliesi, Michele, Preneel, Bart, Sassone, Vladimir, ...
We consider the problem of computing a minimum cycle basis in a directed graph. The input to this problem is a directed graph G whose edges have non-negative weights. A cycle in this graph is...
Communication and Mobility Control in Boxed Ambients (2005)
Michele Bugliesi, Silvia Crafa, Massimo Merro, Vladimiro Sassone
Boxed Ambients (BA) replace Mobile Ambients ’ open capability with communication primitives acting across ambient boundaries. The expressiveness of the new model of communication is achieved at the...
Analysis of typed analyses of authentication protocols (2005)
Michele Bugliesi, Riccardo Focardi, Matteo Maffei
Abstract. This paper contrasts two existing type-based techniques for the analysis of authentication protocols. The former, proposed by Gordon and Jeffrey, uses dependent types for nonces and...
Analysis of typed analyses of authentication protocols (2005)
Michele Bugliesi, Riccardo Focardi, Matteo Maffei
This paper contrasts two existing type-based techniques for the analysis of authentication protocols. The former, proposed by Gordon and Jeffrey, uses dependent types for nonces and cryptographic...
Compositional analysis of authentication protocols (2004)
Michele Bugliesi, Riccardo Focardi, Matteo Maffei
We propose a new method for the static analysis of entity authentication protocols. We develop our approach based on a dialect of the spi-calculus as the underlying formalism for expressing protocol...
Type based discretionary access control (2004)
Michele Bugliesi, Dario Colazzo, Silvia Crafa
Abstract. Discretionary Access Control (DAC) systems provide powerful mechanisms for resource management based on the selective distribution of capabilities to selected classes of principals. We...
Type based discretionary access control (2004)
Michele Bugliesi, Dario Colazzo, Silvia Crafa
Abstract. Discretionary Access Control (DAC) systems provide powerful mechanisms for resource management based on the selective distribution of capabilities to selected classes of principals. We...
Compositional Analysis of Authentication Protocols (2004)
Michele Bugliesi, Riccardo Focardi, Matteo Maffei
We propose a new method for the static analysis of entity authentication protocols. We develop our approach based on a dialect of the spi-calculus as the underlying formalism for expressing protocol...
Non-Interference Proof Techniques for the Analysis of Cryptographic Protocols (2003)
Michele Bugliesi, Sabina Rossi
Non-interference has been advocated by various authors as a uniform framework for the formal specification of security properties in cryptographic protocols. Unfortunately, specifications based on...
Context-Sensitive Equivalences for NonInterference based Protocol Analysis (2003)
Michele Bugliesi, Ambra Ceccato, Sabina Rossi
Abstract. We develop new proof techniques, based on non-interference, for the analysis of safety and liveness properties of cryptographic protocols expressed as terms of the process algebra...
Secrecy in untrusted networks (2003)
Michele Bugliesi, Silvia Crafa, Amela Prelic, Vladimiro Sassone
Abstract. We investigate the protection ofmigrating agents against the untrusted sites they traverse. The resulting calculus provides a formal framework to reason about protection policies and...
Secrecy in untrusted networks (2003)
Michele Bugliesi, Silvia Crafa, Amela Prelic, Vladimiro Sassone
Abstract. We investigate the protection of migrating agents against the untrusted sites they traverse. The resulting calculus provides a formal framework to reason about protection policies and...
Secrecy in untrusted networks (2003)
Michele Bugliesi, Silvia Crafa, Amela Prelic, Vladimiro Sassone
Abstract. We investigate the protection of migrating agents against the untrusted sites they traverse. The resulting calculus provides a formal framework to reason about protection policies and...
Non-Interference Proof Techniques for the Analysis of Cryptographic Protocols (2003)
Michele Bugliesi, Ambra Ceccato, Sabina Rossi
Abstract. We develop new proof techniques, based on Non-Interference, for the analysis of safety and liveness properties of cryptographic protocols expressed as terms of the process algebra...
Principles for entity authentication (2003)
Michele Bugliesi, Riccardo Focardi, Matteo Maffei, Fabio Tudone
Abstract. We study the roles of message components in authentication protocols. In particular, we investigate how a certain component contributes to the task of achieving entity authentication. To...
Principles for Entity Authentication (2003)
Michele Bugliesi, Riccardo Focardi, Matteo Maffei
We study the roles of message components in authentication protocols.
Michele Bugliesi, Sabina Rossi
Abstract Non-interference has been advocated by various authors as a uniform frameworkfor the formal specification of security properties in cryptographic protocols. Unfortunately, specifications...
Communication interference in mobile boxed ambients (2002)
Michele Bugliesi, Silvia Crafa, Massimo Merro, Vladimiro Sassone
communication primitives acting across ambient boundaries. Expressiveness is achieved at the price of communication interferences on message reception whose resolution requires synchronisation of...
Communication Interference in Mobile Boxed Ambients (2002)
Michele Bugliesi, Silvia Crafa, Massimo Merro, Vladimiro Sassone
Boxed Ambients (BA) replace Mobile Ambients'open capability with communication primitives acting across ambient boundaries. Expressiveness is achieved at the price of communication interferences...
Communication Interference in Mobile Boxed Ambients (2002)
Michele Bugliesi, Silvia Crafa, Massimo Merro, Vladimiro Sassone
Boxed Ambients (BA) replace Mobile Ambients'open capability with communication primitives acting across ambient boundaries. Expressiveness is achieved at the price of communication interferences...
Typed Interpretations of Extensible Objects (2002)
Viviana Bono, Michele Bugliesi, Silvia Crafa
This paper describes a type preserving and computationally adequate interpretation of a full-edged object calculus that supports message passing and constructs for object update and extension. The...
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, Silvia Crafa
Abstract. 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...
Reasoning about security in mobile ambients (2001)
Michele Bugliesi, Silvia Crafa
Abstract. 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...
Abstract. 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...
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...
Depth subtyping and type inference for object calculi (2000)
Michele Bugliesi, Foscari Venezia
We present a new type system based on the notion of Split types. In this system, every method is assigned two types, namely, an update type and a select type. We show that the system of Split types...
Depth subtyping and type inference for object calculi (2000)
We present a new type system based on the notion of Split types. In this system, every method is assigned two types, namely, an update type and a select type. We show that the system of Split types...
Depth subtyping and type inference for object calculi (2000)
Michele Bugliesi, Foscari Venezia
We present a new type system based on the notion of Split types. In this system, every method is assigned two types, namely, an update type and a select type. We show that the system of Split types...
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...
Interpretations of extensible objects and types (1999)
Viviana Bono, Michele Bugliesi
Abstract. We present a type-theoretic encoding of extensible objects and types. The ambient theory is a higher-order-calculus with polymorphic types, recursive types and operators, and subtyping....
Object Calculi with Dynamic Messages (1999)
Michele Bugliesi, Silvia Crafa
Dynamic messages, as proposed in [Nis98], are first-class expressions that may occur as messages within programs: being first-class, they may dynamically be bound to program variables, and evaluated...
Optimizing Modular Logic Languages (1998)
Michele Bugliesi, Anna Ciampolini, Evelina Lamma, Paola Mello
Several applications in the areas of Software Engineering and Artificial Intelligence require support for modular programming and incremental knowledge organization. Modular logic programming has...
A Subtyping for Extensible, Incomplete Objects (1998)
Viviana Bono, Michele Bugliesi, Mariangiola Dezani-ciancaglini, Luigi Liquori
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 use of...
Matching for the Lambda Calculus of Objects (1998)
Viviana Bono, Michele Bugliesi
A relation between recursive object types, called matching, has been proposed [7] to provide an adequate typing of inheritance in class-based languages. This paper investigates the role of this...
Matching [for] the Lambda Calculus of Objects (1998)
Viviana Bono, Michele Bugliesi
A relation between recursive object types, called matching, has been proposed [8] to provide an adequate typing of inheritance in class-based languages. This
Subtyping Constraints for Incomplete Objects (1997)
Viviana Bono, Michele Bugliesi, Luigi Liquori
Abstract. We extend the type system for the Lambda Calculus of Objects [14] to account for a notion of width subtyping. The main novelties over previous work are the use of bounded quantication to...
Matching Constraints for the Lambda Calculus of Objects (1997)
Viviana Bono, Michele Bugliesi
We present a new type system for the Lambda Calculus of Objects [16], based on matching. The new system retains the property of type safety of the original system, while using implicit match-bounded...
A Lambda Calculus of Incomplete Objects (1996)
Viviana Bono, Michele Bugliesi, Luigi Liquori
Abstract. This paper extends the Lambda Calculus of Objects as proposed in [5] with a new support for incomplete objects. Incomplete objects behave operationally as “standard ” objects; their...
A Lambda Calculus of Incomplete Objects (1996)
Viviana Bono, Michele Bugliesi, Luigi Liquori
Abstract. This paper extends the Lambda Calculus of Objects as proposed in [5] with a new support for incomplete objects. Incomplete objects behave operationally as \standard " objects;...
A linear logic calculus of objects (1996)
Michele Bugliesi, Giorgio Delzanno, Luigi Liquori, Maurizio Martelli
This paper presents a linear logic programming language, called O \Gammaffi, that gives a complete account of an object-oriented calculus with inheritance and override. This language is best...
A Lambda Calculus of Incomplete Objects (1996)
Viviana Bono, Michele Bugliesi, Luigi Liquori
This paper extends the Lambda Calculus of Objects as proposed in [5] with a new support for incomplete objects. Incomplete objects behave operationally as \standard" objects; their typing,...
A Stable Model Semantics for Behavioral Inheritance in Deductive Object Oriented Languages (1995)
Exte Nd Ed, Michele Bugliesi, Hasan M. Jamil
) Michele Bugliesi 1 Hasan M. Jamil 2 Dip. di Matematica Pura ed Applicata Dept. of Computer Science Universit`a di Padova, Italy Concordia University, Canada michele@goedel.math.unipd.it...
A stable model semantics for behavioral inheritance in deductive object oriented languages (1995)
Michele Bugliesi, Hasan M. Jamil
Abstract. We present a model for deductive object oriented query languages with inheritance and overriding. In this model, we consider a DAG like dynamic isa hierarchy and we account for both value...
A logic for encapsulation in object oriented languages (1994)
Michele Bugliesi, Hasan M. Jamil
The language F-logic proposed by Kifer et al. [15] is a very nice declarative formalism for OODBs and is regarded as one of the best developed proposals so far. The work on F-Logic has provided...
A logic for encapsulation in object oriented languages (1994)
Michele Bugliesi, Hasan M. Jamil
Abstract. We present a logic language with encapsulation based on an object-oriented data model. We give a formal account of the semantics of this language by de ning a proof theory, a model theory...
A logic for encapsulation in object oriented languages (1994)
Michele Bugliesi, Hasan M. Jamil
Abstract. We present a logic language with encapsulation based on an object-oriented data model. We give a formal account of the semantics of this language by defining a proof theory, a model theory...
A Logic for Encapsulation in Object Oriented Languages (1994)
Exte Nd Ed, Michele Bugliesi, Hasan M. Jamil
) Michele Bugliesi 1 Dip. di Matematica Pura ed Applicata, Univ. di Padova Via Belzoni 7, I-35131 Padova, Italy e-mail: michele@goedel.math.unipd.it Hasan M. Jamil 2 Department of Computer Science,...
A Logic for Encapsulation in Object Oriented Languages (1994)
Michele Bugliesi, Hasan M. Jamil
We present a logic language with encapsulation based on an object-oriented data model. We give a formal account of the semantics of this language by defining a proof theory, a model theory and a...
Modularity In Logic Programming (1993)
Michele Bugliesi, Evelina Lamma, Paola Mello
ion We mentioned earlier in this section that the choice of TP as the denotation of a program may not yield a satisfactory semantics for the algebra. Indeed, the property of being homomorphic is very...
Partial Deduction for Structured Logic Programming (1993)
Michele Bugliesi, Evelina Lamma, Paola Mello
In this paper we discuss an extension of Partial Deduction in the framework of structured logic programs. The class of programs we consider includes statically configured systems such as block- and...
Michele Bugliesi, Hasan M. Jamil
) Michele Bugliesi 1 Hasan M. Jamil 2 Dip. di Matematica Pura ed Applicata Dept. of Computer Science Universit`a di Padova, Italy Concordia University, Canada michele@goedel.math.unipd.it...