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 | 122 | 2015 |
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 | 100 | 2016 |
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 | 57 | 2018 |
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 | 52 | 2019 |
Weakening WebAssembly C Watt, A Rossberg, J Pichon-Pharabod Proceedings of the ACM on Programming Languages 3 (OOPSLA), 1-28, 2019 | 36 | 2019 |
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 | 25 | 2015 |
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 | 24 | 2020 |
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 | 22 | 2022 |
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 | 20 | 2021 |
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 | 19 | 2020 |
Relaxed virtual memory in Armv8-A B Simner, A Armstrong, J Pichon-Pharabod, C Pulte, R Grisenthwaite, ... European Symposium on Programming, 143-173, 2022 | 14 | 2022 |
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 | 13 | 2023 |
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 | 12 | 2019 |
A no-thin-air memory model for programming languages JYA Pichon-Pharabod University of Cambridge, 2018 | 2 | 2018 |
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 | 1 | 2023 |
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 | 1 | 2023 |
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A Z Liu, S Stepanenko, J Pichon-Pharabod, A Timany | 1 | 2023 |
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, ... | 1* | |
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 |