Papers by topic

• CHERI: Capability enhanced systems (project page)
• ISA semantics and Sail (project page)
• Relaxed-memory concurrency
  • Relaxed-memory concurrency: Power, ARM, and RISC-V (rmem tool for ARM, POWER, RISC-V, and x86)
  • Relaxed-memory concurrency: C/C++11 (cppmem tool)
  • Relaxed-memory concurrency: x86
  • Relaxed-memory concurrency: the CompCert-TSO verified compiler (project page)
  • Relaxed-memory concurrency: general
• Cerberus: C semantics (project page) (Cerberus tool)
• Cerberus: ISO WG14 C standards committee papers (project page)
• LinkSem: ELF linking semantics (project page)
• SibylFS: POSIX filesystem semantics (project page)
• nqsb-TLS (project page)
• Tool support for semantics
  • Lem: tool support for semantics (project page)
  • Ott: tool support for semantics (project page)
  • The POPLmark challenge (project page)
• Netsem: semantics for TCP, UDP, and Sockets (project page)
• Type-safe distributed languages (Acute and HashCaml)
• Dynamic update
• Java modules (project page)
• Language and communication infrastructure for mobile computation: Nomadic Pict (project page)
• Security policy
• Anonymity
• Secure encapsulation
• Iota: XML scripting
• Observational concurrent language semantics
• Process calculi
  • Models for name-passing processes
  • From rewrite rules to bisimulation congruences
  • Locality typing
  • Pi calculus tutorials
  • Finite Axiomatisability
• Hardware model abstraction
• Misc
• Plasma Physics

CHERI: Capability enhanced systems (project page)

• Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8). Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, Graeme Barnes, David Chisnall, Jessica Clarke, Brooks Davis, Lee Eisen, Nathaniel Wesley Filardo, Richard Grisenthwaite, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert Norton, Alexander Richardson, Peter Rugg, Peter Sewell, Stacey Son, and Hongyan Xia. Technical Report UCAM-CL-TR-951, University of Cambridge, Computer Laboratory, October 2020. [ bib | project page | .pdf | abstract ]
• CHERI C/C++ Programming Guide. Robert N. M. Watson, Alexander Richardson, Brooks Davis, John Baldwin, David Chisnall, Jessica Clarke, Nathaniel Filardo, Simon W. Moore, Edward Napierala, Peter Sewell, and Peter G. Neumann. Technical Report UCAM-CL-TR-947, University of Cambridge, Computer Laboratory, June 2020. [ bib | project page | .pdf | abstract ]
• Cornucopia: Temporal Safety for CHERI Heaps. Nathaniel Wesley Filardo, Brett F. Gutstein, Jonathan Woodruff, Sam Ainsworth, Lucian Paul-Trifu, Brooks Davis, Hongyan Xia, Edward Tomasz Napierala, Alexander Richardson, John Baldwin, David Chisnall, Jessica Clarke, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Alfredo Mazzinghi, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, Timothy M. Jones, Simon W. Moore, Peter G. Neumann, , and Robert N. M. Watson. In Security and Privacy 2020. [ bib | DOI | project page | pdf | abstract ]
• Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony Fox, Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell. In Security and Privacy 2020. [ bib | DOI | project page | pdf | abstract ]
• An Introduction to CHERI. Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Peter Neumann. Technical Report UCAM-CL-TR-941, University of Cambridge, Computer Laboratory, September 2019. [ bib | project page | pdf | abstract ]
• Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process, Kyndylan Nienhuis, Alexandre Joannou, Anthony Fox, Michael Roe, Thomas Bauereiss, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell. Draft, August 2019. [ bib | project page | pdf | abstract ]
• Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 7). Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, David Chisnall, Brooks Davis, Nathaniel Wesley Filardo, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert Norton, Alex Richardson, Peter Rugg, Peter Sewell, Stacey Son, and Hongyan Xia. Technical Report UCAM-CL-TR-927, University of Cambridge, Computer Laboratory, June 2019. 496pp. [ bib | pdf | abstract ]
• CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment. Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G. Neumann, Simon W. Moore, John Baldwin, David Chisnall, James Clarke, Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, J. Edward Maste, Alfredo Mazzinghi, Edward Tomasz Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, and Jonathan Woodruff. In ASPLOS 2019, Best paper award. [ bib | DOI | project page | pdf | http | abstract ]
• CheriABI: Enforcing valid pointer provenance and minimizing pointer privilege in the POSIX C run-time environment. Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G. Neumann, Simon W. Moore, John Baldwin, David Chisnall, James Clarke, Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, J. Edward Maste, Alfredo Mazzinghi, Edward Tomasz Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, and Jonathan Woodruff. Technical Report UCAM-CL-TR-932, University of Cambridge, Computer Laboratory, January 2019. [ bib | project page | pdf | abstract ]
• ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS. Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 71. [ bib | DOI | supplementary material | project page | pdf | abstract ]
• Exploring C Semantics and Pointer Provenance. Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 67. Also available as ISO/IEC JTC1/SC22/WG14 N2311. [ bib | DOI | supplementary material | project page | pdf | abstract ]
• Proving security properties of CHERI-MIPS. Kyndylan Nienhuis, Alexandre Joannou, and Peter Sewell. In Automated Reasoning Workshop (ARW) 2018, Two-page abstract. [ bib | pdf | abstract ]
• Into the depths of C: elaborating the de facto standards. Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N.M. Watson, and Peter Sewell. In PLDI 2016, PLDI 2016 Distinguished Paper award. [ bib | DOI | project page | pdf | http | abstract ]

ISA semantics and Sail (project page)

• ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS. Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 71. [ bib | DOI | supplementary material | project page | pdf | abstract ]
• Formalisation of MiniSail in the Isabelle Theorem Prover. Alasdair Armstrong, Neel Krishnaswami, Peter Sewell, and Mark Wassell. In Automated Reasoning Workshop (ARW) 2018, Two-page abstract. [ bib | project page | pdf | abstract ]
• Detailed Models of Instruction Set Architectures: From Pseudocode to Formal Semantics. Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Shaked Flur, Kathryn E. Gray, Prashanth Mundkur, Robert M. Norton, Christopher Pulte, Alastair Reid, Peter Sewell, Ian Stark, and Mark Wassell. In Automated Reasoning Workshop (ARW) 2018, Two-page abstract. [ bib | project page | pdf | abstract ]
• Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. In POPL 2018. [ bib | DOI | project page | errata | pdf | abstract ]
• Mixed-size Concurrency: ARM, POWER, C/C++11, and SC. Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell. In POPL 2017. [ bib | DOI | project page | pdf | abstract ]
• Modelling the ARMv8 architecture, operationally: concurrency and ISA. Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. In POPL 2016. [ bib | DOI | project page | pdf | abstract ]
• An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors . Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar, and Peter Sewell. In MICRO 2015. [ bib | DOI | pdf | abstract ]

• ARMv8-A system semantics: instruction fetch in relaxed architectures (extended version). Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, and Peter Sewell. In ESOP 2020. [ bib | project page | pdf | abstract ]
• The RISC-V Instruction Set Manual Volume I: Unprivileged ISA. Andrew Waterman and Krste Asanović, editors. December 2018. Document Version 20181221-Public-Review-draft. Contributors: Arvind, Krste Asanović, Rimas Avižienis, Jacob Bachmeyer, Christopher F. Batten, Allen J. Baum, Alex Bradbury, Scott Beamer, Preston Briggs, Christopher Celio, Chuanhua Chang, David Chisnall, Paul Clayton, Palmer Dabbelt, Roger Espasa, Shaked Flur, Stefan Freudenberger, Jan Gray, Michael Hamburg, John Hauser, David Horner, Bruce Hoult, Alexandre Joannou, Olof Johansson, Ben Keller, Yunsup Lee, Paul Loewenstein, Daniel Lustig, Yatin Manerkar, Luc Maranget, Margaret Martonosi, Joseph Myers, Vijayanand Nagarajan, Rishiyur Nikhil, Jonas Oberhauser, Stefan O'Rear, Albert Ou, John Ousterhout, David Patterson, Christopher Pulte, Jose Renau, Colin Schmidt, Peter Sewell, Susmit Sarkar, Michael Taylor, Wesley Terpstra, Matt Thomas, Tommy Thorn, Caroline Trippel, Ray VanDeWalker, Muralidaran Vijayaraghavan, Megan Wachs, Andrew Waterman, Robert Watson, Derek Williams, Andrew Wright, Reinoud Zandijk, and Sizhuo Zhang. [ bib | pdf ]
• Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. In POPL 2018. [ bib | DOI | project page | errata | pdf | abstract ]
• Mixed-size Concurrency: ARM, POWER, C/C++11, and SC. Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell. In POPL 2017. [ bib | DOI | project page | pdf | abstract ]
• Modelling the ARMv8 architecture, operationally: concurrency and ISA. Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. In POPL 2016. [ bib | DOI | project page | pdf | abstract ]
• An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors . Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar, and Peter Sewell. In MICRO 2015. [ bib | DOI | pdf | abstract ]
• A Tutorial Introduction to the ARM and POWER Relaxed Memory Models, Luc Maranget, Susmit Sarkar, and Peter Sewell., October 2012. Draft. [ bib | pdf | abstract ]
• Fences in Weak Memory Models (Extended Version) . Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. Formal Methods in System Design, 40(2):170--205, April 2012. [ bib | DOI | pdf | abstract ]
• Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER. Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, and Peter Sewell. In POPL 2012. [ bib | DOI | project page | errata | pdf | abstract ]
• Synchronising C/C++ and POWER. Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams. In PLDI 2012. [ bib | DOI | project page | errata | pdf | abstract ]
• An Axiomatic Memory Model for POWER Multiprocessors. Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams. In CAV 2012. [ bib | DOI | pdf | abstract ]
• Litmus: running tests against hardware. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. In TACAS 2011. [ bib | DOI | pdf | http | abstract ]
• Understanding POWER Multiprocessors. Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. In PLDI 2011. [ bib | DOI | project page | pdf | abstract ]
• Fences in Weak Memory Models. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. In CAV 2010. [ bib | DOI | pdf | abstract ]
• The Semantics of Power and ARM Multiprocessor Machine Code. Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli. In DAMP 2009. [ bib | DOI | pdf | abstract ]

• An operational semantics for C/C++11 concurrency. Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell. In OOPSLA 2016. [ bib | DOI | pdf | http | abstract ]
• A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. Jean Pichon-Pharabod and Peter Sewell. In POPL 2016. [ bib | DOI | project page | pdf | abstract ]
• The Problem of Programming Language Concurrency Semantics. Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. In ESOP 2015. [ bib | DOI | pdf | abstract ]
• Mathematizing C++ Concurrency. Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. In POPL 2011. [ bib | DOI | pdf | abstract ]
• N3196: Omnibus Memory Model and Atomics Paper, P. McKenney, M. Batty, C. Nelson, H. Boehm, A. Williams, S. Owens, S. Sarkar, P. Sewell, T. Weber, M.Wong, L. Crowl, and B. Kosnik. ISO JTC1/SC22/WG21 -- The C++ Standards Committee. Working Paper, November 2010. [ bib ]
• N3125: Omnibus Memory Model and Atomics Paper, P. McKenney, M. Batty, C. Nelson, H. Boehm, A. Williams, S. Owens, S. Sarkar, P. Sewell, T. Weber, M.Wong, and L. Crowl. ISO JTC1/SC22/WG21 - The C++ Standards Committee. Working Paper, August 2010. [ bib ]
• N3132: Mathematizing C++ Concurrency: The Post-Rapperswil Model, M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. ISO JTC1/SC22/WG21 - The C++ Standards Committee. Working Paper, August 2010. [ bib ]

