@article{ho2024rust,
  author = {Ho, Son and Fromherz, Aymeric and Protzenko, Jonathan},
  title = {Sound Borrow-Checking for Rust via Symbolic Semantics},
  year = {2024},
  issue_date = {August 2024},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {8},
  number = {ICFP},
  url = {https://doi.org/10.1145/3674640},
  doi = {10.1145/3674640},
  journal = {Proc. ACM Program. Lang.},
  month = {aug},
  articleno = {251},
  numpages = {29},
  keywords = {Rust, Semantics, Verification}
}

@article{ho2024dafny,
  title={Incremental Proof Development in Dafny with Module-Based Induction},
  author={Ho, Son and Pit-Claudel, Clément},
  journal={ArXiv},
  year={2024},
  volume={abs/2401.16233},
  url={https://arxiv.org/abs/2401.16233},
}

@article{ho2023modularity,
  author = {Ho, Son and Fromherz, Aymeric and Protzenko, Jonathan},
  title = {Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification},
  year = {2023},
  issue_date = {August 2023},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {7},
  number = {ICFP},
  url = {https://doi.org/10.1145/3607844},
  doi = {10.1145/3607844},
  journal = {Proc. ACM Program. Lang.},
  month = {aug},
  articleno = {202},
  numpages = {32},
  keywords = {Cryptographic Primitives, Proof Engineering}
}

@article{ho2022aeneas,
  author = {Ho, Son and Protzenko, Jonathan},
  title = {Aeneas: Rust verification by functional translation},
  year = {2022},
  issue_date = {August 2022},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {6},
  number = {ICFP},
  url = {https://doi.org/10.1145/3547647},
  doi = {10.1145/3547647},
  journal = {Proc. ACM Program. Lang.},
  month = {aug},
  articleno = {116},
  numpages = {31},
  keywords = {verification, functional translation, Rust}
}

@inproceedings{ho2022noise,
  author={Ho, Son and Protzenko, Jonathan and Bichhawat, Abhishek and Bhargavan, Karthikeyan},
  booktitle={2022 IEEE Symposium on Security and Privacy (SP)}, 
  title={Noise: A Library of Verified High-Performance Secure Channel Protocol Implementations}, 
  year={2022},
  volume={},
  number={},
  pages={107-124},
  keywords={Resistance;Privacy;Freeware;Protocols;Codes;Libraries;Safety},
  doi={10.1109/SP46214.2022.9833621}}

@article{abrahamsson2020cakeml,
  author = {Abrahamsson, Oskar and Ho, Son and Kanabar, Hrutvik and Kumar, Ramana and Myreen, Magnus O. and Norrish, Michael and Tan, Yong Kiam},
  title = {Proof-Producing Synthesis of CakeML from Monadic HOL Functions},
  year = {2020},
  issue_date = {Oct 2020},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  volume = {64},
  number = {7},
  issn = {0168-7433},
  url = {https://doi.org/10.1007/s10817-020-09559-8},
  doi = {10.1007/s10817-020-09559-8},
  abstract = {We introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial examples, including the instruction encoder and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance. This development has been carried out in the HOL4 theorem prover.},
  journal = {J. Autom. Reason.},
  month = {oct},
  pages = {1287–1306},
  numpages = {20},
  keywords = {Interactive theorem proving, Program synthesis, ML, Higher-order logic}
}

@inproceedings{ho2018cakeml,
  author="Ho, Son
  and Abrahamsson, Oskar
  and Kumar, Ramana
  and Myreen, Magnus O.
  and Tan, Yong Kiam
  and Norrish, Michael",
  editor="Galmiche, Didier
  and Schulz, Stephan
  and Sebastiani, Roberto",
  title="Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions",
  booktitle="Automated Reasoning",
  year="2018",
  publisher="Springer International Publishing",
  address="Cham",
  pages="646--662",
  isbn="978-3-319-94205-6"
}

@inproceedings{feree2018io,
  author = {F\'{e}r\'{e}e, Hugo and \r{A}man Pohjola, Johannes and Kumar, Ramana and Owens, Scott and Myreen, Magnus O. and Ho, Son},
  title = {Program Verification in the Presence of I/O: Semantics, Verified Library Routines, and Verified Applications},
  year = {2018},
  isbn = {978-3-030-03591-4},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  url = {https://doi.org/10.1007/978-3-030-03592-1_6},
  doi = {10.1007/978-3-030-03592-1_6},
  booktitle = {Verified Software. Theories, Tools, and Experiments: 10th International Conference, VSTTE 2018, Oxford, UK, July 18–19, 2018, Revised Selected Papers},
  pages = {88–111},
  numpages = {24},
  location = {Oxford, United Kingdom}
}