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.
jean.pichon at cs.au.dk
Office: Turing 129 (building 5341)
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.
I have received an AUFF Starting Grant and a Google ASPIRE 2021 award.
Reactive Scratch: helping children learn programming using the technology of the 80s (rather than that of the 60s).
- 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
- 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: 07 Oct 2022