• The C11 and C++11 Concurrency Model. Mark John Batty. PhD thesis, University of Cambridge, 2014. 2015 SIGPLAN John C. Reynolds Doctoral Dissertation award and 2015 CPHC/BCS Distinguished Dissertation Competition winner. [ bib | pdf | abstract ]
• Library Abstraction for C/C++ Concurrency. Mark Batty, Mike Dodds, and Alexey Gotsman. In POPL 2013. [ bib | DOI | pdf | abstract ]
• Nitpicking C++ Concurrency. Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, and Susmit Sarkar. In PPDP 2011. [ bib | DOI | pdf | abstract ]
• Safe Optimisations for Shared-memory Concurrent Programs. Jaroslav Ševčík. In PLDI 2011. [ bib | DOI | pdf | abstract ]

• x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors. Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. Communications of the ACM, 53(7):89--97, July 2010. (Research Highlights). [ bib | DOI | pdf | http | abstract ]
• A better x86 memory model: x86-TSO (extended version). Scott Owens, Susmit Sarkar, and Peter Sewell. Technical Report UCAM-CL-TR-745, University of Cambridge, Computer Laboratory, March 2009. 52pp. [ bib | errata | pdf | abstract ]
• The Semantics of x86-CC Multiprocessor Machine Code. Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus Myreen, and Jade Alglave. In POPL 2009. [ bib | DOI | pdf | abstract ]
• A better x86 memory model: x86-TSO. Scott Owens, Susmit Sarkar, and Peter Sewell. In TPHOLs 2009. [ bib | DOI | pdf | http | abstract ]

• A Separation Logic for Fictional Sequential Consistency. Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, and Jean Pichon-Pharabod. In ESOP 2015. [ bib | DOI | pdf | abstract ]
• Reasoning About the Implementation of Concurrency Abstractions on x86-TSO. Scott Owens. In ECOOP 2010. [ bib | project page | pdf | abstract ]
• A Rely-guarantee Proof System for x86-TSO. Tom Ridge. In VSTTE 2010. [ bib | pdf | abstract ]

Relaxed-memory concurrency: the CompCert-TSO verified compiler (project page)

• CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. J. ACM, 60(3):22:1--22:50, June 2013. [ bib | DOI | project page | pdf | abstract ]
• CompCert-TSO release, Version 1.12, Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell, August 2011. [ bib | project page | .html ]
• Relaxed-Memory Concurrency and Verified Compilation. Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. In POPL 2011. [ bib | DOI | project page | pdf | abstract ]

• Verifying Fence Elimination Optimisations. Viktor Vafeiadis and Francesco Zappa Nardelli. In SAS 2011. [ bib | pdf | abstract ]

• Tales from the Jungle. Peter Sewell. In ICFP 2012, Invited talk abstract. [ bib | DOI | abstract ]
• False Concurrency and Strange-but-true Machines . Peter Sewell. In CONCUR 2012, Invited talk abstract. [ bib | DOI | pdf | abstract ]
• Multi-Core Memory Models and Concurrency Theory (Dagstuhl Seminar 11011). Hans-Juergen Boehm, Ursula Goltz, Holger Hermanns, and Peter Sewell. Dagstuhl Reports, 1(1):1--26, 2011. [ bib | DOI | pdf | abstract ]
• Memory, an elusive abstraction. Peter Sewell. In ISMM 2010, Invited talk abstract. [ bib | DOI | pdf ]
• Relaxed memory models must be rigorous. Francesco Zappa Nardelli, Peter Sewell, Jaroslav Ševčík, Susmit Sarkar, Scott Owens, Luc Maranget, Mark Batty, and Jade Alglave. In EC2. [ bib | pdf | abstract ]
• Multiprocessor Architectures Don't Really Exist (But They Should). Peter Sewell. In MTV 2010, Invited session on Verification issues for multi-core systems. [ bib | pdf | abstract ]

Cerberus: C semantics (project page)

• Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C. Stella Lau, Victor B. F. Gomes, Kayvan Memarian, Jean Pichon-Pharabod, and Peter Sewell. In CAV 2019. [ bib | DOI | project page | pdf | abstract ]
• Exploring C Semantics and Pointer Provenance. Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 67. Also available as ISO/IEC JTC1/SC22/WG14 N2311. [ bib | DOI | supplementary material | project page | pdf | abstract ]
• Into the depths of C: elaborating the de facto standards. Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N.M. Watson, and Peter Sewell. In PLDI 2016, PLDI 2016 Distinguished Paper award. [ bib | DOI | project page | pdf | http | abstract ]

Cerberus: ISO WG14 C standards committee papers (project page)

