Author name cluster

Alan Jeffrey

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

2 author rows

CSL Conference 2011 Conference Paper

The Lax Braided Structure of Streaming I/O

Alan Jeffrey
Julian Rathke

We investigate and implement a model of typed streaming I/O. Each type determines a language of traces analogous to regular expressions on strings, and programs are modelled by certain monotone functions on these traces. We show that sequential composition forms a lax braided monoid in the category of types and programs. This lax braided structure allows programs to be represented diagrammatically using Joyal and Street's string diagrams in 3D space. Monotone functions over traces cannot be executed efficiently, so we present an equivalent monoidal category of transducers. We demonstrate that transducers can be executed efficiently, theoretically by showing that programs with diagrams embedded in the plane can be executed in O(1) space, and experimentally by an implementation in the Agda dependently typed functional language. Agda supports machine-assisted proof: we have mechanically verified that the transducer implementation and the I/O model form lax braided monoidal categories.

Details

TCS Journal 2008 Journal Article

Full abstraction for polymorphic π -calculus

Alan Jeffrey
Julian Rathke

The problem of finding a fully abstract model for the polymorphic π -calculus was stated in Pierce and Sangiorgi’s work in 1997 and has remained open since then. In this paper, we show that a variant of their language has a fully abstract model, which does not depend on type unification or logical relations. This is the first fully abstract model for a polymorphic concurrent language. In addition, we discuss the relationship between our work and Pierce and Sangiorgi’s, and show that their model based on type unification is sound but not complete.

Details DOI

I&C Journal 2006 Journal Article

Pattern-matching spi-calculus

Christian Haack
Alan Jeffrey

Cryptographic protocols often make use of nested cryptographic primitives, for example signed message digests, or encrypted signed messages. Gordon and Jeffrey’s prior work on types for authenticity did not allow for such nested cryptography. In this work, we present the pattern-matching spi-calculus, which is an obvious extension of the spi-calculus to include pattern-matching as primitive. The novelty of the language is in the accompanying type system, which uses the same language of patterns to describe complex data dependencies which cannot be described using prior type systems. We show that any appropriately typed process is guaranteed to satisfy robust authenticity, secrecy and integrity properties.

Details DOI

TCS Journal 2005 Journal Article

A fully abstract may testing semantics for concurrent objects

Alan Jeffrey
Julian Rathke

This paper provides a fully abstract semantics for a variant of the concurrent object calculus. We define may testing for concurrent object components and then characterise it using a trace semantics inspired by UML interaction diagrams. The main result of this paper is to show that the trace semantics is fully abstract for may testing. This is the first such result for a concurrent object language.

Details DOI

TCS Journal 2004 Journal Article

A theory of bisimulation for a fragment of concurrent ML with local names

Alan Jeffrey
Julian Rathke

Concurrent ML is an extension of Standard ML with π-calculus-like primitives for multi-threaded programming. CML has a reduction semantics, but to date there has been no labelled transition system semantics provided for the entire language. In this paper, we present a labelled transition semantics for a fragment of CML called μνCML which includes features not covered before: dynamically generated local channels and thread identifiers. We show that weak bisimilarity for μνCML is a congruence, and coincides with barbed bisimulation congruence. We also provide a variant of Sangiorgi's normal bisimulation for μνCML, and show that this too coincides with bisimilarity.

Details DOI

TCS Journal 2003 Journal Article

Typing correspondence assertions for communication protocols

Andrew D Gordon
Alan Jeffrey

Woo and Lam propose correspondence assertions for specifying authenticity properties of security protocols. Prior work on checking correspondence assertions depends on model-checking and is limited to finite-state systems. We propose a dependent type and effect system for checking correspondence assertions. Since it is based on type-checking, our method is not limited to finite-state systems. This paper presents our system in the simple and general setting of the π-calculus. We show how to type-check correctness properties of example communication protocols based on secure channels. In a related paper, we extend our system to the more complex and specific setting of checking cryptographic protocols based on encrypted messages sent over insecure channels.

Details DOI

TCS Journal 1999 Journal Article

A fully abstract semantics for a higher-order functional language with nondeterministic computation

Alan Jeffrey

This paper presents a functional programming language, based on Moggi’s monadic metalanguage. In the first part of this paper, we show how the language can be regarded as a monad on a category of signatures, and that the resulting category of algebras is equivalent to the category of computationally cartesian closed categories. In the second part, we extend the language to include a nondeterministic operational semantics, and show that the lower powerdomain semantics is fully abstract for may-testing.

Details DOI

TCS Journal 1995 Journal Article

A complete axiomatization of timed bisimulation for a class of timed regular behaviours

Luca Aceto
Alan Jeffrey

One of the most satisfactory results in process theory is Milner's axiomatization of strong bisimulation for regular CCS. This result holds for open terms with finite-state recursion. Wang has shown that timed bisimulation can also be axiomatized, but only for closed terms without recursion. In this paper, we provide an axiomatization for timed bisimulation of open terms with finite-state recursion.

Details DOI