Dave Cunningham, Werner Dietl, Sophia Drossopoulou, Peter Müller, Er J. Summers
Abstract. The Universe Type System is an ownership type system for object-oriented programming languages that hierarchically structures the object store; it is used to reason modularly about...
Mariangiola Dezani-ciancaglini, Sophia Drossopoulou, Dimitris Mostrous, Nobuko Yoshida
A session takes place between two parties; after establishing a connection, each party interleaves local computations and communications (sending or receiving) with the other. Session types...
Lock Inference Proven Correct (2009)
Dave Cunningham, Sophia Drossopoulou, Susan Eisenbach
Abstract. With the introduction of multi-core CPUs, multi-threaded programming is becoming significantly more popular. Unfortunately, it is difficult for programmers to ensure their code is correct...
Aliasing, confinement, and ownership in object-oriented programming (2009)
Drossopoulou, Sophia, Müller, Peter, Noble, James, Wrigstad, Tobias
The power of objects lies in the flexibility of their interconnection structure. But this flexibility comes at a cost. Because an object can be modified via any alias, object-oriented programs are...
Diomidis Spinellis Publications An Object Model for Multiparadigm Programming (2008)
Diomidis Spinellis, Sophia Drossopoulou, Susan Eisenbach
This is an HTML rendering of a working paper draft that led to a publication. The publication should always be cited in preference to this draft using the following reference:
2. IMPLEMENTING STATE CLASSES 3. PARAMETERIZED STATES 4. THE SANTA CLAUS PROBLEM (2008)
Ferruccio Damiani, Nick Cameron, Sophia Drossopoulou, Elena Giachino, Paola Giannini
Up to now state classes NOT promising in sequential programming promising for coordination EOS, Genova, January 9-10, 2006 – p. Up to now state classes NOT promising in sequential programming...
Abstract Tribe: A Simple Virtual Class Calculus 1 (2008)
Dave Clarke, Sophia Drossopoulou
Beginning with BETA, a range of programming language mechanisms have been developed to allow inheritance in the presence of mutually dependent classes. This paper presents Tribe, a type system which...
Permco –APermissive Approach to Covariant Overriding of Subclass Members (2008)
We describe Permco, a permissive approach which allows covariant overriding of instance variables and any overriding of instance methods. Subclasses are considered subtypes. Instance method access is...
John Boyland, Alex Buckley, Patrice Chalin, Dave Clarke, Paola Giannini, Marieke Huisman, ...
This report contains the papers presented at FTfJP ’07: 9th workshop on Formal
Towards an Existential Types Model for Java (2008)
Nick Cameron, Erik Ernst, Sophia Drossopoulou
Abstract. Wildcards extend Java generics by softening the mismatch between subtype and parametric polymorphism. Although they are a key part of the Java 5.0 programming language, a type system...
John Boyland, Alex Buckley, Patrice Chalin, Dave Clarke, Paola Giannini, Marieke Huisman, ...
This report contains the papers presented at FTfJP ’07: 9th workshop on Formal
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...
Abstract Tribe: A Simple Virtual Class Calculus 1 (2008)
Dave Clarke, Sophia Drossopoulou
Beginning with BETA, a range of programming language mechanisms such as virtual classes (class-valued attributes of objects) have been developed to allow inheritance in the presence of mutually...
UJ: Type Soundness for Universe Types (2008)
Dave Cunningham, Adrian Francalanza, Sophia Drossopoulou, Werner Dietl, Peter Müller
Universe types characterise aliasing in object oriented programming languages and are used to reason modularly about programs. In this report we formalise prior work by Müller and Poetzsch-Heffter,...
Towards an Existential Types Model for Java (2008)
Nick Cameron, Erik Ernst, Sophia Drossopoulou
Abstract. Wildcards extend Java generics by softening the mismatch between subtype and parametric polymorphism. Although they are a key part of the Java 5.0 programming language, a type system...
Safety in Flexible Dynamic Linking (2008)
Alex Buckley, Sophia Drossopoulou
Dynamic linking lets programs use the most recent versions of classes without re-compilation. In Java and .NET, bytecode specifies which classes should be dynamically linked. This information...
Overloading and Inheritance (2008)
Davide Ancona Sophia, Davide Ancona, Sophia Drossopoulou, Elena Zucca
Overloading allows several function definitions for the same name, distinguished primarily through different argument types; it is typically resolved at compile-time. Inheritance allows subclasses to...
Aliasing, confinement, and ownership in object-oriented programming (2008)
Drossopoulou, Sophia, Noble, James, Wrigstad, Tobias
The power of objects lies in the flexibility of their interconnection structure. But this flexibility comes at a cost. Because an object can be modified via any alias, object-oriented programs are...
A Featherweight Model for Chorded Languages (2008)
Alexis Petrounias, Sophia Drossopoulou, Susan Eisenbach
Chords are a concurrency mechanism of object-oriented languages inspired by the join of the Join-Calculus. We present SCHOOL, the Small Chorded Object-Oriented Language, a featherweight model which...
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...
A Unified Framework for Verification Techniques for Object Invariants (2008)
Drossopoulou, Sophia, Francalanza, Adrian, Müller, P., Summers, Alexander J.
Object invariants define the consistency of objects. They have subtle semantics, mainly because of call-backs, multi-object invariants, and subclassing. Several verification techniques for object...
Davide Ancona, Sophia Drossopoulou, Elena Zucca
Overloading allows several function definitions for the same name, distinguished primarily through different argument types; it is typically resolved at compile-time. Inheritance allows subclasses to...
A Parallel Genetic Algorithm Approach to the Knife Change Minimisation Problem (2007)
Aneurin M. Easwaran, Sophia Drossopoulou
The knife change minimisation problem is a special case of the Generalised Travelling Salesman Problem arising in the paper industry as a sub-problem to the one-dimensional cutting stock problem. In...
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...
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...
Sophia Drossopoulou, Paola Giannini
Re-classi cation 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 imperative, typed,...
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...
Sophia Drossopoulou, James Noble, Matthew J Smith
Existing ownership type systems require objects to have precisely one primary owner, organizing the heap into an ownership tree. Unfortunately, a tree structure is too restrictive for many programs,...
please, check this site for updates and extensions of this paper (2007)
Sophia Drossopoulou, Adrian Francalanza
Verification of object-oriented programs relies on object invariants which express consistency criteria of objects. The semantics of object invariants is subtle, mainly because of call-backs,...
Session Types for Object-Oriented Languages (2006)
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...
Session Types for Object-Oriented Languages (2006)
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....
Session Types for Object-Oriented Languages (2006)
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 State Abstraction for Coordination in Java-like Languages (2006)
Ferruccio Damiani, Elena Giachino, Paola Giannini, Nick Cameron, Sophia Drossopoulou
Abstract. Objects ’ state, intended as some abstraction over the value of fields, is always in the mind of a COOL (Concurrent Object-Oriented Language) programmer. In fact, as the state of an...
Session Types for Object-Oriented Languages (2006)
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...
Formalization of Generic Universe Types (2006)
Werner Dietl, Sophia Drossopoulou, Peter Müller
Ownership is a powerful concept to structure the object store and to control aliasing and modifications of objects. This paper presents an ownership type system for a Java-like programming language...
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...
Towards Type Inference for JavaScript (2005)
Christopher Anderson Paola, Christopher Anderson, Paola Giannini, Sophia Drossopoulou
Object-oriented scripting languages like JavaScript and Python are popular partly because of their dynamic features. These include the runtime modification of objects and classes through addition of...
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...
Flexible Bytecode for Linking in .NET (2005)
Alex Buckley, Michelle Murray, Susan Eisenbach, Sophia Drossopoulou
Dynamic linking in modern execution environments like .NET is considerably more sophisticated than in the days of C shared libraries on UNIX. One aspect of this sophistication is that .NET assemblies...
Polymorphic Bytecode: Compositional Compilation for Java-like Languages (2005)
Davide Ancona, Ferruccio Damiani, Sophia Drossopoulou, Elena Zucca
We define compositional compilation as the ability to typecheck source code fragments in isolation, generate corresponding binaries, and link together fragments whose mutual assumptions are...
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...
SCHOOL: a Small Chorded Object-Oriented Language (2005)
Sophia Drossopoulou, Alexis Petrounias, Alex Buckley, Susan Eisenbach
Chords are a declarative synchronisation construct based on the Join calculus, available in the programming language C # . Compared with synchronisation constructs in most imperative languages,...
Chai: Traits for Java-like Languages (2005)
Charles Smith, Sophia Drossopoulou
Traits support the factoring out of common behaviour, and its integration into classes in a manner that coexists smoothly with inheritance-based structuring mechanisms.
Simple dependent types: Concord (2004)
Paul Jolly, Sophia Drossopoulou, Christopher Anderson, Klaus Ostermann
Abstract. We suggest a simple model for a restricted form of dependent types in object oriented languages, whereby classes belong to groups and dependency is introduced via intragroup
Simple Dependent Types: Concord Final Year Project Report (2004)
Paul Jolly, Supervised Dr, Sophia Drossopoulou, Christopher Anderson
The organisation of code at an object level has long been considered a prudent approach to software development. However, in many situations the single-class perspective is too fine grained a...
Even more principal typings for Java-like languages (2004)
Davide Ancona, Ferruccio Damiani, Sophia Drossopoulou, Elena Zucca
Abstract. We propose a new type system for Java-like languages which allows compilation of a class in isolation, that is, in a context where no information is available on other classes. Indeed, by...
Even More Principal Typings for Java-like Languages (2004)
Davide Ancona Ferruccio, Davide Ancona, Ferruccio Damiani, Sophia Drossopoulou, Elena Zucca
We propose a new type system for Java-like languages which allows compilation of a class in isolation, that is, in a context where no information is available on other classes. Indeed, by this type...
Flexible Dynamic Linking (2004)
Alex Buckley, Sophia Drossopoulou
Dynamic linking, as in Java and C#, allows users to execute the most recent versions of software without re-compilation or re-linking. Dynamic linking is guided by type names stored in the bytecode.
Even More Principal Typings for Java-like Languages (2004)
Davide Ancona, Ferruccio Damiani, Sophia Drossopoulou, Elena Zucca
We propose a new type system for Java-like languages which allows compilation of a class in isolation, that is, in a context where no information is available on other classes. Indeed, by this type...
Giovanni Lagorio, Giovanni Lagorio, Davide Ancona, Elena Zucca, Gilad Bracha, ...
Type systems for Java separate compilation and selective recompilation by
Flexible models for dynamic linking (2003)
Sophia Drossopoulou, Giovanni Lagorio, Susan Eisenbach
code links further code on the fly, as needed; and thus, end-users receive updates automatically. On the down side, each program run may link different versions of the same code, possibly causing...
Flexible models for dynamic linking (2003)
Sophia Drossopoulou, Giovanni Lagorio, Susan Eisenbach
code links further code on the fly, as needed; and thus, end-users receive updates automatically. On the down side, each program run may link different versions of the same code, possibly causing...
Cheaper reasoning with ownership types (2003)
Matthew Smith, Sophia Drossopoulou
Abstract. We use ownership types to facilitate program verification. Namely, an assertion that has been established for a part of the heap which is unaffected by some execution will still hold after...
Refined Effects for Unanticipated Object Re-classification: Fickle_3 (Extended Abstract) (2003)
Ferruccio Damiani, Sophia Drossopoulou, Paola Giannini
In previous work on the language Fickle and its extension Fickle_II Dezani and us introduced language features for object re-classification for imperative, typed, class-based, object-oriented...
Flexible, Source Level Dynamic Linking And Re-Linking (2003)
Sophia Drossopoulou, Susan Eisenbach
We give a formal semantics for dynamic linking and re-linking of code. The semantics is at source language level, and allows linking at a finer grain than current Java or C# implementations: Besides...
Flexible Models for Dynamic Linking (2003)
Sophia Drossopoulou, Giovanni Lagorio, Susan Eisenbach
Dynamic linking supports flexible code deployment: partially linked code links further code on the fly, as needed; and thus, end-users receive updates automatically. On the down side, each program...
Flexible Models for Dynamic Linking (2003)
Sophia Drossopoulou, Giovanni Lagorio, Susan Eisenbach
Dynamic linking supports flexible code deployment: partially linked code links further code on the fly, as needed; and thus, end-users receive updates automatically. On the down side, each program...
Dave Clarke (ed.), Edited Dave Clarke, Dave Clarke (editor, Rasekhar Boyapati, Robert Lee, Martin Rinard, ...
This paper describes an e#cient technique for supporting safe runtim downcasts in asystem with ownership types. This technique uses the type passing approach, but avoids the associated significant...
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...
Three Case studies in FickleII (2002)
In this paper we explore the use of object reclassification as in Fickleii [3] through the study of three examples. These examples are normal and privileged accounts, empty or nonempty lists, and...
Sophia Drossopoulou, Susan Eisenbach
Through dynamic linking, Java supports a novel paradigm for code deployment, which ensures fast program start-up and linking with the most recent version of code. Thus Java dynamic linking, gives...
Ownership, Encapsulation and the Disjointness of Type and Effect (2002)
Dave Clarke, Sophia Drossopoulou
Ownership types provide a statically enforceable notion of object-level encapsulation. We extend ownership types with computational e#ects to support reasoning about objectoriented programs. The...
More dynamic object re-classification: FickleII (2002)
Sophia Drossopoulou, Paola Giannini
Reclassification changes the class membership of an object at run-time while retaining its identity. We suggest language features for object reclassification, which extend an imperative, typed,...
Overloading and inheritance (2001)
Davide Ancona, Sophia Drossopoulou, Elena Zucca
Abstract. Overloading allows several function denitions for the same name, distinguished primarily through dierent argument types, and is typically resolved at compile-time. Inheritance allows...
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...
An abstract model of Java dynamic linking and loading (2001)
We suggest a model for dynamic loading and linking as in Java. We distinguish five components in a Java implementation: evaluation, resolution, loading, verification, and preparation -- with their...
Sophia Antipolis, Sophia Drossopoulou, Susan Eisenbach, Bart Jacobs, Gary T. Leavens, I. Attali, ...
Towards an abstract model of Java dynamic linking and verfication (2000)
We suggest a model for dynamic linking and verification as in Java. We distinguish five components in a Java implementation: evaluation, resolution, loading, verification, and preparation-- with...
Overloading and Inheritance in Java (Extended Abstract) (2000)
Davide Ancona, Elena Zucca, Sophia Drossopoulou
The combination of overloading and inheritance in Java introduces questions about function selection, and makes some function calls ambiguous. We believe that the approach taken by Java designers is...
Overloading and Inheritance in Java (2000)
Davide Ancona, Elena Zucca, Sophia Drossopoulou
The combination of overloading and inheritance in Java introduces questions about function selection, and makes some function calls ambiguous. We believe that the approach taken by Java designers is...
Java Exceptions Throw no Surprises (2000)
Sophia Drossopoulou, Tanya Valkevych
We outline a proof of type soundness for Java exceptions and exception handling. We distinguish between normal execution, where no exception is thrown -- or, more precisely, any exception thrown is...
Java exceptions throw no surprises (2000)
Sophia Drossopoulou, Tatyana Valkevych
Abstract We present a summary of our formalization of the static and dynamic semantics of Java related to exceptions. We distinguish between normal execution, where no exception is thrown- or, more...
Formalising composition-oriented programming (1999)
We present a snapshot of work in progress to define a formal model of the composition technology which underpins Subject-oriented and Aspectoriented programming. 1
Objects Dynamically Changing Class (1999)
Sophia Drossopoulou, Mariangiola Dezani-ciancaglini, Ferruccio Damiani, Paola Giannini
We suggest language features that allow objects to mutate, i.e. change their class membership at run-time. These features could extend an imperative, typed, class-based, object-oriented language like...
Sophia Drossopoulou, Susan Eisenbach, David Wragg
We propose a calculus describing compilation and linking in terms of operations on fragments, i.e. compilation units, without reference to their specific contents. We believe this calculus faithfully...
What can Java Binary Compatibility mean? (1999)
Sophia Drossopoulou, Susan Eisenbach, David Wragg
Java binary compatibility prescribes conditions under which modiøcation and re-compilation of classes does not necessitate re-compilation of further classes importing the modiøed classes. Binary...
What is Java Binary Compatibility? (1998)
Sophia Drossopoulou, David Wragg, Susan Eisenbach
Separate compilation allows the decomposition of programs into units that may be compiled separately, and linked into an executable. Traditionally, separate compilation was equivalent to the...
Towards an Operational Semantics and Proof of Type Soundness for Java (1998)
Sophia Drossopoulou, Susan Eisenbach
this paper does not obey the subsumption rule. For instance, the type of aPhil.like is Phil, but the type of pascal.like
Java Binary Compatibility is Almost Correct (1998)
David Wragg, Sophia Drossopoulou, Susan Eisenbach
The Java language description is unusual in that it defines the effect of interleaving separate compilation and source code modications. In Java, certain source code modications, such as adding a...
What is Java Binary Compatibility? (1998)
Sophia Drossopoulou, David Wragg, Susan Eisenbach
Separate compilation allows the decomposition of programs into units that may be compiled separately, and linked into an executable. Traditionally, separate compilation was equivalent to the...
Sophia Drossopoulou, Susan Eisenbach, David Wragg
We suggest a calculus describing compilation and linking in terms of operations on fragments, i.e. compilation units, without reference to their specific contents. We believe this calculus faithfully...
Is the Java type system sound (1997)
Sophia Drossopoulou, Susan Eisenbach
We argue that the Java type system is sound, by proving a subject reduction theorem. We define a subset of Java, a language which is safe and which reflects the most essential features of Java, a...
Java is Type Safe - Probably (1997)
Sophia Drossopoulou, Susan Eisenbach
. Amidst rocketing numbers of enthusiastic Java programmers and internet applet users, there is growing concern about the security of executing Java code produced by external, unknown sources. Rather...
Java is Type Safe - Probably (1996)
Sophia Drossopoulou, Susan Eisenbach
. Amidst rocketing numbers of enthusiastic Java programmers and internet applet users, there is growing concern about the security of executing Java code produced by external, unknown sources. Rather...
Using Objects for Structuring Multiparadigm Programming Environments (1995)
Diomidis Spinellis, Sophia Drossopoulou, Susan Eisenbach
Multiparadigm programming allows the programmer to write the implementation of a system in a number of different paradigms. We describe our approach to multiparadigm programming based on modeling...
Diomidis Spinellis, Sophia Drossopoulou, Susan Eisenbach
Abstract. Computer language paradigms offer linguistic abstractions and proof theories for expressing program implementations. Similarly, system architectures offer the hardware abstractions and...
Diomidis Spinellis, Sophia Drossopoulou, Susan Eisenbach
. Computer language paradigms offer linguistic abstractions and proof theories for expressing program implementations. Similarly, system architectures offer the hardware abstractions and quantitative...