Jean Pichon-Pharabod

According to our database, Jean Pichon-Pharabod authored at least 17 papers between 2015 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic.

Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod

Proc. ACM Program. Lang., January, 2024

2023

Iris-Wasm: Robust and Modular Verification of WebAssembly Programs.

Xiaojia Rao, Aïna Linn Georges, Maxime Legoupil, Conrad Watt, Jean Pichon-Pharabod, Philippa Gardner, Lars Birkedal

Proc. ACM Program. Lang., 2023

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, Lars Birkedal

Proc. ACM Program. Lang., 2023

2022

Relaxed virtual memory in Armv8-A (extended version).

Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell

CoRR, 2022

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

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

Relaxed virtual memory in Armv8-A.

Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell

Proceedings of the Programming Languages and Systems, 2022

2021

Two Mechanisations of WebAssembly 1.0.

Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner

Proceedings of the Formal Methods - 24th International Symposium, 2021

2020

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

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures.

Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell

Proceedings of the Programming Languages and Systems, 2020

2019

Weakening WebAssembly.

Conrad Watt, Andreas Rossberg, Jean Pichon-Pharabod

Proc. ACM Program. Lang., 2019

Promising-ARM/RISC-V: a simpler and faster operational concurrency model.

Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, Chung-Kil Hur

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

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, Peter Sewell

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

A no-thin-air memory model for programming languages.

Jean Yves Alexis Pichon-Pharabod

PhD thesis, 2018

A Separation Logic for a Promising Semantics.

Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis

Proceedings of the Programming Languages and Systems, 2018

2016

A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions.

Jean Pichon-Pharabod, Peter Sewell

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

2015

A Separation Logic for Fictional Sequential Consistency.

Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, Jean Pichon-Pharabod

Proceedings of the Programming Languages and Systems, 2015

The Problem of Programming Language Concurrency Semantics.

Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, Peter Sewell

Proceedings of the Programming Languages and Systems, 2015