Jean Pichon-Pharabod
Tenure-track assistant professor in the Logic & Semantics group at the Institut for Datalogi of Aarhus University.
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, and an affiliated lecturer.
Contact
jean.pichon at cs.au.dk
Office: Turing 129 (building 5341)
Google Scholar
orcid: 0000-0002-4442-6543
institutional webpage
Research interests
I am interested in bridging the gap between programming language theory and the industrial practice of programming with real-world systems, focusing in particular on relaxed memory concurrency and systems programming, from modelling and tooling to developing new reasoning methods
I am looking for motivated PhD students, PostDocs, and interns.
Students
Funding
I have received an AUFF Starting Grant and a Google ASPIRE 2021 award.
Outreach
Reactive Scratch: helping children learn programming using the technology of the 80s (rather than that of the 60s).
Teaching
Student projects
Student projects
Software
Publications
See DBLP.
- An axiomatic basis for computer programming on the relaxed Arm-A architecture, Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod, in POPL 2024 pdf
- VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A, Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, and Lars Birkedal, in PLDI 2023 pdf
- Iris-Wasm: Robust and Modular Verification of WebAssembly Programs, Xiaojia Rao, Aïna Linn Georges, Conrad Watt, Maxime Legoupil, Jean Pichon-Pharabod, Philippa Gardner, and Lars Birkedal, in PLDI 2023 pdf
- Islaris: Verification of Machine Code Against Authoritative ISA Semantics, Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell, in PLDI 2022 pdf
- Relaxed virtual memory in Armv8-A, Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell, in ESOP 2022 pdf
- Two Mechanisations of WebAssembly 1.0, Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner, in FM 2021 pdf
- 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
- 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: 23 Apr 2024