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, lecturing Part II (3rd year) Hoare Logic & Model Checking.
Contact
jean.pichon at cs.au.dk
Office: Turing 129 (building 5341)
Google Scholar
orcid: 0000-0002-4442-6543
academic 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.
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).
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: 20 Dec 2023