Group papers, by date
This lists all the group papers and theses, in reverse chronological order.
sewellandgroupbib2
Formal Mechanised Semantics of CHERI C: Capabilities,
Provenance, and Undefined Behaviour .
Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke,
Brooks Davis, Alex Richardson, David Chisnall, Brian Campbell, Ian Stark,
Robert N. M. Watson, and Peter Sewell.
In ASPLOS 2024.
[ bib |
pdf |
abstract ]
An axiomatic basis for computer programming on the relaxed
Arm-A architecture: the AxSL logic .
Angus Hammond1 , Zongyuan Liu1 , Thibaut Pérami, Peter
Sewell, Lars Birkedal, and Jean Pichon-Pharabod.
In POPL 2024, 1 These authors contributed equally. Proc. ACM
Program. Lang. 8, POPL, Article 21.
[ bib |
doi |
pdf |
abstract ]
Iris-Wasm: Robust and Modular Verification of WebAssembly
Programs .
Xiaojia Rao, Aïna Linn Georges, Maxime Legoupil, Conrad Watt,
Jean Pichon-Pharabod, Philippa Gardner, and Lars Birkedal.
Proc. ACM Program. Lang. , 7(PLDI), June 2023.
[ bib |
doi |
pdf |
http |
abstract ]
WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial
Fuzzing Oracle for WebAssembly .
Conrad Watt, Maja Trela, Peter Lammich, and Florian Märkl.
Proc. ACM Program. Lang. , 7(PLDI), June 2023.
[ bib |
doi |
pdf |
http |
abstract ]
The Cerberus C semantics .
Kayvan Memarian.
Technical Report UCAM-CL-TR-981, University of Cambridge, Computer
Laboratory, May 2023.
PhD thesis.
[ bib |
doi |
.pdf |
abstract ]
Isla: Integrating full-scale ISA semantics and axiomatic
concurrency models (extended version) .
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte,
and Peter Sewell.
Formal Methods in System Design , May 2023.
[ bib |
doi |
pdf |
http |
abstract ]
MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe
Code .
Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson,
Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco
Patrignani, Marco Vassena, and Deian Stefan.
Proc. ACM Program. Lang. , 7(POPL):425--454, January 2023.
[ bib |
doi |
pdf |
http |
abstract ]
The Arm Morello Evaluation Platform---Validating
CHERI-Based Security in a High-Performance System .
Richard Grisenthwaite, Graeme Barnes, Robert N. M. Watson, Simon W.
Moore, Peter Sewell, and Jonathan Woodruff.
IEEE Micro , 43(3):50--57, 2023.
[ bib |
doi |
http |
abstract ]
Improving Security with Hardware Support: CHERI and Arm's
Morello .
Robert N. M. Watson, Peter Sewell, and William Martin.
The Next Wave (The National Security Agency's review of emerging
technologies) , 4(1):10--21, 2023.
ISSN 2640-1789 (print), ISSN 2640-1797 (online).
[ bib |
project page |
pdf |
abstract ]
CN: Verifying systems C code with separation-logic
refinement types .
Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian,
Peter Sewell, and Neel Krishnaswami.
In POPL 2023.
[ bib |
doi |
project page |
pdf |
abstract ]
Multicore Semantics: Making Sense of Relaxed Memory (MPhil
slides) , Peter Sewell, Christopher Pulte, Shaked Flur, Mark
Batty, Luc Maranget, and Alasdair Armstrong, October 2022.
[ bib |
.pdf ]
Formal CHERI: rigorous engineering and design-time proof of
full-scale architecture security properties , Peter Sewell,
Thomas Bauereiss, Brian Campbell, and Robert N. M. Watson.
Blog post,
https://www.lightbluetouchpaper.org/2022/07/22/formal-cheri/ , July
2022.
[ bib |
project page |
http ]
Islaris: Verification of Machine Code Against Authoritative
ISA Semantics .
Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell,
Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell.
In PLDI 2022.
[ bib |
doi |
project page |
pdf |
abstract ]
N3005: A Provenance-aware Memory Object Model for C. Working
Draft Technical Specification ISO/IEC TS 6010:2023 (E) ,
Jens Gustedt, Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, and Martin
Uecker.
ISO/IEC JTC1/SC22/WG14 N3005
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n3005.pdf , June 2022.
[ bib |
pdf |
abstract ]
Verified Security for the Morello Capability-enhanced
Prototype Arm Architecture .
Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong,
Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, and Peter
Sewell.
In ESOP 2022.
[ bib |
doi |
project page |
pdf |
http |
abstract ]
Relaxed virtual memory in Armv8-A .
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher
Pulte, Richard Grisenthwaite, and Peter Sewell.
In ESOP 2022.
[ bib |
doi |
project page |
pdf |
http |
abstract ]
Relaxed virtual memory in Armv8-A (extended
version) , Ben Simner, Alasdair Armstrong, Jean
Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, and Peter Sewell,
March 2022.
http://arxiv.org/abs/2203.00642 .
[ bib |
project page |
pdf |
abstract ]
Candle: A Verified Implementation of HOL
Light .
Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell.
In ITP 2022.
[ bib |
doi |
http ]
Isolation without taxation: near-zero-cost transitions for
WebAssembly and SFI .
Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael
LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan.
Proc. ACM Program. Lang. , 6(POPL):1--30, January 2022.
[ bib |
doi |
pdf |
http |
abstract ]
VIP: Verifying Real-World C Idioms with Integer-Pointer
Casts .
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers,
Derek Dreyer, and Peter Sewell.
In POPL 2022, Proc. ACM Program. Lang. 6, POPL, Article 20.
[ bib |
doi |
supplementary material |
project page |
pdf |
abstract ]
Sail Morello (CHERI Arm) instruction-set architecture (ISA)
model , Arm Limited, Thomas Bauereiss, Brian Campbell,
Alasdair Armstrong, Alastair Reid, and Peter Sewell, 2022.
[ bib |
project page |
github ]
Bad Reasons to Reject Good Papers, and vice
versa , Peter Sewell.
SIGPLAN PL Perspectives Blog, December 2021.
Also published 2022-12-07 on the Communications of the ACM Blog
https://cacm.acm.org/blogs/blog-cacm/267440-bad-reasons-to-reject-good-papers-and-vice-versa/fulltext .
[ bib |
http ]
Verified security properties for the capability-enhanced
CHERI-MIPS architecture .
Kyndylan Nienhuis.
PhD thesis, University of Cambridge, September 2021.
[ bib |
doi |
http |
abstract ]
Verified security for the Morello capability-enhanced
prototype Arm architecture .
Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong,
Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, and Peter
Sewell.
Technical Report UCAM-CL-TR-959, University of Cambridge, Computer
Laboratory, September 2021.
[ bib |
project page |
pdf |
abstract ]
Isla: Integrating full-scale ISA semantics and axiomatic
concurrency models .
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte,
and Peter Sewell.
In CAV 2021.
[ bib |
doi |
pdf |
http |
abstract ]
N2676: A Provenance-aware Memory Object Model for C. Working
Draft Technical Specification , Jens Gustedt, Peter Sewell,
Kayvan Memarian, Victor B. F. Gomes, and Martin Uecker.
ISO/IEC JTC1/SC22/WG14 N2676
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2676.pdf , March 2021.
[ bib |
pdf |
abstract ]
Mechanising and evolving the formal semantics of WebAssembly:
the Web's new low-level language .
Conrad Watt.
PhD thesis, University of Cambridge, 2021.
EAPLS Best Dissertation Award 2021, and Honorable Mention for the
2022 ACM Doctoral Dissertation Award.
[ bib |
doi |
http |
abstract ]
Two Mechanisations of WebAssembly 1.0 .
Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and
Philippa Gardner.
In FM 2021.
[ bib |
doi |
http |
abstract ]
RefinedC: Automating the Foundational Verification of C Code
with Refined Ownership Types .
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian,
Derek Dreyer, and Deepak Garg.
In PLDI 2021.
[ bib |
pdf |
abstract ]
Underpinning the foundations: Sail-based semantics, testing,
and reasoning for production and CHERI-enabled architectures (invited
talk) .
Peter Sewell.
In CPP 2021.
[ bib |
doi |
http ]
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 |
doi |
project page |
pdf |
abstract ]
N2577: A Provenance-aware Memory Object Model for C. Working
Draft Technical Specification , Jens Gustedt, Peter Sewell,
Kayvan Memarian, Victor B. F. Gomes, and Martin Uecker.
ISO/IEC JTC1/SC22/WG14 N2577
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2577.pdf , September
2020.
[ bib |
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 ]
ARMv8-A system semantics: instruction fetch in relaxed
architectures .
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean
Pichon-Pharabod, Luc Maranget, and Peter Sewell.
In ESOP 2020.
[ bib |
project page |
errata |
pdf |
abstract ]
Repairing and mechanising the JavaScript relaxed memory
model .
Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier,
Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod, and Shu-yu Guo.
In PLDI 2020.
[ bib |
doi |
http |
abstract ]
The RISC-V Instruction Set Manual Volume I: Unprivileged
ISA.
Andrew Waterman and Krste Asanović, editors.
December 2019.
Document Version 20191213. 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, Ken
Dockser, Roger Espasa, Shaked Flur, Stefan Freudenberger, Marc Gauthier, Andy
Glew, Jan Gray, Michael Hamburg, John Hauser, David Horner, Bruce Hoult, Bill
Huffman, Alexandre Joannou, Olof Johansson, Ben Keller, David Kruckemyer,
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, Josh Scheid, 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 ]
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.
Technical Report UCAM-CL-TR-940, University of Cambridge, Computer
Laboratory, September 2019.
[ bib |
pdf |
abstract ]
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 |
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 ]
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 ]
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 ]
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 ]
REMS: Rigorous Engineering for Mainstream Systems. Summary
2013-03 -- 2019-01 , Peter Sewell, February 2019.
[ bib |
pdf |
abstract ]
Promising-ARM/RISC-V: a simpler and faster operational
concurrency model .
Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan
Lee, and Chung-Kil Hur.
In PLDI 2019.
[ bib |
doi |
pdf |
http ]
A Program Logic for First-Order Encapsulated
WebAssembly .
Conrad Watt, Petar Maksimovic, Neelakantan R. Krishnaswami, and
Philippa Gardner.
In ECOOP 2019.
[ bib |
doi |
http ]
CT-wasm: type-driven secure cryptography for the web
ecosystem .
Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian
Stefan.
Proc. ACM Program. Lang. , 3(POPL):77:1--77:29, 2019.
[ bib |
doi |
http ]
Weakening WebAssembly .
Conrad Watt, Andreas Rossberg, and Jean Pichon-Pharabod.
Proc. ACM Program. Lang. , 3(OOPSLA):133:1--133:28, 2019.
[ bib |
doi |
http ]
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 ]
Through computer architecture, darkly .
A. Theodore Markettos, Robert N. M. Watson, Simon W. Moore, Peter
Sewell, and Peter G. Neumann.
Commun. ACM , 62(6):25--27, 2019.
[ bib |
doi |
http ]
Cerberus-BMC tool for exploring the behaviour of small
concurrent C test programs with respect to an arbitrary axiomatic
concurrency model , Stella Lau, Kayvan Memarian, Victor B. F.
Gomes, Kyndylan Nienhuis, Justus Matthiesen, James Lingard, and Peter Sewell,
2019.
[web interface] .
[ bib |
project page |
github ]
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 ]
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 ]
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 ]
The Semantics of Multicopy Atomic ARMv8 and
RISC-V .
Christopher Pulte.
PhD thesis, University of Cambridge, September 2018.
[ bib |
doi |
http |
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 ]
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 ]
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 ]
Mechanising and verifying the WebAssembly
specification .
Conrad Watt.
In CPP 2018.
[ bib |
doi |
http ]
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 ]
A no-thin-air memory model for programming
languages .
Jean Yves Alexis Pichon-Pharabod.
PhD thesis, University of Cambridge, September 2017.
[ bib |
doi |
http |
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 ]
An operational semantics for C/C++11
concurrency .
Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell.
In OOPSLA 2016.
[ bib |
doi |
pdf |
http |
abstract ]
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 ]
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 ]
Not-quite-so-broken TLS 1.3 mechanised conformance
checking .
David Kaloper-Meršinjak and Hannes Mehnert.
In TRON workshop, 2016.
[ bib |
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 ]
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 ]
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 ]
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 ]
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: lessons in re-engineering a security
protocol specification and implementation, David Kaloper
Meršinjak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell, May
2015.
Presentation at HCSS 2015: the Fifteenth Annual High Confidence
Software and Systems Conference.
[ bib |
project page |
abstract ]
Cerberus: towards an Executable Semantics for Sequential and
Concurrent C11, Kayvan Memarian, Kyndylan Nienhuis, Justus
Matthiesen, James Lingard, and Peter Sewell, May 2015.
Presentation at HCSS 2015: the Fifteenth Annual High Confidence
Software and Systems Conference.
[ bib |
project page |
abstract ]
Rigorous Architectural Modelling for Production
Multiprocessors, S. Flur, K. Gray, G. Kerneis, D. Mulligan,
C. Pulte, S. Sarkar, and P. Sewell, May 2015.
Presentation at HCSS 2015: the Fifteenth Annual High Confidence
Software and Systems Conference.
[ bib |
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 ]
A Separation Logic for Fictional Sequential
Consistency .
Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, and Jean
Pichon-Pharabod.
In ESOP 2015.
[ bib |
doi |
pdf |
abstract ]
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 ]
POPL 2014 Program Chair's Report .
Peter Sewell.
SIGPLAN Notices , 49(4):10--26, July 2014.
[ bib |
doi |
pdf |
abstract ]
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 ]
Lem , Dominic Mulligan, Thomas Tuerk, Scott
Owens, Kathryn E. Gray, and Peter Sewell, 2014.
http://www.cl.cam.ac.uk/~pes20/lem/ .
[ bib |
project page |
http ]
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 ]
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 ]
Library Abstraction for C/C++ Concurrency .
Mark Batty, Mike Dodds, and Alexey Gotsman.
In POPL 2013.
[ 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 ]
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 ]
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 ]
Ott release, version 0.20.3 , Peter Sewell and
Francesco Zappa Nardelli, August 2011.
http://www.cl.cam.ac.uk/~pes20/ott/ .
[ bib |
project page |
http ]
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 ]
Responses to FoC Questions, Peter O'Hearn,
February 2011.
Briefing note for EPSRC ICT team, with contributions and input from
Anuj Dawar, Philippa Gardner, Chris Hankin, Tom Melham, Faron Moller, Andrew
Pitts, Uday Reddy, Peter Sewell, and Philip Wadler. 11pp.
[ bib ]
Fundamentals of Computing Research: a perspective from the
ground, Peter Sewell, February 2011.
Briefing note for EPSRC ICT team, with input from Anuj Dawar, Chris
Hankin, Tom Melham, Faron Moller, Peter O'Hearn, and Phil Wadler. 6pp.
[ bib ]
Lightweight Java .
Rok Strnisa and Matthew J. Parkinson.
Archive of Formal Proofs , 2011, 2011.
[ bib |
html |
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 ]
Verifying Fence Elimination Optimisations .
Viktor Vafeiadis and Francesco Zappa Nardelli.
In SAS 2011.
[ bib |
pdf |
abstract ]
ppcmem , Jade Alglave, Luc Maranget, Pankaj
Pawan, Susmit Sarkar, Peter Sewell, Derek Williams, and Francesco
Zappa Nardelli, 2011.
http://www.cl.cam.ac.uk/~pes20/ppcmem/ .
[ bib |
http ]
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 ]
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 ]
Mathematizing C++ Concurrency .
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark
Weber.
In POPL 2011.
[ bib |
doi |
pdf |
abstract ]
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 ]
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 ]
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 ]
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 ]
Ott or Nott .
Stephanie Weirich, Scott Owens, Peter Sewell, and Francesco
Zappa Nardelli.
In WMM 2010, 2pp.
[ bib |
project page |
pdf |
abstract ]
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 ]
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 ]
Formalising, improving, and reusing the Java Module
System .
Rok Strniša.
PhD thesis, University of Cambridge, 2010.
[ bib |
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 ]
Memory, an elusive abstraction .
Peter Sewell.
In ISMM 2010, Invited talk abstract.
[ bib |
doi |
pdf ]
Fences in Weak Memory Models .
Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell.
In CAV 2010.
[ bib |
doi |
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 ]
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 ]
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 ]
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 ]
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 ]
Verifying Distributed Systems: The Operational
Approach .
Thomas Ridge.
In POPL 2009.
[ bib |
doi |
project page |
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 ]
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 ]
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 ]
A better x86 memory model: x86-TSO .
Scott Owens, Susmit Sarkar, and Peter Sewell.
In TPHOLs 2009.
[ bib |
doi |
pdf |
http |
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 ]
Verifying Overlay Networks for Relocatable Computations (or:
Nomadic Pict, relocated) .
Peter Sewell and Pawel Wojciechowski.
In RRDD Workshop, 2008.
[ bib |
project page |
pdf |
abstract ]
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 ]
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 ]
Specifying real-world binding structures .
Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli.
In WMM 2007, 1pp.
[ bib |
project page |
pdf ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
Acute release , Peter Sewell, James J. Leifer,
Keith Wansbrough, Mair Allen-Williams, Francesco Zappa Nardelli, Pierre
Habouzit, and Viktor Vafeiadis, January 2005.
[ bib |
project page |
http ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
The TCP Specification: A Quick Introduction ,
Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, and Keith
Wansbrough, 2004.
[ bib |
project page |
ps |
pdf ]
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 ]
Passive Attack Analysis for Connection-Based Anonymity
Systems .
Andrei Serjantov and Peter Sewell.
In ESORICS 2003.
[ bib |
doi |
ps |
pdf |
http |
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 ]
Formalizing Dynamic Software Updating .
Gavin Bierman, Michael Hicks, Peter Sewell, and Gareth Stoyle.
In USE 2003, 17pp.
[ bib |
ps |
pdf |
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 ]
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 ]
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 ]
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 ]
Pi Calculus (Chapter 9) , Peter Sewell.
pages 177--197.
Cambridge University Press, December 2001.
ISBN 0521771846.
[ bib |
ps |
pdf |
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 ]
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: Correct Communication Infrastructure for Mobile
Computation .
Asis Unyapoth and Peter Sewell.
In POPL 2001.
[ bib |
doi |
project page |
ps |
pdf |
http |
abstract ]
Modules, Abstract Types, and Distributed
Versioning .
Peter Sewell.
In POPL 2001.
[ bib |
doi |
errata |
pdf |
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 ]
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 ]
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 ]
Secure Composition of Untrusted Code: Wrappers and Causality
Types .
Peter Sewell and Jan Vitek.
In CSFW 2000.
[ bib |
doi |
ps |
pdf |
http |
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 ]
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 ]
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 ]
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 ]
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 ]
Secure Composition of Insecure Components .
Peter Sewell and Jan Vitek.
In CSFW 1999.
[ bib |
doi |
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 ]
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 ]
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 ]
From Rewrite Rules to Bisimulation Congruences .
Peter Sewell.
In CONCUR 1998, Subsumed by the TCS 2002 paper.
[ bib |
doi |
ps |
pdf |
http |
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 ]
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 ]
Location Independence for Mobile Agents .
Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce.
In WIPL 1998, 6pp.
[ bib |
project page |
ps |
pdf ]
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 ]
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 ]
On Implementations and Semantics of a Concurrent Programming
Language .
Peter Sewell.
In CONCUR 1997.
[ bib |
doi |
ps (cmr) |
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 ]
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 ]
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 ]
Network Semantics: formal specification of TCP, UDP, and the
Sockets API , Steve Bishop, Matthew Fairbairn, Hannes Mehnert,
Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, and Keith
Wansbrough, 2001--2017.
[ bib |
project page |
github ]
The Ott tool for writing definitions of programming languages
and calculi , Peter Sewell, Francesco Zappa Nardelli, Scott
Owens, Joey Eremondi, Hannes Mehnert, Karl Palmskog, Thibaut Perami, Matthew
Parkinson, Hannes Mehnert, kit-ty kate, Brian Campbell, Francois Pottier,
Gilles Peskine, Alastair Reid, Tom Ridge, Susmit Sarkar, Rok Strniša,
and Viktor Vafeiadis, 2005--2023.
[ bib |
project page |
github ]
Linksem: Executable semantic model for aspects of ELF linking
and DWARF debug information , Dominic Mulligan, Stephen
Kell, Simon Ser, Peter Sewell, Shaked Flur, Thibaut Pérami, Robert
Norton, Ramana Kumar, Jonathan French, and Thomas Bauereiss, 2014--2023.
[ bib |
github ]
Lem, a tool for lightweight executable
mathematics , Dominic Mulligan, Thomas Bauereiss, Kathryn E.
Gray, Scott Owens, Peter Sewell, Thomas Tuerk, Basile Clement, Brian
Campbell, Christopher Pulte, David Sheets, Fabian Immler, Frederic Loulergue,
Francesco Zappa Nardelli, Gabriel Kerneis, James Lingard, Jean
Pichon-Pharabod, Justus Matthiesen, Kayvan Memarian, Kyndylan Nienhuis, Lars
Hupel, Mark Batty, Michael Greenberg, Michael Norrish, Ohad Kammar, Peter
Boehm, Robert Norton, Sami Mäkelä, Shaked Flur, Stephen Kell, Thibaut
Pérami, Thomas Bauereiss, Thomas Williams, Victor Gomes, and emersion,
2010--2023.
[ bib |
project page |
github ]
Cerberus C executable semantics and exploration
tool , Kayvan Memarian, Victor B. F. Gomes, Justus Matthiesen,
Peter Sewell, Kyndylan Nienhuis, Stella Lau, Jean Pichon-Pharabod,
Christopher Pulte, Rodolphe Lepigre, James Lingard, Thomas Sewell, and Dhruv
Makwana, 2016--2023.
[web interface] .
[ bib |
project page |
github ]
CppMem: C/C++ memory model exploration tool ,
Mark Batty, Scott Owens, Jean Pichon-Pharabod, Susmit Sarkar, and Peter
Sewell, 2012--2019.
[web interface] .
[ bib |
http ]
RMEM: Executable operational concurrency model exploration
tool for ARMv8, RISC-V, Power, and x86 , Susmit
Sarkar, Peter Sewell, Luc Maranget, Shaked Flur, Christopher Pulte, Jon
French, Ben Simner, Scott Owens, Pankaj Pawan, Francesco Zappa Nardelli, Sela
Mador-Haim, Dominic Mulligan, Ohad Kammar, Jean Pichon-Pharabod, Gabriel
Kerneis, Alasdair Armstrong, Thomas Bauereiss, and Jeehoon Kang, 2010--2023.
[web interface] .
[ bib |
github ]
Sail CHERI-RISC-V instruction-set architecture (ISA)
model , Alasdair Armstrong, Thomas Bauereiss, Brian Campbell,
Jessica Clarke, Nathaniel Wesley Filardo, Alexandre Joannou, Prashanth
Mundkur, Robert Norton-Wright, Alexander Richardson, Peter Rugg, and Peter
Sewell, 2019--2023.
[ bib |
project page |
github ]
Sail CHERI-MIPS instruction-set architecture (ISA)
model , Alasdair Armstrong, Thomas Bauereiss, Brian Campbell,
Jessica Clarke, Nathaniel Filardo, Shaked Flur, Jon French, Kathryn E. Gray,
Alexandre Joannou, Robert Norton-Wright, Christopher Pulte, Alexander
Richardson, and Peter Sewell, 2016--2021.
[ bib |
project page |
github ]
Sail RISC-V instruction-set architecture (ISA)
model , Prashanth Mundkur, Rishiyur S. Nikhil, Jon French,
Brian Campbell, Robert Norton-Wright, Alasdair Armstrong, Thomas Bauereiss,
Shaked Flur, Christopher Pulte, Peter Sewell, Alexander Richardson, Hesham
Almatary, Jessica Clarke, Nathaniel Wesley Filardo, Peter Rugg, and Scott
Johnson, 2014--2023.
[ bib |
project page |
github ]
Sail Armv9.3-A and ARMv8.5-A instruction-set architecture
(ISA) models , Thomas Bauereiss, Brian Campbell, Alasdair
Armstrong, Alastair Reid, Kathryn E. Gray, Anthony Fox, Peter Sewell, and Arm
Limited, 2019, 2022.
[ bib |
project page |
github ]
The Isla symbolic evaluation engine for Sail and
Isla-axiomatic exploration tool for axiomatic concurrency
models , Alasdair Armstrong, Brian Campbell, Thibaut
Pérami, Ben Simner, Peter Sewell, and Dhruv Makwana, 2019--2023.
[web interface] .
[ bib |
project page |
github ]
The Sail Instruction-Set Architecture (ISA) specification
language , Alasdair Armstrong, Thomas Bauereiss, Brian
Campbell, Shaked Flur, Jon French, Kathryn E. Gray, Stephen Kell, Gabriel
Kerneis, Neel Krishnaswami, Prashanth Mundkur, Robert Norton-Wright,
Christopher Pulte, Alastair Reid, Peter Sewell, Ian Stark, and Mark Wassell,
2013--2023.
[ bib |
project page |
github ]
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 ]
This file was generated by
bibtex2html 1.99.
This file was partly generated by
bibtex2html 1.96.