• P1726R0: Pointer lifetime-end zap, Paul E. McKenney, Maged Michael, Jens Mauer, Peter Sewell, Martin Uecker, Hans Boehm, Hubert Tong, and Niall Douglas. ISO/IEC JTC1/SC22/WG21 P1726R0, June 2019. [ bib | pdf ]
• N2378: C provenance semantics: slides (extracts from N2363), Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, Jens Gustedt, and Martin Uecker. ISO/IEC JTC1/SC22/WG14 N2378 v1, April 2019. [ bib | project page | pdf ]
• N2369: Pointer lifetime-end zap, Paul E. McKenney, Maged Michael, and Peter Sewell. ISO/IEC JTC1/SC22/WG14 N2369, April 2019. [ bib | project page | pdf ]
• N2364: C provenance semantics: detailed semantics (for PNVI-plain, PNVI address-exposed, PNVI address-exposed user-disambiguation, and PVI models), Peter Sewell, Kayvan Memarian, and Victor B. F. Gomes. ISO/IEC JTC1/SC22/WG14 N2364, April 2019. [ bib | project page | pdf ]
• N2363: C provenance semantics: examples, Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, Jens Gustedt, and Martin Uecker. ISO/IEC JTC1/SC22/WG14 N2363, April 2019. [ bib | project page | pdf ]
• N2362: Moving to a provenance-aware memory object model for C, Jens Gustedt, Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, and Martin Uecker. ISO/IEC JTC1/SC22/WG14 N2362 v1, March 2019. [ bib | project page | pdf ]
• Exploring C Semantics and Pointer Provenance. Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 67. Also available as ISO/IEC JTC1/SC22/WG14 N2311. [ bib | DOI | supplementary material | project page | pdf | abstract ]
• N2263: Clarifying Pointer Provenance (Q1-Q20) v4 , Kayvan Memarian, Victor Gomes, and Peter Sewell. ISO SC22 WG14 N2263, March 2018. [ bib | project page | html ]
• N2223: Clarifying the C Memory Object Model: Introduction to N2219 -- N2222, Kayvan Memarian, Victor Gomes, and Peter Sewell. ISO SC22 WG14 N2223, March 2018. [ bib | project page | html ]
• N2222: Further Pointer Issues (Q21-Q46), Kayvan Memarian, Victor Gomes, and Peter Sewell. ISO SC22 WG14 N2222, March 2018. [ bib | project page | html ]
• N2221: Clarifying Unspecified Values (Q48-Q59) v3, Kayvan Memarian, Victor Gomes, and Peter Sewell. ISO SC22 WG14 N2221, March 2018. [ bib | project page | html ]
• N2220: Clarifying Trap Representations (Q47) v3 , Kayvan Memarian, Victor Gomes, and Peter Sewell. ISO SC22 WG14 N2220, March 2018. [ bib | project page | html ]
• N2219: Clarifying Pointer Provenance (Q1-Q20) v3 , Kayvan Memarian, Victor Gomes, and Peter Sewell. ISO SC22 WG14 N2219, March 2018. [ bib | project page | html ]
• N2091: Clarifying Trap Representations, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2091, September 2016. [ bib | project page | html ]
• N2090: Clarifying Pointer Provenance, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2090, September 2016. [ bib | project page | html ]
• N2089: Clarifying Unspecified Values, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2089, September 2016. [ bib | project page | html ]
• Into the depths of C: elaborating the de facto standards. Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N.M. Watson, and Peter Sewell. In PLDI 2016, PLDI 2016 Distinguished Paper award. [ bib | DOI | project page | pdf | http | abstract ]
• N2015: What is C in practice? (Cerberus survey v2): Analysis of Responses -- with Comments, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2015, March 2016. [ bib | project page | txt ]
• N2014: What is C in practice? (Cerberus survey v2): Analysis of Responses, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2014, March 2016. [ bib | project page | html ]
• N2013: C memory object and value semantics: the space of de facto and ISO standards, David Chisnall, Justus Matthiesen, Kayvan Memarian, Kyndylan Nienhuis, Peter Sewell, and Robert N. M. Watson. ISO SC22 WG14 N2013, March 2016. [ bib | project page | pdf ]
• N2012: Clarifying the C memory object model, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2012, March 2016. [ bib | project page | html ]
• P1797R0: C/C++ Memory Object Model Papers -- Introduction, Peter Sewell. ISO/IEC JTC1/SC22/WG21 P1797R0. [ bib | html ]
• P1796R0: Effective Types: Examples, Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, Jens Gustedt, and Hubert Tong. ISO/IEC JTC1/SC22/WG21 P1796R0. [ bib | pdf ]

LinkSem: ELF linking semantics (project page)

• The missing link: explaining ELF static linking, semantically. Stephen Kell, Dominic P. Mulligan, and Peter Sewell. In OOPSLA 2016. [ bib | DOI | project page | pdf | http | abstract ]

SibylFS: POSIX filesystem semantics (project page)

• SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems. Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, and Peter Sewell. In SOSP 2015. [ bib | DOI | project page | pdf | abstract ]

nqsb-TLS (project page)

• Not-Quite-So-Broken TLS: Lessons in Re-Engineering a Security Protocol Specification and Implementation. David Kaloper-Mersinjak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell. In USENIX Security 2015. [ bib | project page | pdf | http | abstract ]

• Not-quite-so-broken TLS 1.3 mechanised conformance checking. David Kaloper-Meršinjak and Hannes Mehnert. In TRON workshop, 2016. [ bib | pdf | abstract ]

Lem: tool support for semantics (project page)

• Lem: Reusable Engineering of Real-world Semantics. Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. In ICFP 2014. [ bib | DOI | project page | pdf | abstract ]
• Lem: A Lightweight Tool for Heavyweight Semantics. Scott Owens, Peter Böhm, Francesco Zappa Nardelli, and Peter Sewell. In ITP 2011, (Rough Diamond). [ bib | DOI | project page | http ]

Ott: tool support for semantics (project page)

