James J. Leifer

Under consideration for publication in J. Functional Programming 1 Acute: High-level programming language design for distributed computation (2008)

Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, Viktor Vafeiadis

† INRIA Rocquencourt Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of...

Abstract Global abstraction-safe marshalling with hash types (2008)

James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough

Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent...

Abstract Acute: high-level programming language design for distributed computation (2008)

Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams

This paper studies key issues for distributed programming in high-level languages. We discuss the design space and describe an experimental language, Acute, which we have defined and implemented....

Under consideration for publication in Formal Aspects of Computing Shallow Linear Action Graphs and their (2008)

James J. Leifer, Robin Milner

Abstract. Action calculi, which generalise process calculi such as Petri nets, π-calculus and ambient calculus, have been presented in terms of action graphs. We here offer linear action graphs as a...

Abstract Acute: High-Level Programming Language Design for Distributed Computation (2008)

Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, Viktor Vafeiadis

Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...

Abstract Global Abstraction-Safe Marshalling with Hash Types (2008)

James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough

Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent...

Under consideration for publication in J. Functional Programming 1 Acute: High-level programming language design (2008)

For Distributed Computation, Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, ...

Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...

Acute: High-Level Programming Language Design (2008)

For Distributed Computation, Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, ...

Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...

y (2007)

James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough, Inria Rocquencourt

Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent...

Abstraction preservation and subtyping in distributed languages (2006)

James J. Leifer

1. Introduction 1.1 Background and motivation Abstract types are a powerful feature of modern programminglanguages. They arise when the implementation of a collection of types and accompanying...

Acute: high-level programming language design for distributed computation (2005)

Sewell, Peter, Leifer, James J., Wansbrough, Keith, Zappa Nardelli, Francesco, Allen-Williams, Mair, Habouzit, Pierre, ...

Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...

Acute: high-level programming language design for distributed computation (2005)

Sewell, Peter, Leifer, James J., Wansbrough, Keith, Zappa Nardelli, Francesco, Allen-Williams, Mair, Habouzit, Pierre, ...

Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...

Acute: high-level programming language design for distributed computation (2005)

Sewell, Peter, Leifer, James J., Wansbrough, Keith, Zappa Nardelli, Francesco, Allen-Williams, Mair, Habouzit, Pierre, ...

Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...

Acute: High-level programming language design for distributed computation : Design rationale and language definition (2004)

Sewell, Peter, Leifer, James J., Wansbrough, Keith, Allen-Williams, Mair, Zappa Nardelli, Francesco, Habouzit, Pierre, ...

This paper studies key issues for distributed programming in high-level languages. We discuss the design space and describe an experimental language, Acute, which we have defined and implemented....

Acute: High-level programming language design for distributed computation : Design rationale and language definition (2004)

Sewell, Peter, Leifer, James J., Wansbrough, Keith, Allen-Williams, Mair, Zappa Nardelli, Francesco, Habouzit, Pierre, ...

This paper studies key issues for distributed programming in high-level languages. We discuss the design space and describe an experimental language, Acute, which we have defined and implemented....

Acute: High-level programming language design for distributed computation : Design rationale and language definition (2004)

Sewell, Peter, Leifer, James J., Wansbrough, Keith, Allen-Williams, Mair, Zappa Nardelli, Francesco, Habouzit, Pierre, ...

This paper studies key issues for distributed programming in high-level languages. We discuss the design space and describe an experimental language, Acute, which we have defined and implemented....

Acute: High-level programming language design for distributed computation (2004)

Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, Viktor Vafeiadis

Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...

doi:10.1017/S0960129506005664 Transition systems, link graphs and Petri nets (2004)

James J. Leifer, Robin Milner

A framework is defined within which reactive systems can be studied formally. The framework is based on s-categories, which are a new variety of categories within which reactive systems can be set up...

Marshalling: Abstraction, Rebinding, and Version Control (2004)

