BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × China
1 × Estonia
1 × Finland
2 × Canada
2 × Denmark
2 × France
2 × Germany
2 × Sweden
3 × United Kingdom
9 × USA
Collaborated with:
S.Sarkar K.Memarian L.Maranget S.Owens J.Alglave K.Wansbrough T.Ridge J.Pichon-Pharabod M.Batty K.Nienhuis M.Norrish F.Z.Nardelli D.P.Mulligan K.E.Gray A.Unyapoth G.L.Cattani R.Strnisa S.Kell S.Flur Christopher Pulte D.Williams G.Stoyle M.W.Hicks G.M.Bierman G.Peskine J.J.Leifer V.Vafeiadis V.B.F.Gomes M.J.Parkinson R.N.M.Watson Will Deacon A.Serjantov Jon French A.Sezgin T.Weber A.D.Gordon R.Harper J.Harrison A.Jeffrey J.Sevcík S.Jagannathan I.Neamtiu S.Lau D.Chisnall B.Davis Alexander Richardson D.Sheets T.Tuerk A.Giugliano A.Madhavapeddy S.Bishop M.Fairbairn M.Smith M.Allen-Williams P.Habouzit Justus Matthiesen James Lingard T.Braibant M.O.Myreen Robert M. Norton S.Mador-Haim R.Alur M.M.K.Martin A.Armstrong Thomas Bauereiss Brian Campbell 0001 A.Reid Prashanth Mundkur Mark Wassell I.Stark Neel Krishnaswami P.G.Neumann S.W.Moore John Baldwin James Clarke N.W.Filardo K.Gudka Alexandre Joannou Ben Laurie A. Theodore Markettos J. Edward Maste Alfredo Mazzinghi Edward Tomasz Napierala M.Roe Stacey D. Son J.Woodruff
Talks about:
concurr (11) semant (11) power (5) model (5) memori (4) multiprocessor (3) distribut (3) abstract (3) pointer (3) languag (3)

Person: Peter Sewell

DBLP DBLP: Sewell:Peter

Facilitated 1 volumes:

POPL 2014Ed

Contributed to:

ESOP 20152015
SOSP 20152015
ICFP 20142014
CAV 20122012
ICFP 20122012
PLDI 20122012
POPL 20122012
PLDI 20112011
POPL 20112011
TACAS 20112011
CAV 20102010
ISMM 20102010
POPL 20092009
FM 20082008
ICFP 20072007
OOPSLA 20072007
POPL 20062006
ICFP 20052005
POPL 20052005
ICFP 20032003
ESOP 20022002
POPL 20012001
LICS 20002000
ICALP 19981998
LICS 19941994
CAV (1) 20192019
OOPSLA 20162016
PLDI 20162016
POPL 20162016
POPL 20172017
POPL 20182018
POPL 20192019
ASPLOS 20192019

Wrote 40 papers:

