Current | Past | Me | Papers | Talks | Artifacts | Extra | HotPage |

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.

Book

A
Theory Of Objects (Springer eBook)
Papers

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)

Lectures

A
Theory of Objects (Sydney
1997-08-04..15)
A Theory of Objects (ECOOP'97 Tutorial)

A Theory of Objects (OOPSLA'96 Tutorial)

Class-based vs Object-based Languages (PLDI'96 Tutorial)

Talks

A
Theory of Objects (LICS'97 Invited
Talk)
Objects, Classes, Abstractions (FOOL'97 Invited Talk)

Foundations of Object-Oriented Programming (Horizon Day 1995)

On Subtyping and Matching (ECOOP'95 Invited Talk)

Operationally Sound Update (HOOTS'95)

An Imperative Object Calculus (FASE'95)

Object Types with Self (FOOL'94)

A Theory of Primitive Objects (ESOP'94 Invited Talk)

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.

Papers

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
Lectures

Typed
Foundations of Object Oriented Programming
(POPL'92 Tutorial)
Talks

An
Accidental Simula User (2007
Dahl-Nygaard Senior Prize)
Objects, Classes, Abstractions (FOOL'97)

Everything is an Object (ECOOP'97 WS on Prototype-based languages)

A Semantics of Multiple Inheritance (SDT'84)

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)
Lectures

Mobility
and Spatial Logics
(Bertinoro School '05)
Talks

Manipulating
Trees with Hidden Labels (FOSSACS'03)
A Spatial Logic for Concurrency (CONCUR'02)

Spatial Logics for Distributed Systems (FWAN'02, Strachey Lecture '02)

A Query Language Based on the Ambient Logic (Concoord Workshop'01)

Logics for Mobility (Cambidge, Nov '00. Lausanne, Oct '00, Tokyo, Aug '00)

Anytime, Anywhere (POPL'00)

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.

Papers

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)

Talks

Semistructured
Computation (DBPL'99)
Persistence and Type Abstraction (Appin 1985)

Links

History
of the Galileo Language
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.

Book

Systems
Programming with Modula-3 (Prentice
Hall)
Papers

The Modula-3 Type System (POPL'89)
[Modula-3] Language definition (Book chapter 2)

Modula-3 report (revised) (SRC 1989)

Links

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

Papers

Building
user interfaces by direct manipulation
(UIS'88)
Squeak: a language for communicating with mice (SIGGRAPH'85)

Crabs: the bitmap terror (Bell Labs 1985)

Talks

Building
user interfaces by direct manipulation
(DEC Video 1987)
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.

Papers

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)

Lectures

Mobility
and Security (Marktoberdorf'99)
Abstractions for Mobile Computation (FMOODS'97 Tutorial)

Talks

Mobile
Ambients (ETAPS'98)
Abstractions for Mobile Computation (Princeton 1997-04)

What is the Web's Model of Computation? (WWW5 1996)

Links

Wikipedia Entry
"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*.

Papers

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

Lecture

Type-Driven
Language Design (PLDI'95 Tutorial)
Typeful Programming (Rio 1898, Bombay 1992)

Data Abstraction, Modularization, and Reusability (U.Texas Year of Programming 1986)

Talks

From
C# to C∞ (2nd Rotor WS 2003)
Secrecy and Group Creation (MFCSIT'00)

Program Fragments, Linking, and Modularization (POPL'97)

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.

Papers

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)

Lectures

Computation
on Wide Area Networks
(Lipari School '01)
Talks

Transitions
in Programming Models (ICSE'05
Keynote Talk)
Globality (ETAPS'01 Invited Talk)

Wide Area Computation (Valladolid, Nov '00. Tokyo, Aug'00)

Global Computing (Edinburgh, Sep '00)

Distributed Mobile Computation in Obliq (1997)

Obliq: A Languages with Distributed Scope (1995)

Migratory Applications (Video 1995)

Software

Obliq
language definition and manual
Obliq examples

Obliq software is included in Modula-3 distributions

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.

Papers

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)

Newsletter

Polymorphism
- The ML/LCF/Hope Newsletter
I.0
,
I.1
,
I.2
,
I.3
,
II.1
,
II.2
.
(1982-1985)
Master Thesis

Una
teoria dei linguaggi applicativi
(U.Pisa 1978)
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.

Papers

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

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.

Papers

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)