James J. Leifer, Peter Sewell, Keith Wansbrough

We discuss the design of programming languages for distributed computation, focussing on support for type-safe marshalling of arbitrary language values. In particular: (1) unmarshalling can involve...

Global abstraction-safe marshalling with hash types (2003)

Leifer, James J., Peskine, Gilles, Sewell, Peter, Wansbrough, Keith

Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent...

Global abstraction-safe marshalling with hash types (2003)

Leifer, James J., Peskine, Gilles, Sewell, Peter, Wansbrough, Keith

Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent...

Global abstraction-safe marshalling with hash types (2003)

Leifer, James J., Peskine, Gilles, Sewell, Peter, Wansbrough, Keith

Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent...

Global abstraction-safe marshalling with hash types (2003)

James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough

Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent...

Global Abstraction-Safe Marshalling with Hash Types (2003)

James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough

Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent...

Global Abstraction-Safe Marshalling With Hash Types (2003)

James J. Leifer, James J. Leifer, James J. Leifer, Gilles Peskine, Gilles Peskine, Gilles Peskine, ...

Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent...

Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 1 (2002)

Leifer, James J.

The dynamics of process calculi, e.g. CCS, have often been defined using a labelled transition system (LTS). More recently it has become common when defining dynamics to use reaction rules ---i.e....

Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 (2002)

Leifer, James J.

This paper is the second in a series of two. It relies on its companion, Part 1, to motivate the central problem addressed by the series, namely: how to synthesise labelled transitions for reactive...

Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 1 (2002)

Leifer, James J.

The dynamics of process calculi, e.g. CCS, have often been defined using a labelled transition system (LTS). More recently it has become common when defining dynamics to use reaction rules ---i.e....

Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 (2002)

Leifer, James J.

This paper is the second in a series of two. It relies on its companion, Part 1, to motivate the central problem addressed by the series, namely: how to synthesise labelled transitions for reactive...

Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 1 (2002)

Leifer, James J.

The dynamics of process calculi, e.g. CCS, have often been defined using a labelled transition system (LTS). More recently it has become common when defining dynamics to use reaction rules ---i.e....

Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 (2002)

Leifer, James J.

This paper is the second in a series of two. It relies on its companion, Part 1, to motivate the central problem addressed by the series, namely: how to synthesise labelled transitions for reactive...

Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 1 (2002)

James J. Leifer, James J. Leifer, Projet Moscova

The dynamics of process calculi, e.g. CCS, have often been defined using a labelled transition system (LTS). More recently it has become common when defining dynamics to use reaction rules ---i.e....

Shallow linear action graphs and their embeddings (2000)

James J. Leifer, Robin Milner

In previous work, action calculus has been presented in terms of action graphs. Many calculi, or at least their salient features, can be expressed as specific action calculi; examples are Petri nets,...

Shallow linear action graphs and their embeddings (2000)

James J. Leifer, Robin Milner

In previous work, action calculus has been presented in terms of action graphs. Many calculi, or at least their salient features, can be expressed as specific action calculi; examples are Petri nets,...

Deriving Bisimulation Congruences for Reactive Systems (2000)

James J. Leifer, Robin Milner

. The dynamics of reactive systems, e.g. CCS, has often been de ned using a labelled transition system (LTS). More recently it has become natural in de ning dynamics to use reaction rules | i.e....

Contexts and Embeddings for Closed Shallow Action Graphs (2000)

Gian Luca Cattani, James J. Leifer, Robin Milner

: Action calculi, which have a graphical presentation, were introduced to develop a theory shared among different calculi for interactive systems. The -calculus, the -calculus, Petri nets, the...

Technical Report (1991)

Number Computer Laboratory, C Peter Sewell, Viktor Vafeiadis, Viktor Vafeiadis, Peter Sewell, Peter Sewell, ...

This paper studies key issues for distributed programming in high-level languages. We discuss the design space and describe an experimental language, Acute, which we have defined and implemented.