Jean Pichon-Pharabod

22 papers A* 5A 5B 2Journal 9Unranked 1
YearRankTypeTitle / Venue / Authors
2026 J jnl
An Axiomatic Basis for Computer Programming on Relaxed Hardware Architectures: The AxSL Logics.
ACM Trans. Program. Lang. Syst.
Zongyuan Liu, Angus Hammond, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod
2025 B conf
CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq.
CPP
Wolfgang Meier, Martin Jensen, Jean Pichon-Pharabod, Bas Spitters
2025 A* conf
Precise exceptions in relaxed architectures.
ISCA
Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, Peter Sewell
2024 J jnl
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic.
Proc. ACM Program. Lang.
Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod
2024 J jnl
Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly.
Proc. ACM Program. Lang.
Maxime Legoupil, June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod, Lars Birkedal
2024 J jnl
Relaxed exception semantics for Arm-A (extended version).
CoRR
Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, Peter Sewell
2023 J jnl
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs.
Proc. ACM Program. Lang.
Xiaojia Rao, Aïna Linn Georges, Maxime Legoupil, Conrad Watt, Jean Pichon-Pharabod, Philippa Gardner, Lars Birkedal
2023 J jnl
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A.
Proc. ACM Program. Lang.
Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, Lars Birkedal
2022 A* conf
Islaris: verification of machine code against authoritative ISA semantics.
PLDI
Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell
2022 J jnl
Relaxed virtual memory in Armv8-A (extended version).
CoRR
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell
2022 A conf
Relaxed virtual memory in Armv8-A.
ESOP
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell
2021 B conf
Two Mechanisations of WebAssembly 1.0.
FM
Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner
2020 A conf
ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures.
ESOP
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell
2020 J jnl
Repairing and Mechanising the JavaScript Relaxed Memory Model.
CoRR
Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod, Shu-Yu Guo
2020 A* conf
Repairing and mechanising the JavaScript relaxed memory model.
PLDI
Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod, Shu-Yu Guo
2019 — conf
Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C.
CAV (1)
Stella Lau, Victor B. F. Gomes, Kayvan Memarian, Jean Pichon-Pharabod, Peter Sewell
2019 A* conf
Promising-ARM/RISC-V: a simpler and faster operational concurrency model.
PLDI
Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, Chung-Kil Hur
2019 J jnl
Weakening WebAssembly.
Proc. ACM Program. Lang.
Conrad Watt, Andreas Rossberg, Jean Pichon-Pharabod
2018 A conf
A Separation Logic for a Promising Semantics.
ESOP
Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis
2016 A* conf
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions.
POPL
Jean Pichon-Pharabod, Peter Sewell
2015 A conf
A Separation Logic for Fictional Sequential Consistency.
ESOP
Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, Jean Pichon-Pharabod
2015 A conf
The Problem of Programming Language Concurrency Semantics.
ESOP
Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, Peter Sewell