Follow
Jean Pichon-Pharabod
Title
Cited by
Cited by
Year
The problem of programming language concurrency semantics
M Batty, K Memarian, K Nienhuis, J Pichon-Pharabod, P Sewell
Programming Languages and Systems: 24th European Symposium on Programming …, 2015
1212015
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
J Pichon-Pharabod, P Sewell
ACM SIGPLAN Notices 51 (1), 622-633, 2016
992016
A separation logic for a promising semantics
K Svendsen, J Pichon-Pharabod, M Doko, O Lahav, V Vafeiadis
Programming Languages and Systems: 27th European Symposium on Programming …, 2018
562018
Promising-ARM/RISC-V: a simpler and faster operational concurrency model
C Pulte, J Pichon-Pharabod, J Kang, SH Lee, CK Hur
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language …, 2019
492019
Weakening WebAssembly
C Watt, A Rossberg, J Pichon-Pharabod
Proceedings of the ACM on Programming Languages 3 (OOPSLA), 1-28, 2019
352019
A separation logic for fictional sequential consistency
F Sieczkowski, K Svendsen, L Birkedal, J Pichon-Pharabod
Programming Languages and Systems: 24th European Symposium on Programming …, 2015
252015
Repairing and mechanising the JavaScript relaxed memory model
C Watt, C Pulte, A Podkopaev, G Barbier, S Dolan, S Flur, ...
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language …, 2020
232020
Islaris: verification of machine code against authoritative ISA semantics
M Sammler, A Hammond, R Lepigre, B Campbell, J Pichon-Pharabod, ...
Proceedings of the 43rd ACM SIGPLAN International Conference on Programming …, 2022
212022
ARMv8-A system semantics: instruction fetch in relaxed architectures
B Simner, S Flur, C Pulte, A Armstrong, J Pichon-Pharabod, L Maranget, ...
Programming Languages and Systems: 29th European Symposium on Programming …, 2020
182020
Two mechanisations of webassembly 1.0
C Watt, X Rao, J Pichon-Pharabod, M Bodin, P Gardner
Formal Methods: 24th International Symposium, FM 2021, Virtual Event …, 2021
172021
Cerberus-BMC: A principled reference semantics and exploration tool for concurrent and sequential C
S Lau, VBF Gomes, K Memarian, J Pichon-Pharabod, P Sewell
Computer Aided Verification: 31st International Conference, CAV 2019, New …, 2019
122019
Relaxed virtual memory in Armv8-A
B Simner, A Armstrong, J Pichon-Pharabod, C Pulte, R Grisenthwaite, ...
European Symposium on Programming, 143-173, 2022
112022
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
X Rao, AL Georges, M Legoupil, C Watt, J Pichon-Pharabod, P Gardner, ...
Proceedings of the ACM on Programming Languages 7 (PLDI), 1096-1120, 2023
102023
A no-thin-air memory model for programming languages
JYA Pichon-Pharabod
University of Cambridge, 2018
22018
Research data for" An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic"
A Hammond, Z Liu, T Pérami, P Sewell, L Birkedal, J Pichon-Pharabod
12023
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A
Z Liu, S Stepanenko, J Pichon-Pharabod, A Timany, A Askarov, L Birkedal
Proceedings of the ACM on Programming Languages 7 (PLDI), 1438-1462, 2023
12023
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A
Z Liu, S Stepanenko, J Pichon-Pharabod, A Timany
12023
CertiCoq-Wasm: Verified compilation from Coq to WebAssembly
W Meier, J Pichon-Pharabod, B Spitters
2023
Relaxed virtual memory in Armv8-A (extended version)
B Simner, A Armstrong, J Pichon-Pharabod, C Pulte, R Grisenthwaite, ...
arXiv preprint arXiv:2203.00642, 2022
2022
Weakening WebAssembly
J Pichon-Pharabod, C Watt, A Rossberg
Association for Computing Machinery, 2019
2019
The system can't perform the operation now. Try again later.
Articles 1–20