Peter Sewell, Nardelli Scott, Owens Gilles Peskine, Thomas Ridge, Susmit Sarkar
It is rare to give a semantic definition of a full-scale programming language, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics —...
ISSN 1476-2986TCP, UDP, and Sockets: Volume 3: The Service-level Specification (2009)
Thomas Ridge, Michael Norrish, Peter Sewell, Thomas Ridge, Michael Norrish, Peter Sewell
Despite more than 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code. In part...
Peter Sewell, Pawe̷l T. Wojciechowski, Asis Unyapoth
Mobile computation, in which executing computations can move from one physical computing device to another, is a recurring theme: from OS process migration, to language-level mobility, to virtual...
TCP, UDP, and Sockets: Volume 3: The Service-level Specification (2009)
Thomas Ridge, Michael Norrish, Peter Sewell
Despite more than 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code. In part...
A rigorous approach to networking: TCP, from implementation to protocol to service (2009)
Tom Ridge, Michael Norrish, Peter Sewell
Abstract. Despite more then 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code....
The Semantics of Power and ARM Multiprocessor Machine Code (2009)
Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell
We develop a rigorous semantics for Power and ARM multiprocessor programs, including their relaxed memory model and the behaviour of reasonable fragments of their instruction sets. The semantics is...
Specifying real-world binding structures (2009)
Representing binding structures is a central challenge in mechanizing the theory of programming languages. Two facets of the problem should be distinguished: on the one hand, one needs a...
The Semantics of Power and ARM Multiprocessor Machine Code (2009)
Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell
We develop a rigorous semantics for Power and ARM multiprocessor programs, including their relaxed memory model and the behaviour of reasonable fragments of their instruction sets. The semantics is...
Specifying real-world binding structures (2009)
Susmit Sarkar, Peter Sewell, Gamma Tdom
Representing binding structures is a central challenge in mech-anizing the theory of programming languages. Two facets of the problem should be distinguished: on the one hand, one needs...
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 objectives of the project were, briefly: (1) To study and design a foundational calculus and prototype programming language, based on the π-calculus, for describing and analysing migratory...
Abstract DRAFT – 2007-04-06 21:31 Ott: Effective Tool Support for the Working Semanticist (2008)
Peter Sewell, Nardelli Scott, Owens Gilles Peskine
It is rare to give a semantic definition of a full-scale programming language, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics —...
Abstract Ott: Effective Tool Support for the Working Semanticist (2008)
Peter Sewell, Nardelli Scott, Owens Gilles Peskine
It is rare to give a semantic definition of a full-scale programming language, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics —...
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...
Specifying real-world binding structures (2008)
Representing binding structures is a central challenge in mechanizing the theory of programming languages. Two facets of the problem should be distinguished: on the one hand, one needs a...
A rigorous approach to networking: TCP (2008)
Tom Ridge, Michael Norrish, Peter Sewell
from implementation to protocol to service
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...
A rigorous approach to networking: TCP, from implementation to protocol to service (2008)
Tom Ridge, Michael Norrish, Peter Sewell
Abstract. Despite more then 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code....
Software systems are becoming heterogeneous: instead of a small number of large programs from well-established sources, a user’s desktop may now consist of many smaller components that interact in...
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
A rigorous approach to networking: TCP, from implementation to protocol to service (2008)
Tom Ridge, Michael Norrish, Peter Sewell
Abstract. Despite more then 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code....
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 Ott: Effective Tool Support for the Working Semanticist (2008)
Peter Sewell, Nardelli Scott, Owens Gilles Peskine
It is rare to give a semantic definition of a full-scale programming language, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics —...
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...
A rigorous approach to networking: TCP (2008)
Tom Ridge, Michael Norrish, Peter Sewell
from implementation to protocol to service
It is Time to Mechanize Programming Language Metatheory (2008)
Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic
How close are we to a world in which mechanically verified software is commonplace? A world in which theorem proving technology is used routinely by both software developers and programming language...
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...
Ott: Tool Support for Semantics User Guide version 0.10.14 (2008)
Peter Sewell, Scott Owens, Matthew Parkinson, Gilles Peskine, Tom Ridge, Susmit Sarkar
Modal Types for Mobile Code (2008)
Tom Murphy Vii, Frank Pfenning, Peter Sewell
In this dissertation I argue that modal type systems provide an elegant and practical means for controlling local resources in spatially distributed computer programs. A distributed program is one...
The Semantics of x86 Multiprocessor Machine Code Supplementary Examples (2008)
Susmit Sarkar, Peter Sewell, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, ...
This note contains supplementary details for the paper The Semantics of x86 Multiprocessor Machine Code [SSZN + 09], with an informal-mathematics presentation of the axiomatic memory model, and...
Software systems are becoming heterogeneous: instead of a small number of large programs from well-established sources, a user's desktop may now consist of many smaller components that interact...
Global/Local Subtyping for a Distributed π-calculus (2007)
In the design of mobile agent programming languages there is a tension between the implementation cost and the expressiveness of the communication mechanisms provided. This paper gives a static type...
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...
In the design of mobile agent programming languages there is a tension between the implementation cost and the expressiveness of the communication mechanisms provided. This paper gives a static type...
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
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...
Ucl Louvain, Christian Schulte, Peter Sewell
Project funded by the European Community under the
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...
Mutatis Mutandis: safe and predictable dynamic software updating (2007)
Bierman, Gavin, Neamtiu, Iulian, Hicks, Michael, Sewell, Peter, Stoyle, Gareth
http://portal.acm.org/ft_gateway.cfm?id=1255455&type=pdf&coll=portal&dl=ACM&CFID=381409&CFTOKEN=93597745This article presents Proteus, a core calculus that models dynamic software updating, a service...
R.: Ott: Effective tool support for the working semanticist (2007)
Peter Sewell, Nardelli Scott, Owens Gilles Peskine, Thomas Ridge, Susmit Sarkar
Abstract It is rare to give a semantic definition of a full-scale programminglanguage, despite the many potential benefits. Partly this is because the available metalanguages for expressing...
Modal Types for Mobile Code (draft) (2007)
Tom Murphy Vii, Frank Pfenning, Peter Sewell
compilers, types In this dissertation I argue that modal type systems provide an elegant and practical means for controlling local resources in spatially distributed computer programs. A distributed...
R.: Ott: Effective tool support for the working semanticist (2007)
Peter Sewell, Nardelli Scott, Owens Gilles Peskine, Thomas Ridge, Susmit Sarkar
Abstract It is rare to give a semantic definition of a full-scale programminglanguage, despite the many potential benefits. Partly this is because the available metalanguages for expressing...
Rigorous protocol design in practice: An optical packet-switch MAC (2006)
Adam Biltcliffe, Michael Dales, Sam Jansen, Thomas Ridge, Peter Sewell
Abstract-- This paper reports on an experiment in networkprotocol design: we use novel rigorous techniques in the design process of a new protocol, in a close collaboration betweensystems and theory...
Rigorous protocol design in practice: An optical packet-switch MAC (2006)
Adam Biltcliffe, Michael Dales, Sam Jansen, Thomas Ridge, Peter Sewell
Abstract — This paper reports on an experiment in network protocol design: we use novel rigorous techniques in the design process of a new protocol, in a close collaboration between systems and...
Rigorous Protocol Design in Practice: An Optical (2006)
Adam Biltcliffe, Michael Dales, Sam Jansen, Thomas Ridge, Peter Sewell
This paper reports on an experiment in network protocol design: we use novel rigorous techniques in the design process of a new protocol, in a close collaboration between systems and theory...
Type-Safe Distributed Programming for OCaml (2006)
John Billings Peter, Peter Sewell, Mark Shinwell
Existing ML-like languages guarantee type-safety, ensuring memory safety and protecting the invariants of abstract types, but only within single executions of single programs. Distributed programming...
Type-safe distributed programming for OCaml (2006)
John Billings, Peter Sewell, Mark Shinwell
Existing ML-like languages guarantee type-safety, ensuring memory safety and protecting the invariants of abstract types, but only within single executions of single programs. Distributed programming...
Rigorous protocol design in practice: An optical packet-switch MAC (2006)
Adam Biltcliffe, Michael Dales, Sam Jansen, Thomas Ridge, Peter Sewell
Abstract — This paper reports on an experiment in network protocol design: we use novel rigorous techniques in the design process of a new protocol, in a close collaboration between systems and...
Rigorous protocol design in practice: An optical packet-switch MAC (2006)
Adam Biltcliffe, Michael Dales, Sam Jansen, Thomas Ridge, Peter Sewell
Abstract-- This paper reports on an experiment in networkprotocol design: we use novel rigorous techniques in the design process of a new protocol, in a close collaboration betweensystems and theory...
Type-safe distributed programming for OCaml (2006)
John Billings, Peter Sewell, Mark Shinwell
Existing ML-like languages guarantee type-safety, ensuring memory safety and protecting the invariants of abstract types, but only within single executions of single programs. Distributed programming...
Mechanized Metatheory for the Masses: The POPLMARK Challenge (2005)
Aydemir, Brian E, Bohannon, Aaron, Fairbairn, Matthew, Foster, J. Nathan, Pierce, Benjamin C, Sewell, Peter, ...
How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machinechecked proofs? We propose an initial set of benchmarks for measuring...
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...
Mechanized metatheory for the masses: The POPLmark Challenge (2005)
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, ...
Abstract. How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machinechecked proofs? We propose a concrete set of benchmarks for...
Mutatis Mutandis: Safe and predictable dynamic software updating (2005)
Gareth Stoyle, Michael Hicks, Gavin Bierman, Peter Sewell
This article presents Proteus, a core calculus that models dynamic software updating, a service for fixing bugs and adding features to a running program. Proteus permits a program’s type structure...
Mutatis Mutandis: Safe and predictable dynamic software updating (2005)
Gareth Stoyle, Michael Hicks, Gavin Bierman, Peter Sewell
This paper presents Proteus, a core calculus that models dynamic software updating, a service for fixing bugs and adding features to a running program. Proteus permits a program’s type structure to...
Mechanized Metatheory for the Masses: The PoplMark Challenge (2005)
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, ...
How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs? We propose a concrete set of benchmarks for measuring...
Mechanized Metatheory for the Masses: The PoplMark Challenge (2005)
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, ...
How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machinechecked proofs? We propose an initial set of benchmarks for measuring...
Safe And Predictable, Gareth Stoyle, Michael Hicks, Gavin Bierman, Peter Sewell, Iulian Neamtiu
Dynamic software updates can be used to fix bugs or add features to a running program without downtime. Essential for some applications and convenient for others, low-level dynamic updating has been...
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...
Mechanized metatheory for the masses: The POPLmark Challenge (2005)
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, ...
Abstract. How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machinechecked proofs? We propose an initial set of benchmarks for...
Mechanized metatheory for the masses: The POPLmark Challenge (2005)
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, ...
Abstract. How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machinechecked proofs? We propose an initial set of benchmarks for...
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
Mechanized metatheory for the masses: The POPLmark Challenge (2005)
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, ...
Abstract. How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machinechecked proofs? We propose an initial set of benchmarks for...
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...
Cassandra: Flexible Trust Management, Applied to Electronic Health Records (2004)
Moritz Y. Becker, Peter Sewell
We study the specification of access control policy in large-scale distributed systems. We present Cassandra, a language and system for expressing policy, and the results of a substantial case study,...
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...
Passive Attack Analysis for Connection-Based Anonymity Systems (2003)
Andrei Serjantov, Peter Sewell
In this paper we consider low latency connection-based anonymity system which can be used for applications like web browsing or SSH. Although several such systems have been designed and built, their...
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...
Formalizing Dynamic Software Updating (2003)
Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle
Dynamic software updating (DSU) enables running programs to be updated with new code and data without interrupting their execution. A number of DSU systems have been designed, but there is still...
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
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...
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...
Secure Composition of Untrusted Code: Box π, Wrappers, and Causality Types (2002)
Software systems are becoming heterogeneous: instead of a small number of large programs from well-established sources, a user's desktop may now consist of many smaller components that interact...
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...
Software systems are becoming heterogeneous: instead of a small number of large programs from well-established sources, a user’s desktop may now consist of many smaller components that interact in...
Nomadic Pict: Correct communication infrastructure for mobile computation (2001)
This paper addresses the design and verication of infrastructure for mobile computation. In particular, we study language primitives for communication between mobile agents. They can be classied into...
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...
Dynamic software updating (2001)
Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle
Dynamic software updating (DSU) enables running programs to be updated with new code and data without interrupting their execution. A number of DSU systems have been designed, but there is still...
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...
Dynamic software updating (2001)
Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle
Dynamic software updating (DSU) enables running programs to be updated with new code and data without interrupting their execution. A number of DSU systems have been designed, but there is still...
Dynamic software updating (2001)
Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle
Dynamic software updating (DSU) enables running programs to be updated with new code and data without interrupting their execution. A number of DSU systems have been designed, but there is still...
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...
Secure composition of untrusted code: Wrappers and causality types (2000)
We consider the problem of assembling concurrent software systems from untrusted or partially trusted o-the-shelf components, using wrapper programs to encapsulate components and enforce security...
Nomadic Pict: Language and infrastructure design for mobile agents (2000)
Pawe T. Wojciechowski, Peter Sewell
We study the distributed infrastructures required for location-independent communication between migrating agents. These infrastructures are problematic: different applications may have very dierent...
Models for name-passing processes: interleaving and causal (2000)
Gian Luca Cattani, Peter Sewell
We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual -calculus...
Applied π - A Brief Tutorial (2000)
This note provides a brief introduction to pi-calculi and their application to concurrent and distributed programming. Chapter 1 introduces a simple pi-calculus and discusses the choice of...
Secure Composition of Untrusted Code: Wrappers and Causality Types (2000)
We consider the problem of assembling concurrent software systems from untrusted or partially trusted off-the-shelf components, using wrapper programs to encapsulate components and enforce security...
Applied π - A Brief Tutorial (2000)
This note provides a brief introduction to -calculi and their application to concurrent and distributed programming. Chapter 1 introduces a simple -calculus and discusses the choice of primitives,...
Models for Name-Passing Processes: Interleaving and Causal (Extended Abstract) (2000)
Gian Luca Cattani, Peter Sewell
We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual...
Models for name-passing processes: interleaving and causal (2000)
Gian Luca Cattani, Peter Sewell
We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual π-calculus...
This note provides a brief introduction to π-calculi and their application to concurrent and distributed programming. Chapter 1 introduces a simple π-calculus and discusses the choice of...
Modules, Abstract Types, and Distributed (2000)
In a wide-area distributed system it is often impractical to synchronise software updates, so one must deal with many coexisting versions. We study static typing support for modular wide-area...
Location-independent communication for mobile agents: a two-level architecture (1999)
Peter Sewell, Benjamin C. Pierce
Abstract. We study communication primitives for interaction between mobile agents. They can be classied into two groups. At a low level there are location dependent primitives that require a...
Secure composition of insecure components (1999)
Software systems are becoming heterogeneous: instead of a small number of large programs from well-established sources, a user’s desktop may now consist of many smaller components that interact in...
Nomadic Pict: Language and Infrastructure Design for Mobile Agents (1999)
Pawel T. Wojciechowski, Peter Sewell
We study the distributed infrastructures required for location-independent communication between migrating agents. These infrastructures are problematic: different applications may have very...
From Rewrite Rules to Bisimulation Congruences (1999)
The dynamics of many calculi can be most clearly de ned by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be...
Secure Composition of Insecure Components (1999)
Software systems are becoming heterogeneous: instead of a small number of large programs from well-established sources, a user's desktop may now consist of many smaller components that interact...
Secure Composition of Untrusted Code: Wrappers and Causality Types (1999)
We consider the problem of assembling concurrent software systems from untrusted or partially trusted components. In previous work we studied wrapper programs that can encapsulate untrusted...
Secure Composition of Untrusted Code: Wrappers and Causality Types (1999)
We consider the problem of assembling concurrent software systems from untrusted or partially trusted off-the-shelf components, using wrapper programs to encapsulate components and enforce security...
Secure Composition of Insecure Components (1999)
Software systems are becoming heterogeneous: instead of a small number of large programs from well-established sources, a user's desktop may now consist of many smaller components that interact...
From rewrite rules to bisimulation congruences (1998)
The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be...
From rewrite rules to bisimulation congruences (1998)
The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be...
Location Independence for Mobile Agents (1998)
Peter Sewell Pawe, Peter Sewell, Pawe/l T. Wojciechowski, Benjamin C. Pierce
this paper we study the first of these, considering the design, semantic definition and implementation
From Rewrite Rules to Bisimulation Congruences (1998)
The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be...
Location-Independent Communication for Mobile Agents: a Two-Level Architecture (1998)
Peter Sewell Pawe, Peter Sewell, Benjamin C. Pierce
. We study communication primitives for interaction between mobile agents. They can be classied into two groups. At a low level there are location dependent primitives that require a programmer to...
Location-Independent Communication for Mobile Agents: a Two-Level Architecture (1998)
Peter Sewell, Pawel T. Wojciechowski, Benjamin C. Pierce
We study communication primitives for interaction between mobile agents. They can be classified into two groups. At a low level there are location dependent primitives that require a programmer to...
Location Independence for Mobile Agents (1998)
Peter Sewell, Pawe/l T. Wojciechowski, Benjamin C. Pierce
this paper we study the first of these, considering the design, semantic definition and implementation of communication primitives by which mobile agents can interact. Communication primitives can be...
From Rewrite Rules to Bisimulation Congruences (1998)
The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be...
Global/local subtyping and capability inference for a distributed π-calculus (1998)
This paper considers how locality restrictions on the use of capabilities can be enforced by a static type system. A distributed π-calculus with a simple reduction semantics is introduced,...
Location Independence for Mobile Agents (1998)
Peter Sewell, Pawe/l T. Wojciechowski, Benjamin C. Pierce
this paper we study the first of these, considering the design, semantic definition and implementation of communication primitives by which mobile agents can interact. Communication primitives can be...
Foundations of Distributed Programming Languages (1998)
Machine M ß-LTS testing C C behaviour (idealised) SOS C-behaviour \Gamma l ` P print!"Hello" \Gamma! P 0 C printh"Hello";ffli \Gamma! C 0 SOS C-behaviour \Gamma l ` P 6 \Gamma!...
On Implementations and Semantics of a Concurrent Programming Language Peter Sewell (1997)
The concurrency theory literature contains many proposals for models of process algebras. We consider an example application of the ß-calculus, the programming language Pict of Pierce and Turner,...
On Implementations and Semantics of a Concurrent Programming Language (1997)
The concurrency theory literature contains many proposals for models of process algebras. We consider an example application of the ß-calculus, the programming language Pict of Pierce and Turner,...
Design Rules and Abstractions (from branching and real time) (1996)
ions (from branching and real time) DRAFT Peter Sewell The Computer Laboratory, University of Cambridge Cambridge CB2 3QG, UK Peter.Sewell@cl.cam.ac.uk September 5, 1996 Abstract Three simple models...
Bisimulation is not Finitely (First Order) Equationally Axiomatisable (1994)
This paper considers the existence of finite equational axiomatisations of bisimulation over a calculus of finite state processes. To express even simple properties such as ¯XE = ¯XE[E=X]...
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...