| 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 | 135 | 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 | 108 | 2016 |
| 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 | 65 | 2019 |
| 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 | 63 | 2018 |
| Weakening WebAssembly C Watt, A Rossberg, J Pichon-Pharabod Proceedings of the ACM on Programming Languages 3 (OOPSLA), 1-28, 2019 | 39 | 2019 |
| 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 | 31 | 2022 |
| 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 | 31 | 2020 |
| 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 | 28 | 2021 |
| 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 | 27 | 2015 |
| 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 | 26 | 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 | 22 | 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 | 16 | 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 | 14 | 2019 |
| 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 Proceedings of the ACM on Programming Languages 8 (POPL), 604-637, 2024 | 7 | 2024 |
| Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly M Legoupil, J Rousseau, AL Georges, J Pichon-Pharabod, L Birkedal Proceedings of the ACM on Programming Languages 8 (OOPSLA2), 304-332, 2024 | 2 | 2024 |
| CertiCoq-Wasm: Verified compilation from Coq to WebAssembly W Meier, J Pichon-Pharabod, B Spitters CoqPL, 2024 | 2 | 2024 |
| 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 | 2 | 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 | 2 | 2023 |
| 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 |
Peter SewellComputer Laboratory, University of CambridgeEmail verificata su cl.cam.ac.uk
