Current Past Me Papers Talks Artifacts Extra HotPage

A Theory of Objects

This book develops a theory of objects as a foundation for object-oriented languages and programming. Our theory provides explanations for object-oriented notions in terms of a few basic primitives, and can be useful for the design and understanding of programming languages.

A Theory Of Objects (Springer eBook)
A theory of primitive objects: Untyped and first-order systems (TACS'94, I&C 1996)
A theory of primitive objects: Second-order systems (ESOP'94, SCP 1995)
A semantics of object types (LICS'94)
An imperative object calculus (TAPSOFT'95, TAPOS 1995)
An imperative object calculus: Basic typing and soundnes (SIPL'95)
An interpretation of objects and object types (POPL'96)
On subtyping and matching (ECOOP'95, TOPLAS 1996)
info A Theory of Objects (Sydney 1997-08-04..15)
info A Theory of Objects (ECOOP'97 Tutorial)
info A Theory of Objects (OOPSLA'96 Tutorial)
info Class-based vs Object-based Languages (PLDI'96 Tutorial)
info A Theory of Objects (LICS'97 Invited Talk)
info Objects, Classes, Abstractions (FOOL'97 Invited Talk)
info Foundations of Object-Oriented Programming (Horizon Day 1995)
info On Subtyping and Matching (ECOOP'95 Invited Talk)
info Operationally Sound Update (HOOTS'95)
info An Imperative Object Calculus (FASE'95)
info Object Types with Self (FOOL'94)
info A Theory of Primitive Objects (ESOP'94 Invited Talk)

Ambient Calculus

There are two distinct areas of work in mobility: mobile computing, concerning computation that is carried out in mobile devices (laptops, personal digital assistants, etc.), and mobile computation, concerning mobile code that moves between devices (applets, agents, etc.). We aim to describe all these aspects of mobility within a single framework that encompasses mobile agents, the ambients where agents interact and the mobility of the ambients themselves.

Types for the Ambient Calculus (I&C)
Mobility and Security (Chapter for Foundations of Secure Computation) (A summary of several  Ambients papers)
Abstractions for Mobile Computation (Chapter for Secure Internet Programming)
Equational Properties of Mobile Ambients (ETAPS'99, MSCS)
Ambient Groups and Mobility Types (TCS'00)
Types for Mobile Ambients (POPL'99)
Mobility Types for Mobile Ambients (ICALP'99)
Mobile Ambient Synchronization (SRC 1997)
Mobile Ambients (ETAPS'98/TCSB'00)
info Mobility and Security (Marktoberdorf'99)
info Abstractions for Mobile Computation (FMOODS'97 Tutorial)
info Mobile Ambients (ETAPS'98)
info Abstractions for Mobile Computation (Princeton 1997-04)
info What is the Web's Model of Computation? (WWW5 1996)
info  Wikipedia Entry

Subtyping & OOP

The purpose of this line of work is to devise type systems where subtyping is an orthogonal concept that applies to all type constructions, including data types, function types, polymorphic types, abstract types, and recursive types. Expressive power and feasibility of typechecking are our major concerns. Expressive power alone might point us to viewing subtypes as arbitrary subsets, but the desire to perform typechecking leads us to a more restricted, structural, notion of subtyping.

Comparing Object Encodings (TACS'97, I&C 1999)
On Binary Methods (TAPOS 1995)
Subtyping and parametricity (LICS'94)
Extensible records in a pure calculus of subtyping (MIT Press 1994)
An extension of system F with subtyping (I&C 1994)
An implementation of F<: (SRC 1993)
Subtyping recursive types (POPL'91, TOPLAS 1993)
A semantic basis for Quest (LISP&FP'90, JFP 1991)
Operations on records (MFPS'89, MSCS 1991, MIT Press)
Structural subtyping and the notion of power type (POPL'88)
Amber (Springer 1986)
The amber machine (Springer 1986)
Typechecking dependent types and subtypes (FLFP'86)
On understanding types, data abstraction, and polymorphism (CS 1985)
A semantics of multiple inheritance (SDT'84, I&C 1988, MorganKaufmann 1990)
 Position Papers
Bad engineering properties of object-oriented languages (CS 1996)
 Edited Proceedings
ECOOP 2003 - Object-Oriented Programming
info Typed Foundations of Object Oriented Programming (POPL'92 Tutorial)
info An Accidental Simula User (2007 Dahl-Nygaard Senior Prize)
info Objects, Classes, Abstractions (FOOL'97)
info Everything is an Object (ECOOP'97 WS on Prototype-based languages)
info A Semantics of Multiple Inheritance (SDT'84)

Semantics & Type Theory

"Parametric polymorphism is more regular and may be illustrated by an example. Suppose f is a function whose argument is of type A and whose results is of B (so that the type of f might be written A => B), and that L is a list whose elements are all of type A (so that the type of L is A list). We can imagine a function, say Map, which applies f in turn to each member of L and makes a list of the results. Thus Map[f,L] will produce a B list. We would like Map to work on all types of list provided f was a suitable function, so that Map would have to be polymorphic. However its polymorphism is of a particularly simple parametric type which could be written (A =>B, A list) => B list, where A and B stand for any types. Polymorphism of both classes presents a considerable challenge to the language designer, but it is not one which we shall take up here." Christopher Strachey, Fundamental Concepts in Programming Languages, 1967.

Classical Cut Elimination in the Pi-Calculus
From X to Pi: Representing Classical Sequent Calculus in Pi-calculus (CL&C'08)
Secrecy and Group Creation (I&C'05 - Concur'00)
Type Systems (Chapter for the CRC Handbook of Computer Science ad Engineering, 2nd Edition)
Program Fragments, Linking, and Modularization (POPL'97)
Dynamic typing in polymorphic languages (JFP 1995)
Formal parametric polymorphism (POPL'93, TCS 1993)
Explicit substitutions (POPL'90, JFP 1991)
Dynamic typing in a statically-typed language (POPL'89, TOPLAS 1991)
Abstract types and the dot notation (TC2WC'90)
Typeful programming (Springer 1989)
Phase Distinctions in Type Theory (Unpublished)
Basic polymorphic typechecking (SCP 1987)
A polymorphic lambda-calculus with Type:Type (SRC 1986)
Real time agents (ICALP'82)
Analog processes (MFCS'80)
 Edited Proceedings
Computation Meaning and Logic: Articles dedicated to Gordon Plotkin
POPL'98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
info Type-Driven Language Design (PLDI'95 Tutorial)
info Typeful Programming (Rio 1898, Bombay 1992)
info Data Abstraction, Modularization, and Reusability (U.Texas Year of Programming 1986)
info From C# to C∞ (2nd Rotor WS 2003)
info Secrecy and Group Creation (MFCSIT'00)
info Program Fragments, Linking, and Modularization (POPL'97)

Spatial Logics

Spatial logics are specification logics for describing the behavior and spatial structure of concurrent systems. Logics for concurrent systems are certainly not new, but the intent to describe spatial properties, and in particular the spatial structure of distributed and mobile systems, seems to have arisen only recently. The spatial properties we consider are essentially of two kinds: whether a system is composed of two or more identifiable subsytems, possibly including hierarchies of named locations, and whether a system restricts the use of certain resources to certain subsytems. The latter, in particular, concerns specifying systems that deal with fresh or secret resources such as keys, nonces, channels, or locations.

 Papers for Processes
A Spatial Logic for Concurrency (Part I) (I&C)
A Spatial Logic for Concurrency (Part II) (TCS)
A Specification Logic for Mobility. Luis Caires. (DI/FCT/UNL Technical Report 4/2000)
Verifiable and Executable Logic Specifications of Concurrent Objects in Lpi. Luis Caires and Luis Monteiro. (ETAPS/ESOP98)
 Papers for Ambients
Anytime, Anywhere (POPL'00)
Logical Properties of Name Restriction (TLCA'01)
Ambient Logic (MSCS limbo)
 Papers for Trees
Manipulating Trees with Hidden Labels (PlotkinVolume'06)
Deciding Validity in a Spatial Logic for Trees (JFP)
Describing Semistructured Data (SIGMOD Record)
A Query Language Based on the Ambient Logic (MSCS)
 Papers for Graphs
A Spatial Logic for Querying Graphs (ICALP'02)
info Mobility and Spatial Logics PDF PDF   (Bertinoro School '05)
info Manipulating Trees with Hidden Labels (FOSSACS'03)
info A Spatial Logic for Concurrency (CONCUR'02)
info Spatial Logics for Distributed Systems (FWAN'02, Strachey Lecture '02)
info A Query Language Based on the Ambient Logic (Concoord Workshop'01)
info Logics for Mobility (Cambidge, Nov '00. Lausanne, Oct '00, Tokyo, Aug '00)
info Anytime, Anywhere (POPL'00)

Distributed Systems

The Internet and the World-Wide-Web provide a computational infrastructure that spans the planet. It is appealing to imagine writing programs that exploit this global infrastructure. Unfortunately, the Web violates many familiar assumptions about the behavior of distributed systems, and demands novel and specialized programming techniques.

Modern Concurrency Abstractions for C# (ECOOP'02, TOPLAS 2004)
Wide Area Computation (ICALP'99)
Service Combinators for Web Computing (DSL'97, TSE 1999)
Distributed applications in a multimedia setting (IWHD'95)
Migratory Applications (UIST'95, Springer 1997)
A Language with Distributed Scope (POPL'95, Computing Systems 1995)
Obliq: A language with distributed scope (SRC 1994)
An implementation model of rendezvous communication (Springer 1985)
 Book Intro
Mobile Computation (Springer 1997)
 Edited Collection
Internet Programming Languages (Springer 1999)
 Position Papers
Global computation (CS 1996, SIGPLAN Notices 1997)
Mobile Computation (Stanford 1995)
info Computation on Wide Area Networks PDF PDF PDF PDF PDF  (Lipari School '01)
info Transitions in Programming Models (ICSE'05 Keynote Talk)
info Globality (ETAPS'01 Invited Talk)
info Wide Area Computation (Valladolid, Nov '00. Tokyo, Aug'00)
info Global Computing (Edinburgh, Sep '00)
info Distributed Mobile Computation in Obliq (1997)
info Obliq: A Languages with Distributed Scope (1995)
Migratory Applications (Video 1995)
Obliq language definition and manual
Obliq examples
info Obliq software is included in Modula-3 distributions

Databases & Semistructured Data

Data orientation has traditionally been the main characteristic of information systems, but has also played an increasingly important role in general-purpose programming languages. At the same time, information systems have evolved towards more expressive ways of modelling reality, which has meant more complex data models and more flexible and integrated query languages. Powerful query languages tightly coupled with complex data models have all the characteristics of programming languages, suggesting that there should be a systematic integration. We argue that type theory (the formal study of type, or classification, systems) is the correct framework within which to study and carry out such unification. In this framework we can analyze existing integrated data-oriented systems and to design better ones.

Greedy Regular Expression Matching (ICALP'04)
Describing Semistructured Data (SIGMOD Record)
Semistructured Computation (DBPL'99)
Types for data-oriented languages (DBPL'99)
A pure calculus of subtyping, and applications (outline) (DBPL'91)
Persistence and Type Abstraction (Data Types and Persistence, 1988)
Galileo: a strongly typed, interactive, conceptual language (TODS 1985)
info Semistructured Computation (DBPL'99)
Persistence and Type Abstraction (Appin 1985)
info History of the Galileo Language

Functional Languages

Much of the early literature on programming languages concentrated on the need to master the complex control flows permitted by unrestricted machine languages, so as to increase confidence in program correctness. Thus, concurrent programming developed the discipline of guarded commands, algorithmic programming developed the notion of structured programs, and symbolic programming embraced the notion of higher-order functions from mathematics and logic.

Compiling a functional language (POPL'84)
Stream Input/Output (Polymorphism 1983)
ML under Unix (Polymorphism 1983)
The Functional Abstract Machine (Polymorphism 1983)
Two-dimensional syntax for functional languages (ECICS'82)
Polymorphism - The ML/LCF/Hope Newsletter I.0 PDF, I.1 PDF, I.2 PDF, I.3 PDF, II.1 PDF, II.2 PDF. (1982-1985)
 Master Thesis
Una teoria dei linguaggi applicativi (U.Pisa 1978)


The goal of Modula-3 is to be as simple and safe as it can be while meeting the needs of modern systems programmers. Instead of exploring new features, we studied the features from the Modula family of languages that have proven themselves in practice and tried to simplify them and fit them into a harmonious language. We found that most of the successful features were aimed at one of two main goals: greater robustness, and a simpler, more systematic type system.

Systems Programming with Modula-3 (Prentice Hall)
The Modula-3 Type System (POPL'89)
[Modula-3] Language definition (Book chapter 2)
Modula-3 report (revised) (SRC 1989)

Extensible Syntax

A frequent dilemma in programming language design is the choice between a language with a rich set of notations and a small, simple core language. We address this dilemma by proposing extensible grammars, a syntax-definition formalism for incremental language extensions and restrictions.

Extensible syntax with lexical scoping (SRC 1994)
Extensible grammars for language specialization (DBPL'93)

User Interfaces

A bitmap screen is a graphic universe where windows, cursors and icons live in harmony, cooperating with each other to achieve functionality and asthetics. Of course it is difficult to resist the temptation to break these rules.

Building user interfaces by direct manipulation (UIS'88)
Squeak: a language for communicating with mice (SIGGRAPH'85)
Crabs: the bitmap terror (Bell Labs 1985)
Building user interfaces by direct manipulation (DEC Video 1987)

Computer Architecture

We apply algebraic techniques to various aspects of hardware description and verification, with particular emphasis on VLSI (Very Large Scale Integration) circuit design. A simple and uniform notation for the description of networks of hardware components is introduced. It is shown how to impose planarity constraints, and how to treat regular and repetitive structures in convenient ways.

An algebraic approach to VLSI design (VLSI'81)
Sticks&Stones: An Applicative VLSI Design Language (U.Edinburgh 1981)
Multiprocessing implementation of a high-level machine language (RdI 1978)
PhD Thesis
An Algebaic Approach to Hardware Description and Verification (U.Edinburgh 1982)