| Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions S Ho, O Abrahamsson, R Kumar, MO Myreen, YK Tan, M Norrish International Joint Conference on Automated Reasoning, 646-662, 2018 | 31 | 2018 |
| Aeneas: Rust verification by functional translation S Ho, J Protzenko Proceedings of the ACM on Programming Languages 6 (ICFP), 711-741, 2022 | 27 | 2022 |
| Noise*: a library of verified high-performance secure channel protocol implementations S Ho, J Protzenko, A Bichhawat, K Bhargavan 2022 IEEE Symposium on Security and Privacy (SP), 107-124, 2022 | 14 | 2022 |
| Proof-producing synthesis of CakeML from monadic HOL functions O Abrahamsson, S Ho, H Kanabar, R Kumar, MO Myreen, M Norrish, ... Journal of Automated Reasoning 64 (7), 1287-1306, 2020 | 13 | 2020 |
| Program Verification in the Presence of I/O H Férée, J Åman Pohjola, R Kumar, S Owens, MO Myreen, S Ho Working Conference on Verified Software: Theories, Tools, and Experiments …, 2018 | 13 | 2018 |
| Zero-cost meta-programmed stateful functors in F J Protzenko, S Ho arXiv preprint arXiv:2102.01644, 2021 | 2 | 2021 |
| Sound Borrow-Checking for Rust via Symbolic Semantics S Ho, A Fromherz, J Protzenko arXiv preprint arXiv:2404.02680, 2024 | | 2024 |
| Incremental Proof Development in Dafny with Module-Based Induction S Ho, C Pit-Claudel arXiv preprint arXiv:2401.16233, 2024 | | 2024 |
| Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification S Ho, A Fromherz, J Protzenko Proceedings of the ACM on Programming Languages 7 (ICFP), 385-416, 2023 | | 2023 |
| Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Long Version) S Ho, J Protzenko, A Bichhawat, K Bhargavan Cryptology ePrint Archive, 2022 | | 2022 |
| Internship proposal: Formal verification of Rust programs S Ho, K Bhargavan | | |
| Program Verification in the Presence of I/O H Férée, JÅ Pohjola, R Kumar, S Owens, MO Myreen, S Ho | | |
