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: Sewell:Peter
Facilitated 1 volumes:
EdContributed to:
2015
2015
2014
20122012
2012201220112011
20112010
20102009
20082007
2007200620052005200320022001
2000
199819942019201620162016201720182019
2019Wrote 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.