Jean Pichon-Pharabod

I have moved to Aarhus University, see my new webpage.
Before that, I was a Research associate in Peter Sewell's group at the Computer Laboratory of the University of Cambridge, working on the REMS project.
Affiliated lecturer, lecturing Part II (3rd year) Hoare Logic & Model Checking.

Contact

jean.pichon at cl.cam.ac.uk
Google Scholar
orcid: 0000-0002-4442-6543

Outreach

Reactive Scratch: helping children learn programming using the technology of the 80s (rather than that of the 60s).

Student projects

Software

CppMem, an interactive C/C++ memory model explorer
Cerberus-BMC, an executable semantics for a substantial fragment of C
wasm_coq, a Coq formalisation of WebAssembly 1.0 (based on C. Watt's WebAssembly semantics in Isabelle) (student project - work in progress)

Publications

See DBLP.

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, in PLDI 2020 pdf
ARMv8-A system semantics: instruction fetch in relaxed architectures, Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, and Peter Sewell, in ESOP 2020 pdf
Weakening WebAssembly, Conrad Watt, Andreas Rossberg, Jean Pichon-Pharabod, in OOPSLA 2019 pdf
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, and Peter Sewell, in CAV 2019 pdf
Promising-ARM/RISC-V: a simpler and faster operational concurrency model, Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, and Chung-Kil Hur, in PLDI 2019 pdf
A separation logic for a promising semantics, Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, and Viktor Vafeiadis, in ESOP 2018 pdf
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions, Jean Pichon-Pharabod and Peter Sewell, in POPL 2016 pdf (more details)
A Separation Logic for Fictional Sequential Consistency, Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, and Jean Pichon-Pharabod, in ESOP 2015 pdf
The Problem of Programming Language Concurrency Semantics, Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell, in ESOP 2015 pdf

Thesis: A no-thin-air memory model for programming languages, Jean Pichon-Pharabod webpage

Last modified: 8 Sep 2021