ESOP-2015-BattyMNPS #concurrent #problem #programming language #semantics
The Problem of Programming Language Concurrency Semantics (MB, KM, KN, JPP, PS), pp. 283–307.
SOSP-2015-RidgeSTGMS #file system #named #specification #testing
SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems (TR, DS, TT, AG, AM, PS), pp. 38–53.
ICFP-2014-MulliganOGRS #named #reuse #semantics
Lem: reusable engineering of real-world semantics (DPM, SO, KEG, TR, PS), pp. 175–188.
CAV-2012-Mador-HaimMSMAOAMSW #axiom #memory management #multi
An Axiomatic Memory Model for POWER Multiprocessors (SMH, LM, SS, KM, JA, SO, RA, MMKM, PS, DW), pp. 495–512.
ICFP-2012-Sewell
Tales from the jungle (PS), pp. 271–272.
PLDI-2012-SarkarMOBSMAW #c #c++
Synchronising C/C++ and POWER (SS, KM, SO, MB, PS, LM, JA, DW), pp. 311–322.
POPL-2012-BattyMOSS #c #c++ #compilation #concurrent
Clarifying and compiling C/C++ concurrency: from C++11 to POWER (MB, KM, SO, SS, PS), pp. 509–520.
PLDI-2011-SarkarSAMW #comprehension #multi
Understanding POWER multiprocessors (SS, PS, JA, LM, DW), pp. 175–186.
POPL-2011-BattyOSSW #c++ #concurrent
Mathematizing C++ concurrency (MB, SO, SS, PS, TW), pp. 55–66.
POPL-2011-GordonHHJS #concurrent #verification
Robin Milner 1934--2010: verification, languages, and concurrency (ADG, RH, JH, AJ, PS), pp. 473–474.
POPL-2011-SevcikVNJS #compilation #concurrent
Relaxed-memory concurrency and verified compilation (JS, VV, FZN, SJ, PS), pp. 43–54.
TACAS-2011-AlglaveMSS #hardware #named #testing
Litmus: Running Tests against Hardware (JA, LM, SS, PS), pp. 41–44.
CAV-2010-AlglaveMSS #memory management #modelling
Fences in Weak Memory Models (JA, LM, SS, PS), pp. 258–272.
ISMM-2010-Sewell #abstraction #memory management
Memory, an elusive abstraction (PS), pp. 51–52.
POPL-2009-SarkarSNORBMA #multi #semantics
The semantics of x86-CC multiprocessor machine code (SS, PS, FZN, SO, TR, TB, MOM, JA), pp. 379–391.
FM-2008-RidgeNS #approach #implementation #network #protocol
A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service (TR, MN, PS), pp. 294–309.
ICFP-2007-SewellNOPRSS #effectiveness #named #semantics #tool support
Ott: effective tool support for the working semanticist (PS, FZN, SO, GP, TR, SS, RS), pp. 1–12.
OOPSLA-2007-StrniaaSP #design #java #semantics
The java module system: core design and semantic definition (RS, PS, MJP), pp. 499–514.
POPL-2006-BishopFNSSW #implementation #logic #specification #testing
Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations (SB, MF, MN, PS, MS, KW), pp. 55–66.
ICFP-2005-SewellLWNAHV #design #distributed #named #programming language
Acute: high-level programming language design for distributed computation (PS, JJL, KW, FZN, MAW, PH, VV), pp. 15–26.
POPL-2005-StoyleHBSN #predict
Mutatis mutandis: safe and predictable dynamic software updating (GS, MWH, GMB, PS, IN), pp. 183–194.
ICFP-2003-BiermanHSSW #question
Dynamic rebinding for marshalling and update, with destruct-time? (GMB, MWH, PS, GS, KW), pp. 99–110.
ICFP-2003-LeiferPSW
Global abstraction-safe marshalling with hash types (JJL, GP, PS, KW), pp. 87–98.
ESOP-2002-WansbroughNSS #semantics #thread
Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures (KW, MN, PS, AS), pp. 278–294.
POPL-2001-Sewell #data type #distributed #version control
Modules, abstract types, and distributed versioning (PS), pp. 236–247.
POPL-2001-UnyapothS #communication #framework #mobile
Nomadic pict: correct communication infrastructure for mobile computation (AU, PS), pp. 116–127.
LICS-2000-CattaniS #modelling #process
Models for Name-Passing Processes: Interleaving and Causal (GLC, PS), pp. 322–333.
ICALP-1998-Sewell #distributed #type system #π-calculus
Global/Local Subtyping and Capability Inference for a Distributed π-calculus (PS), pp. 695–706.
LICS-1994-Sewell #axiom #bisimulation #equation #first-order
Bisimulation is Not Finitely (First Order) Equationally Axiomatisable (PS), pp. 62–70.
CAV-2019-LauGMPS #c #concurrent #named #semantics
Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C (SL, VBFG, KM, JPP, PS), pp. 387–397.
OOPSLA-2016-KellMS #semantics
The missing link: explaining ELF static linking, semantically (SK, DPM, PS), pp. 607–623.
OOPSLA-2016-NienhuisMS #concurrent #semantics
An operational semantics for C/C++11 concurrency (KN, KM, PS), pp. 111–128.
PLDI-2016-MemarianMLNCWS #standard
Into the depths of C: elaborating the de facto standards (KM, JM, JL, KN, DC, RNMW, PS), pp. 1–15.
POPL-2016-FlurGPSSMDS #architecture #concurrent #modelling
Modelling the ARMv8 architecture, operationally: concurrency and ISA (SF, KEG, CP, SS, AS, LM, WD, PS), pp. 608–621.
POPL-2016-Pichon-Pharabod #concurrent #optimisation #semantics
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions (JPP, PS), pp. 622–633.
POPL-2017-FlurSPNMGSBS #concurrent
Mixed-size concurrency: ARM, POWER, C/C++11, and SC (SF, SS, CP, KN, LM, KEG, AS, MB, PS), pp. 429–442.
POPL-2018-PulteFDFSS #axiom #concurrent #modelling #multi
Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8 (CP, SF, WD, JF, SS, PS), p. 29.
POPL-2019-ArmstrongBCRGNM #semantics
ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS (AA, TB, BC0, AR, KEG, RMN, PM, MW, JF, CP, SF, IS, NK, PS), p. 31.
POPL-2019-MemarianGDKRWS #c #pointer #semantics
Exploring C semantics and pointer provenance (KM, VBFG, BD, SK, AR, RNMW, PS), p. 32.
ASPLOS-2019-DavisWRNMBCCFGJ #c #named #pointer #runtime
CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment (BD, RNMW, AR, PGN, SWM, JB, DC, JC, NWF, KG, AJ, BL, ATM, JEM, AM, ETN, RMN, MR, PS, SDS, JW), pp. 379–393.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.