• Ott or Nott. Stephanie Weirich, Scott Owens, Peter Sewell, and Francesco Zappa Nardelli. In WMM 2010, 2pp. [ bib | project page | pdf | abstract ]
• Ott: Effective Tool Support for the Working Semanticist. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. Journal of Functional Programming, 20(1):70--122, January 2010. Invited submission from ICFP 2007, which was awarded the ACM SIGPLAN Most Influential ICFP 2007 Paper, in 2017. [ bib | DOI | project page | pdf | abstract ]
• Ott: Effective Tool Support for the Working Semanticist. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. In ICFP 2007, ACM SIGPLAN Most Influential ICFP Paper Award 2017 (for 2007). [ bib | DOI | project page | ps | pdf | abstract ]
• Ott release, version 0.10.9, Peter Sewell and Francesco Zappa Nardelli, August 2007. http://www.cl.cam.ac.uk/~pes20/ott/. [ bib | project page | http ]

The POPLmark challenge (project page)

• It is Time to Mechanize Programming Language Metatheory. Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, and Steve Zdancewic. In VSTTE 2005, 5pp. [ bib | DOI | project page | pdf | http | abstract ]
• Mechanized metatheory for the masses: The POPLmark Challenge. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. In TPHOLs 2005. [ bib | DOI | project page | ps | pdf | http | abstract ]

Netsem: semantics for TCP, UDP, and Sockets (project page)

• Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API. Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, and Keith Wansbrough. J. ACM, 66(1):1:1--1:77, December 2018. [ bib | DOI | project page | pdf | http | abstract ]
• TCP, UDP, and Sockets: Volume 3: The Service-level Specification. Thomas Ridge, Michael Norrish, and Peter Sewell. Technical Report UCAM-CL-TR-742, University of Cambridge, Computer Laboratory, February 2009. 305pp. [ bib | project page | pdf ]
• A rigorous approach to networking: TCP, from implementation to protocol to service. Tom Ridge, Michael Norrish, and Peter Sewell. In FM 2008. [ bib | DOI | project page | ps | pdf | http | abstract ]
• Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL. Adam Biltcliffe, Michael Dales, Sam Jansen, Thomas Ridge, and Peter Sewell. In ICNP 2006, See also the SWIFT MAC Protocol: HOL Specification at http://www.cl.cam.ac.uk/~pes20/optical/spec.pdf. [ bib | DOI | project page | ps | pdf | http | abstract ]
• Engineering with Logic: HOL Specification and Symbolic-Evaluation Testing for TCP Implementations. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough. In POPL 2006. [ bib | DOI | project page | ps | pdf | http ]
• Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough. In SIGCOMM 2005. [ bib | DOI | project page | ps | pdf | http | abstract ]
• An approximation to the real TCP state diagram, Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough, March 2005. This is a poster with a version of the "TCP state diagram" extracted from the specification. It is rather more complete than the usual diagram, but is still a very abstract and simplified view of the state space of our specification. It is intended to be printed at A1 size or bigger. [ bib | project page | ps | pdf ]
• TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification. Volume 2: The Specification.. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough. Technical Report UCAM-CL-TR-625, Computer Laboratory, University of Cambridge, March 2005. 386pp. [ bib | project page | ps | pdf | .html | abstract ]
• TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification. Volume 1: Overview. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough. Technical Report UCAM-CL-TR-624, Computer Laboratory, University of Cambridge, March 2005. 88pp. [ bib | project page | ps | pdf | .html | abstract ]
• The TCP Specification: A Quick Introduction, Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, and Keith Wansbrough, 2004. [ bib | project page | ps | pdf ]
• Rigour is good for you, and feasible: reflections on formal treatments of C and UDP sockets.. Michael Norrish, Peter Sewell, and Keith Wansbrough. In SIGOPS EW 2002. [ bib | DOI | project page | ps | pdf | http | abstract ]
• Timing UDP: mechanized semantics for sockets, threads and failures. Keith Wansbrough, Michael Norrish, Peter Sewell, and Andrei Serjantov. In ESOP 2002. [ bib | DOI | project page | ps | pdf | http | abstract ]
• The UDP Calculus: Rigorous Semantics for Real Networking. Andrei Serjantov, Peter Sewell, and Keith Wansbrough. In TACS 2001. [ bib | DOI | project page | ps | pdf | http | abstract ]
• Timing UDP: The HOL Model, Michael Norrish, Andrei Serjantov, Peter Sewell, and Keith Wansbrough, July 2001. http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html. [ bib | project page | .html ]
• The UDP Calculus: Rigorous Semantics for Real Networking. Andrei Serjantov, Peter Sewell, and Keith Wansbrough. Technical Report UCAM-CL-TR-515, Computer Laboratory, University of Cambridge, July 2001. iv+70pp. [ bib | project page | ps | pdf | .html | abstract ]

• Verifying Distributed Systems: The Operational Approach. Thomas Ridge. In POPL 2009. [ bib | DOI | project page | pdf | abstract ]

Type-safe distributed languages (Acute and HashCaml)

