Peter Sewell -

Registered user since Wed 14 Sep 2016

Name:Peter Sewell

Country:United Kingdom

Affiliation:University of Cambridge

Personal website:http://www.cl.cam.ac.uk/~pes20/

Contributions

POPL 2023	Author of CN: Verifying Systems C Code with Separation-Logic Refinement Types within the POPL-track
SPLASH 2022	Committee Member in Review Committee within the OOPSLA-track
PLDI 2022	Author of Islaris: Verification of Machine Code Against Authoritative ISA Semantics within the PLDI-track
POPL 2022	Author of VIP: Verifying Real-World C Idioms with Integer-Pointer Casts within the POPL-track
WITS 2022	Author of CN: A Refinement Type System for C within the WITS 2022-track
CPP 2021	Author of Invited Talk: Underpinning the foundations: Sail-based semantics, testing, and reasoning, for production and CHERI-enabled architectures within the CPP 2021-track
REMS-DeepSpec 2020	Author of ARMv8 and RISC-V relaxed memory concurrency within the REMS-DeepSpec 2020-track Author of Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V within the REMS-DeepSpec 2020-track Author of Welcome and brief project overviews within the REMS-DeepSpec 2020-track Author of Cerberus: executable reference semantics and memory object models for ISO and de facto C within the REMS-DeepSpec 2020-track Committee Member in Organizing Committee within the REMS-DeepSpec 2020-track Author of Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM} within the REMS-DeepSpec 2020-track
POPL 2020	Panelist in Panel within the POPLmark 15 Year Retrospective Panel-track Organizing Committee in Organizing Committee within the POPLmark 15 Year Retrospective Panel-track
HASE 2020	Speaker of Interactive Knowledge Shares within the HASE 2020-track
SPLASH 2019	Committee Member in External Review Committee within the OOPSLA-track
POPL 2019	Author of Exploring C Semantics and Pointer Provenance within the Research Papers-track Author of ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS within the Research Papers-track
WoSSCA 2018	Committee Member in Program Committee within the WoSSCA 2018-track
POPL 2018	Author of Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 within the Research Papers-track Author of Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8 within the Artifact Evaluation-track Committee Member in Program Committee within the Research Papers-track
PLDI 2017	Committee Member in External Program Committee
POPL 2017	Author of Mixed-size Concurrency: ARM, POWER, C/C++11, and SC within the POPL-track
PiP 2017	Committee Member in Program Committee within the PiP 2017-track
SPLASH 2016	Author of The Missing Link: Explaining ELF Static Linking, Semantically within the OOPSLA-track Author of An Operational Semantics for C/C++11 Concurrency within the OOPSLA-track
ICFP 2016	Committee Member in External Review Committee within the Research Papers-track
PLDI 2016	Author of Into the depths of C: elaborating the de facto standards within the Research Papers-track
POPL 2016	Author of Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA within the Research Papers-track Author of A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions within the Research Papers-track Committee Member in Steering Committee
PLDI 2015	Committee Member in External Review Committee within the Research Papers-track
ESOP 2015	Author of The Problem of Programming Language Concurrency Semantics within the ESOP-track