Dynamic rebinding for marshalling and update, (2009)
Peter Sewell, Gareth Stoyle, Michael Hicks, Gavin Bierman, Keith Wansbrough
via redex-time and destruct-time reduction
The Design of Distributed Programming Languages (2008)
Peter Sewell, John Billings, Steve Bishop, Matthew Fairbairn, Pierre Habouzit, Michael Hicks, ...
High-level programming languages For non-distributed, non-concurrent programming, they’re pretty good. We have ML (SML/OCaml), Haskell, Java, C#, with: • type safety • rich concrete types –...
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....
Peter Sewell, Mike Hicks, Gareth Stoyle, Keith Wansbrough, Gavin Bierman
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example...
Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, Viktor Vafeiadis
Acute and TCP: specifying and developing abstractions for global computation (2008)
James Leifer, Michael Norrish, Peter Sewell, Keith Wansbrough
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
The TCP/IP protocols and Sockets API underlie much of modern computation, but their semantics have historically been very complex and ill-defined. The real standard is the de facto one of the common...
Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, Viktor Vafeiadis
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
The TCP/IP protocols and Sockets API underlie much of modern computation, but their semantics have historically been very complex and ill-defined. The real standard is the de facto one of the common...
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...
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...
Engineering with Logic: HOL Specification and (2008)
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, ...
The TCP/IP protocols and Sockets API underlie much of modern computation, but their semantics have historically been very complex and ill-defined. The real standard is the de facto one of the common...
First Year Plan of Work Usage Types for Compiler Optimisation (2007)
A number of optimisations and potential optimisations in lazy functional languages relate to knowledge about the number of times a value is accessed or
PEer-toPeer Implementation and TheOry Workpackage 1: Formal Models (2007)
Peter Sewell, Keith Wansbrough, Steven Bishop, Michael Norrish, Ucam The
We discuss each in turn, concluding by listing the associated papers published during this year. 1 Transactions and the Semantics of Failure Overview Work in this task has proceeded at three levels...
Andrei Serjantov, Peter Sewell, Keith Wansbrough
Abstract. Network programming is notoriously hard to understand: one has to deal with a variety of protocols (IP, ICMP, UDP, TCP etc), concurrency, packet loss, host failure, timeouts, the complex...
Timing UDP:MechanizedSemantics forSockets,Threads, andFailures (2007)
Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov
www.cl.cam.ac.uk/users/pes20/Netsem Abstract. This paper studies the semantics of failure in distributed programming. We present a semantic model for distributed programs that use the standard...
Michael Norrish, Peter Sewell, Keith Wansbrough
is good for you and feasible: reflections on formal treatments of
Once Upon a Polymorphic Type (2007)
Keith Wansbrough, Simon Peyton Jones
We present a sound type-based `usage analysis' for a realistic lazy functional language. Accurate information on the usage of program subexpressions in a lazy functional language permits a...
A Natural Definition of Random Language (2007)
We propose a natural definition of random language, based on the standard AIT definitions of random string and random sequence. We demonstrate the equivalence of our natural definition with an...
A Methodology for Procedure Cloning (2007)
Procedure cloning is an interprocedural optimisation technique that creates duplicates or `clones ' of a procedure, each representing different sets of assumptions about the state on entry to...
www.cl.cam.ac.uk/users/kw217/ (2007)
Keith Wansbrough, Simon Peyton Jones, Cambridge Cb Nh
research.microsoft.com/Users/simonpj/ We present a sound type-based `usage analysis ' for a realistic lazy functional language. Accurate information on the usage of program subexpressions in a...
Macros and Preprocessing in Haskell (2007)
www.cl.cam.ac.uk/users/kw217/ Existing large Haskell systems make extensive use of the C preprocessor, CPP. Such use is problematic, as CPP is not designed for use with Haskell code. Certain features...
CCP
Tracing Lazy Functional Languages 07.483 Advanced Project in Computer Science 1 (2007)
The tracing of conventional imperative languages is straightforward, and tracing is probably the most common debugging technique in use today. However, attempting blindly to trace pure functional...
PEer-toPeer Implementation and TheOry Workpackage 1: Formal Models (2007)
Peter Sewell, Keith Wansbrough, Steven Bishop, Michael Norrish, Ucam The
We discuss each in turn, concluding by listing the associated papers published during this year. 1 Transactions and the Semantics of Failure Overview Work in this task has proceeded at three levels...
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...
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...
Rigorous Specification and Conformance Testing (2005)
Techniques For Network, Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, ...
Network protocols are hard to implement correctly. Despite the existence of RFCs and other standards, implementations often have subtle differences and bugs. One reason for this is that the...
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
We have developed a mathematically rigorous and experimentally-validated post-hoc specification of the behaviour of TCP, UDP, and the Sockets API. It characterises the API and network-interface...
Rigorous And Experimentally-Validated, Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, ...
We have developed a mathematically rigorous and experimentally-validated post-hoc specification of the behaviour of TCP, UDP, and the Sockets API. It characterises the API and network-interface...
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
Network protocols are hard to implement correctly. Despite the existence of RFCs and other standards, implementations often have subtle differences and bugs. One reason for this is that the...
rigorous and experimentally-validated behavioural specification Volume 1: Overview (2005)
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough, ...
rigorous and experimentally-validated behavioural specification
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
Network protocols are hard to implement correctly. Despite the existence of RFCs and other standards, implementations often have subtle differences and bugs. One reason for this is that the...
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....
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....
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...
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...
Dynamic Rebinding for Marshalling and Update, with Destruct-time λ (2004)
Gavin Bierman, Gavin Bierman, Michael Hicks, Michael Hicks, Peter Sewell, Peter Sewell, ...
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example...
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, Inria Rocquencourt, James J. Leifer, ...
apport de recherche
Dynamic rebinding for marshalling and update, with destruct-time λ (2003)
Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, Keith Wansbrough
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example...
Dynamic Rebinding for Marshalling and Update, with Destruct-time λ (2003)
Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, Keith Wansbrough
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example...
Dynamic Rebinding for Marshalling and Update, (2003)
Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, Keith Wansbrough
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example...
Required Foundations for Pear-to-Peer Systems (2003)
Peter Sewell, James Leifer, Uwe Nestmann, Andrei Serjantov, Keith Wansbrough
This report places the foundational work of PEPITO, the initial work of which was described in Deliverable D1.7 "First Progress Report on Formal Models", in the broad perspective of P2P...
Dynamic Rebinding for Marshalling and Update, with Destruct-time (2003)
Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, Keith Wansbrough
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example...
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...
Dynamic Rebinding for Marshalling and Update, (2003)
Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, Keith Wansbrough
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example...
Dynamic Rebinding for Marshalling and Update, with Destruct-time λ (2003)
Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, Keith Wansbrough
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example...
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...
Global Abstraction-Safe Marshalling with Hash Types (2003)
James Leifer Gilles, 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, Gilles Peskine, Gilles Peskine, Peter Sewell, Peter Sewell, ...
apport de recherche
Simple Polymorphic Usage Analysis (2002)
Keith Wansbrough, Clare Hall, Keith Wansbrough
Soli deo gloria
Rigour is Good for You and Feasible: (2002)
Reflections On Formal, Michael Norrish, Peter Sewell, Keith Wansbrough
Introduction We summarise two projects that formalised complex real world systems: UDP and its sockets API, and the C programming language. We describe their goals and the techniques used in both. We...
Simple Polymorphic Usage Analysis (2002)
the corresponding page number in the dissertation. Technical reports published by the University of Cambridge Computer Laboratory are freely available via the Internet:
Timing UDP: mechanized semantics for sockets, threads and failures (2002)
Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov
www.cl.cam.ac.uk/users/pes20/Netsem Abstract. This paper studies the semantics of failure in distributed programming. We present a semantic model for distributed programs that use the standard...
Rigour is good for you and feasible: reflections on formal treatments of C and UDP sockets (2002)
Michael Norrish, Peter Sewell, Keith Wansbrough
Introduction We summarise two projects that formalised complex real world systems. We describe their goals and the techniques used in both. We conclude by discussing how such techniques might be...
Timing UDP: mechanized semantics for sockets, threads and failures (2002)
Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov
This paper studies the semantics of failure in distributed programming. We present a semantic model for distributed programs that use the standard sockets interface; it covers message loss, host...
Dynamic Rebinding for Distributed Programming (2002)
Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, Keith Wansbrough
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises. Typically...
Rigorous Semantics For, Andrei Serjantov, Peter Sewell, Keith Wansbrough
Network programming is notoriously hard to understand: one has to deal with a variety of protocols (IP, ICMP, UDP, TCP etc), concurrency, packet loss, host failure, timeouts, the complex sockets...
The UDP calculus: Rigorous semantics for real networking (2001)
Andrei Serjantov, Andrei Serjantov, Peter Sewell, Peter Sewell, Keith Wansbrough, Keith Wansbrough
Abstract. Network programming is notoriously hard to understand: one has to deal with a variety of protocols (IP, ICMP, UDP, TCP etc), concurrency, packet loss, host failure, timeouts, the complex...
The UDP Calculus: Rigorous Semantics for Real Networking (2001)
Andrei Serjantov, Andrei Serjantov, Peter Sewell, Peter Sewell, Keith Wansbrough, Keith Wansbrough
Network programming is notoriously hard to understand: one has to deal with a variety of protocols (IP, ICMP, UDP, TCP etc), concurrency, packet loss, host failure, timeouts, the complex sockets...
Simple Usage Polymorphism (2000)
Keith Wansbrough, Simon Peyton Jones, Cambridge Cb Nh
We present a novel inference algorithm for a type system featuring subtyping and usage (annotation) polymorphism. This algorithm infers simply-polymorphic types rather than the...
Simple Usage Polymorphism (2000)
Keith Wansbrough, Simon Peyton Jones, Cambridge Cb Nh
We present a novel inference algorithm for a type system featuring subtyping and usage (annotation) polymorphism. This algorithm infers simply-polymorphic types rather than the...
A Novel Problem in Constraint-Based Type Inference (1999)
this document, we have simpli ed the languages. Firstly, we have omitted constructors and case, replacing them instead by the choice operator e 1 8 e 2 which nondeterministically selects one branch...
A modular monadic action semantics (1997)
Keith Wansbrough, Keith Wansbrough, John Hamer, John Hamer
The following paper was originally published in the
A modular monadic action semantics (1997)
A domain-specific language (DSL) is a framework which is designed to precisely meet the needs of a particular application. Domain-specific languages exist for a variety of reasons. As productivity...
A Modular Monadic Action Semantics (1997)
A Modular Monadic Action Semantics Masters Thesis Keith Wansbrough Department of Computer Science University of Auckland February 1997. Action semantics and modular monadic semantics are two...
A Modular Monadic Action Semantics (1997)
Keith Wansbrough For, Keith Wansbrough
A Modular Monadic Action Semantics Masters Thesis Keith Wansbrough Department of Computer Science University of Auckland February 1997. Action semantics and modular monadic semantics are two...
Tracing lazy functional languages (1996)
Jeremy Gibbons, Keith Wansbrough
We argue that Ariola and Felleisen's and Maraist, Odersky and Wadler's call-byneed lambda calculus forms a suitable formal basis for tracing evaluation in lazy functional languages.
Tracing Lazy Functional Languages (1996)
Jeremy Gibbons And, Jeremy Gibbons, Keith Wansbrough
We argue that Ariola and Felleisen's and Maraist, Odersky and Wadler's axiomatization of the callby -need lambda calculus forms a suitable formal basis for tracing evaluation in lazy...
Tracing Lazy Functional Languages (1995)
Jeremy Gibbons, Jeremy Gibbons, Keith Wansbrough, Keith Wansbrough
We argue that Ariola and Felleisen's and Maraist, Odersky and Wadler's axiomatization of the call-by-need lambda calculus forms a suitable formal basis for tracing evaluation in lazy...
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.
The UDP Calculus: Rigorous Semantics For Real Networking
Andrei Serjantov, Peter Sewell, Keith Wansbrough
Network programming is notoriously hard to understand: one has to deal with a variety of protocols (IP, ICMP, UDP, TCP etc), concurrency, packet loss, host failure, timeouts, the complex sockets...