• Dynamic Rebinding for Marshalling and Update, via Redex-time and Destruct-time Reduction. Peter Sewell, Gareth Stoyle, Michael Hicks, Gavin Bierman, and Keith Wansbrough. Journal of Functional Programming, 18(4):437--502, 2008. [ bib | DOI | pdf | abstract ]
• Acute: High-level programming language design for distributed computation. Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, and Viktor Vafeiadis. Journal of Functional Programming, 17(4--5):547--612, July 2007. Invited submission for an ICFP 2005 special issue. [ bib | DOI | project page | ps | pdf | http | abstract ]
• Type-Safe Distributed Programming for OCaml. John Billings, Peter Sewell, Mark Shinwell, and Rok Strniša. In ML 2006. [ bib | DOI | project page | ps | pdf | http | abstract ]
• HashCaml release, version 3.09.1-alpha-795, John Billings, Peter Sewell, Mark Shinwell, and Rok Strniša, April 2006. [ bib | project page | .html ]
• Acute: High-level programming language design for distributed computation. Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, and Viktor Vafeiadis. In ICFP 2005. [ bib | DOI | project page | ps | pdf | http | abstract ]
• Source release of the Acute system, Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-Williams, Francesco Zappa Nardelli, Pierre Habouzit, and Viktor Vafeiadis, January 2005. [ bib | project page | http ]
• Acute: High-level programming language design for distributed computation. Design rationale and language definition. Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-Williams, Francesco Zappa Nardelli, Pierre Habouzit, and Viktor Vafeiadis. Technical Report UCAM-CL-TR-605, University of Cambridge Computer Laboratory, October 2004. Also published as INRIA RR-5329. 193pp. [ bib | project page | ps | pdf | .html | abstract ]
• Acute and TCP: specifying and developing abstractions for global computation. James Leifer, Michael Norrish, Peter Sewell, and Keith Wansbrough. In APPSEM II Workshop, 2004, 2pp. [ bib ]
• Dynamic Rebinding for Marshalling and Update, with Destruct-time λ. Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, and Keith Wansbrough. Technical Report UCAM-CL-TR-568, University of Cambridge Computer Laboratory, February 2004. 85pp. [ bib | ps | pdf | .html | abstract ]
• Dynamic Rebinding for Marshalling and Update, with Destruct-time lambda. Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, and Keith Wansbrough. In ICFP 2003. [ bib | DOI | ps | pdf | http | abstract ]
• Global abstraction-safe marshalling with hash types. James Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough. In ICFP 2003. [ bib | DOI | ps | pdf | http | abstract ]
• Global abstraction-safe marshalling with hash types. James Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough. Technical Report UCAM-CL-TR-569, University of Cambridge Computer Laboratory, June 2003. Also published as INRIA Rocquencourt report RR-4851. 86pp. [ bib | ps | pdf | .html | abstract ]
• Modules, Abstract Types, and Distributed Versioning. Peter Sewell. In POPL 2001. [ bib | DOI | errata | pdf | http | abstract ]
• Modules, Abstract Types, and Distributed Versioning. Peter Sewell. Technical Report UCAM-CL-TR-506, University of Cambridge, September 2000. 46pp. [ bib | errata | ps | pdf | .html | abstract ]

• Dynamic Rebinding for Marshalling and Update, via Redex-time and Destruct-time Reduction. Peter Sewell, Gareth Stoyle, Michael Hicks, Gavin Bierman, and Keith Wansbrough. Journal of Functional Programming, 18(4):437--502, 2008. [ bib | DOI | pdf | abstract ]
• Mutatis Mutandis: Safe and predictable dynamic software updating. Gareth Stoyle, Michael Hicks, Gavin Bierman, Peter Sewell, and Iulian Neamtiu. ACM Transactions on Programming Languages and Systems (TOPLAS), 29(4):70pp, August 2007. [ bib | DOI | pdf | abstract ]
• Mutatis Mutandis: Safe and Predictable Dynamic Software Updating. Gareth Stoyle, Michael Hicks, Gavin Bierman, Peter Sewell, and Iulian Neamtiu. In POPL 2005. [ bib | DOI | pdf | http | abstract ]
• Dynamic Rebinding for Marshalling and Update, with Destruct-time λ. Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, and Keith Wansbrough. Technical Report UCAM-CL-TR-568, University of Cambridge Computer Laboratory, February 2004. 85pp. [ bib | ps | pdf | .html | abstract ]
• Dynamic Rebinding for Marshalling and Update, with Destruct-time lambda. Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, and Keith Wansbrough. In ICFP 2003. [ bib | DOI | ps | pdf | http | abstract ]
• Formalizing Dynamic Software Updating. Gavin Bierman, Michael Hicks, Peter Sewell, and Gareth Stoyle. In USE 2003, 17pp. [ bib | ps | pdf | abstract ]

• Practical Dynamic Software Updating for C. Iulian Neamtiu, Michael Hicks, Gareth Stoyle, and Manuel Oriol. In PLDI 2006. [ bib | DOI | project page | pdf | abstract ]
• A Theory of Dynamic Software Updates. Gareth Paul Stoyle. PhD thesis, University of Cambridge, 2006. [ bib | pdf | abstract ]

Java modules (project page)

• The Java Module System: core design and semantic definition. Rok Strniša, Peter Sewell, and Matthew Parkinson. In OOPSLA 2007. [ bib | DOI | project page | pdf | abstract ]

• Lightweight Java. Rok Strnisa and Matthew J. Parkinson. Archive of Formal Proofs, 2011, 2011. [ bib | html | abstract ]
• Fixing the Java Module System, in Theory and in Practice. Rok Strniša. In FTfJP 2008, The informal proceedings are available as technical report ICIS-R08013 from the Radboud University, https://www-sop.inria.fr/everest/events/FTfJP08/ftfjp08.pdf. [ bib | project page | pdf | abstract ]
• Formalising, improving, and reusing the Java Module System. Rok Strniša. PhD thesis, University of Cambridge. [ bib | pdf | abstract ]

Language and communication infrastructure for mobile computation: Nomadic Pict (project page)

