The Problem of Programming Language Concurrency Semantics. - Mark Batty; Kayvan Memarian; Kyndylan Nienhuis; Jean Pichon-Pharabod; Peter Sewell (ESOP, 2015)

A Separation Logic for Fictional Sequential Consistency. - Filip Sieczkowski; Kasper Svendsen; Lars Birkedal; Jean Pichon-Pharabod (ESOP, 2015)

A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. - Jean Pichon-Pharabod; Peter Sewell (POPL, 2016)

A Separation Logic for a Promising Semantics. - Kasper Svendsen; Jean Pichon-Pharabod; Marko Doko; Ori Lahav 001; Viktor Vafeiadis (ESOP, 2018)

A no-thin-air memory model for programming languages. - Jean Yves Alexis Pichon-Pharabod (2018)

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; Peter Sewell (CAV (1), 2019)

Promising-ARM/RISC-V: a simpler and faster operational concurrency model. - Christopher Pulte; Jean Pichon-Pharabod; Jeehoon Kang; Sung-Hwan Lee 001; Chung-Kil Hur (PLDI, 2019)

Weakening WebAssembly. - Conrad Watt; Andreas Rossberg; Jean Pichon-Pharabod (Proc. ACM Program. Lang., 2019)

ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures. - Ben Simner; Shaked Flur; Christopher Pulte; Alasdair Armstrong; Jean Pichon-Pharabod; Luc Maranget; Peter Sewell (ESOP, 2020)

Repairing and mechanising the JavaScript relaxed memory model. - Conrad Watt; Christopher Pulte; Anton Podkopaev; Guillaume Barbier; Stephen Dolan; Shaked Flur; Jean Pichon-Pharabod; Shu-yu Guo (PLDI, 2020)

Two Mechanisations of WebAssembly 1.0. - Conrad Watt; Xiaojia Rao; Jean Pichon-Pharabod; Martin Bodin; Philippa Gardner (FM, 2021)

Relaxed virtual memory in Armv8-A. - Ben Simner; Alasdair Armstrong; Jean Pichon-Pharabod; Christopher Pulte; Richard Grisenthwaite; Peter Sewell (ESOP, 2022)

Islaris: verification of machine code against authoritative ISA semantics. - Michael Sammler; Angus Hammond; Rodolphe Lepigre; Brian Campbell 001; Jean Pichon-Pharabod; Derek Dreyer; Deepak Garg 001; Peter Sewell (PLDI, 2022)

Relaxed virtual memory in Armv8-A (extended version). - Ben Simner; Alasdair Armstrong; Jean Pichon-Pharabod; Christopher Pulte; Richard Grisenthwaite; Peter Sewell (CoRR, 2022)

VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A. - Zongyuan Liu 001; Sergei Stepanenko; Jean Pichon-Pharabod; Amin Timany; Aslan Askarov; Lars Birkedal (Proc. ACM Program. Lang., 2023)

Iris-Wasm: Robust and Modular Verification of WebAssembly Programs. - Xiaojia Rao; Aïna Linn Georges; Maxime Legoupil; Conrad Watt; Jean Pichon-Pharabod; Philippa Gardner; Lars Birkedal (Proc. ACM Program. Lang., 2023)

Relaxed exception semantics for Arm-A (extended version). - Ben Simner; Alasdair Armstrong; Thomas Bauereiss; Brian Campbell 001; Ohad Kammar; Jean Pichon-Pharabod; Peter Sewell (CoRR, 2024)

Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly. - Maxime Legoupil; June Rousseau; Aïna Linn Georges; Jean Pichon-Pharabod; Lars Birkedal (Proc. ACM Program. Lang., 2024)

An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. - Angus Hammond; Zongyuan Liu 001; Thibaut Pérami; Peter Sewell; Lars Birkedal; Jean Pichon-Pharabod (Proc. ACM Program. Lang., 2024)

Artifact and Appendix of 'Iris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe WebAssembly'. - Maxime Legoupil; June Rousseau; Aïna Linn Georges; Jean Pichon-Pharabod; Lars Birkedal (Zenodo, 2024)

CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq. - Wolfgang Meier; Martin Jensen; Jean Pichon-Pharabod; Bas Spitters (CPP, 2025)

Precise exceptions in relaxed architectures. - Ben Simner; Alasdair Armstrong; Thomas Bauereiss; Brian Campbell 001; Ohad Kammar; Jean Pichon-Pharabod; Peter Sewell (ISCA, 2025)