• Nomadic Pict: Programming Languages, Communication Infrastructure Overlays, and Semantics for Mobile Computation . Peter Sewell, Pawel Wojciechowski, and Asis Unyapoth. ACM Transactions on Programming Languages and Systems (TOPLAS), 32(4):1--63 (and electronic appendix, 33pp), 2010. [ bib | DOI | project page | pdf | abstract ]
• Verifying Overlay Networks for Relocatable Computations (or: Nomadic Pict, relocated). Peter Sewell and Pawel Wojciechowski. In RRDD Workshop, 2008. [ bib | project page | pdf | abstract ]
• Nomadic Pict: Correct Communication Infrastructure for Mobile Computation. Asis Unyapoth and Peter Sewell. In POPL 2001. [ bib | DOI | project page | ps | pdf | http | abstract ]
• Nomadic Pict: Language and Infrastructure Design for Mobile Agents. Pawel T. Wojciechowski and Peter Sewell. IEEE Concurrency, 8(2):42--52, April--June 2000. Invited submission for ASA/MA 99. [ bib | DOI | project page | http | abstract ]
• Location-Independent Communication for Mobile Agents: a Two-Level Architecture, Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce. pages 1--31. Springer-Verlag, October 1999. [ bib | DOI | project page | ps | pdf | .html | abstract ]
• Nomadic Pict: Language and Infrastructure Design for Mobile Agents. Pawel T. Wojciechowski and Peter Sewell. In ASA/MA 1999, Best paper award. [ bib | DOI | project page | ps | pdf | http | abstract ]
• Location-Independent Communication for Mobile Agents: a Two-Level Architecture. Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce. Technical Report UCAM-CL-TR-462, Computer Laboratory, University of Cambridge, April 1999. 31pp. [ bib | project page | ps | pdf | .html | abstract ]
• Location Independence for Mobile Agents. Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce. In WIPL 1998, 6pp. [ bib | project page | ps | pdf ]

• Nomadic π-calculi: Expressing and verifying communication infrastructure for mobile computation. Asis Unyapoth. PhD thesis, University of Cambridge, Computer Laboratory, June 2001. Published as UCAM-CL-TR-514. [ bib | project page | pdf | abstract ]
• Nomadic Pict: language and infrastructure design for mobile computation. Pawel Tomasz Wojciechowski. PhD thesis, University of Cambridge, Computer Laboratory, June 2000. Published as UCAM-CL-TR-492. [ bib | project page | pdf | abstract ]

• Cassandra: Flexible Trust Management, Applied to Electronic Health Records. Moritz Y. Becker and Peter Sewell. In CSFW 2004. [ bib | DOI | ps | pdf | http | abstract ]
• Cassandra: Distributed Access Control Policies with Tunable Expressiveness. Moritz Y. Becker and Peter Sewell. In POLICY 2004. [ bib | DOI | pdf | http | abstract ]

• Cassandra: flexible trust management and its application to electronic health records. Moritz Y. Becker. PhD thesis, University of Cambridge, October 2005. Published as UCAM-CL-TR-648. [ bib | pdf | abstract ]
• A formal security policy for an NHS electronic health record service. Moritz Y. Becker. Technical Report UCAM-CL-TR-628, University of Cambridge, Computer Laboratory, March 2005. [ bib | pdf | abstract ]

• Passive-attack analysis for connection-based anonymity systems. Andrei Serjantov and Peter Sewell. International Journal of Information Security, 4(3):172--180, June 2005. Special issue on ESORICS 2003. [ bib | DOI | http | abstract ]
• Passive Attack Analysis for Connection-Based Anonymity Systems. Andrei Serjantov and Peter Sewell. In ESORICS 2003. [ bib | DOI | ps | pdf | http | abstract ]

• On the anonymity of anonymity systems. Andrei Serjantov. PhD thesis, University of Cambridge, Computer Laboratory, October 2004. Published as UCAM-CL-TR-604. [ bib | pdf | abstract ]

• Secure Composition of Untrusted Code: Box-π, Wrappers and Causality Types. Peter Sewell and Jan Vitek. Journal of Computer Security, 11(2):135--188, 2003. Invited submission for a CSFW 00 special issue. [ bib | ps | pdf | http | abstract ]
• Secure Composition of Untrusted Code: Wrappers and Causality Types. Peter Sewell and Jan Vitek. In CSFW 2000. [ bib | DOI | ps | pdf | http | abstract ]
• Secure Composition of Untrusted Code: Wrappers and Causality Types. Peter Sewell and Jan Vitek. Technical Report UCAM-CL-TR-478, Computer Laboratory, University of Cambridge, November 1999. 36pp. [ bib | ps | pdf | .html | abstract ]
• Secure Composition of Insecure Components. Peter Sewell and Jan Vitek. In CSFW 1999. [ bib | DOI | ps | pdf | http | abstract ]
• Secure Composition of Insecure Components. Peter Sewell and Jan Vitek. Technical Report UCAM-CL-TR-463, Computer Laboratory, University of Cambridge, April 1999. 44pp. [ bib | ps | pdf | .html | abstract ]

• Iota: A concurrent XML scripting language with applications to Home Area Networking. G. M. Bierman and P. Sewell. Technical Report UCAM-CL-TR-557, Computer Laboratory, University of Cambridge, January 2003. 32pp. [ bib | pdf | .html | abstract ]

• On Implementations and Semantics of a Concurrent Programming Language. Peter Sewell. In CONCUR 1997. [ bib | DOI | ps (cmr) | ps | pdf | http | abstract ]

• Models for Name-Passing Processes: Interleaving and Causal. Gian Luca Cattani and Peter Sewell. Information and Computation, 190(2):136--178, May 2004. [ bib | DOI | http | abstract ]
• Models for Name-Passing Processes: Interleaving and Causal. Gian Luca Cattani and Peter Sewell. Technical Report UCAM-CL-TR-505, Computer Laboratory, University of Cambridge, September 2000. 42pp. [ bib | ps | pdf | .html | abstract ]
• Models for Name-Passing Processes: Interleaving and Causal (Extended Abstract). Gian Luca Cattani and Peter Sewell. In LICS 2000. [ bib | DOI | ps | pdf | http | abstract ]

• From Rewrite Rules to Bisimulation Congruences. Peter Sewell. Theoretical Computer Science, 274(1--2):183--230, March 2002. Invited submission for a CONCUR 98 special issue. [ bib | DOI | ps | pdf | http | abstract ]
• From Rewrite Rules to Bisimulation Congruences. Peter Sewell. In CONCUR 1998, Subsumed by the TCS 2002 paper. [ bib | DOI | ps | pdf | http | abstract ]
• From Rewrite Rules to Bisimulation Congruences. Peter Sewell. Technical Report UCAM-CL-TR-444, University of Cambridge, June 1998. 72pp. [ bib | ps (cmr) | ps | pdf | .html | abstract ]

• Global/Local Subtyping and Capability Inference for a Distributed π-calculus. Peter Sewell. In ICALP 1998, (The link is to an extended version). [ bib | DOI | ps | pdf | http | abstract ]
• Global/Local Subtyping for a Distributed π-calculus. Peter Sewell. Technical Report UCAM-CL-TR-435, Computer Laboratory, University of Cambridge, August 1997. 57pp. [ bib | ps (cmr) | ps | pdf | .html | abstract ]

• Pi Calculus (Chapter 9), Peter Sewell. pages 177--197. Cambridge University Press, December 2001. ISBN 0521771846. [ bib | ps | pdf | abstract ]
• Applied π -- A Brief Tutorial. Peter Sewell. Technical Report UCAM-CL-TR-498, Computer Laboratory, University of Cambridge, August 2000. 65pp. [ bib | ps | pdf | .html | abstract ]
• A Brief Introduction to Applied π, Peter Sewell, January 1999. Lecture notes for the Mathfit Instructional Meeting on Recent Advances in Semantics and Types for Concurrency: Theory and Practice, July 1998. [ bib | .html ]

• Nonaxiomatisability of Equivalences over Finite State Processes. Peter Sewell. Annals of Pure and Applied Logic, 90:163--191, December 1997. Invited submission from LICS '94. [ bib | DOI | ps | pdf | http | abstract ]
• The Algebra of Finite State Processes. Peter Michael Sewell. PhD thesis, University of Edinburgh, October 1995. Dept. of Computer Science technical report CST-118-95, also published as LFCS-95-328. [ bib | ps (cmr) | ps | pdf | abstract ]
• Bisimulation is Not Finitely (First-Order) Equationally Axiomatisable. Peter M. Sewell. In LICS 1994, Subsumed by the APAL 1997 paper. [ bib | DOI | ps | pdf | http | abstract ]

• Design Rules and Abstractions (from branching and real time). Peter Sewell. In DCC96, ISBN 3--540--76102--0 (The link is to an extended version). [ bib | ps | pdf | abstract ]

• POPL 2014 Program Chair's Report. Peter Sewell. SIGPLAN Notices, 49(4):10--26, July 2014. [ bib | DOI | pdf | abstract ]
• Principles of POPL. Derek Dreyer, John Field, Roberto Giacobazzi, Michael Hicks, Suresh Jagannathan, Mooly Sagiv, Peter Sewell, and Phil Wadler. SIGPLAN Notices, 48(4S):12--16, July 2013. [ bib | DOI ]
• Robin Milner 1934--2010: verification, languages, and concurrency. Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, and Peter Sewell. In POPL 2011. [ bib | DOI ]
• Process Calculi: The End of the Beginning? (From Thought Experiments to Experimental Semantics). Peter Sewell. Electr. Notes Theor. Comput. Sci., 162:317--321, 2006. [ bib | DOI | http | abstract ]
• Applied Semantics: Specifying and Developing Abstractions for Distributed Computation (Grand Challenge Discussion Paper -- GC2, GC4, and GC6), Peter Sewell and Keith Wansbrough. Position paper for Grand Challenge meeting (Newcastle). 5pp, 2004. [ bib | pdf ]

• The Determination of Sheath Potential from Retarding Field Analyser Measurements in Tokamak Edge Plasmas. G. F. Matthews, G. M. McCracken, P. M. Sewell, M. E. Woods, and B. J. Hopkins. J. Nucl. Mater., 145--147:225--230, February 1987. [ bib | http | abstract ]
• The Optimisation of Limiter Geometry to Reduce Impurity Influx in Tokamaks. G. F. Matthews, G. M. McCracken, P. C. Stangeby, C. S. Pitcher, P. M. Sewell, and D. H. J. Goodall. Plasma Physics and Controlled Fusion, 29(2):189--203, February 1987. [ bib | http | abstract ]
• Investigation of the Wake Due to a Large Probe, using a Spatially Scanning Langmuir Probe. G. F. Matthews, P. C. Stangeby, and P. M. Sewell. J. Nucl. Mater., 145--147:220--224, February 1987. [ bib | http | abstract ]
• An Investigation of the Secondary-Electron Emission of Carbon Samples Exposed to a Hydrogen Plasma. M. E. Woods, B. J. Hopkins, G. F. Matthews, G. M. McCracken, P. M. Sewell, and H. Fahrang. J. Physics D: Applied Physics, 20:1136--1142, 1987. [ bib | http | abstract ]

This file was partly generated by bibtex2html 1.96.