references.bib

@inproceedings{Haas2017WebAssembly,
  author = {Andreas Haas and Andreas Rossberg and Derek L. Schuff and Ben L. Titzer and Michael Holman and Dan Gohman and Luke Wagner and Alon Zakai and J. F. Bastien},
  title = {Bringing the Web Up to Speed with {WebAssembly}},
  booktitle = {Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation},
  pages = {185--200},
  year = {2017},
  publisher = {Association for Computing Machinery},
  doi = {10.1145/3062341.3062363}
}

@manual{WasmCore30,
  author = {{WebAssembly Working Group}},
  title = {{WebAssembly Core Specification}, Release 3.0},
  year = {2026},
  note = {Binary format version 1},
  url = {https://webassembly.github.io/spec/core/}
}

@inproceedings{Watt2018Mechanising,
  author = {Conrad Watt},
  title = {Mechanising and Verifying the {WebAssembly} Specification},
  booktitle = {Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  pages = {53--65},
  year = {2018},
  publisher = {Association for Computing Machinery},
  doi = {10.1145/3167082}
}

@inproceedings{Watt2021Two,
  author = {Conrad Watt and Xiaojia Rao and Jean Pichon-Pharabod and Martin Bodin and Philippa Gardner},
  title = {Two Mechanisations of {WebAssembly} 1.0},
  booktitle = {Formal Methods: 24th International Symposium, FM 2021},
  series = {Lecture Notes in Computer Science},
  volume = {13047},
  pages = {61--79},
  year = {2021},
  publisher = {Springer},
  doi = {10.1007/978-3-030-90870-6_4}
}

@article{Watt2023WasmRef,
  author = {Conrad Watt and Maja Trela and Peter Lammich and Florian M{\"a}rkl},
  title = {{WasmRef-Isabelle}: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for {WebAssembly}},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {PLDI},
  articleno = {110},
  pages = {100--123},
  year = {2023},
  doi = {10.1145/3591224}
}

@article{Youn2024SpecTec,
  author = {Dongjun Youn and Joachim Breitner and Philippa Gardner and Jaehyun Lee and Sam Lindley and Matija Pretnar and Xiaojia Rao and Andreas Rossberg and Sukyoung Ryu and Wonho Shin and Conrad Watt},
  title = {Bringing the {WebAssembly} Standard Up to Speed with {SpecTec}},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {PLDI},
  year = {2024},
  doi = {10.1145/3656440}
}

@inproceedings{Watt2019WasmLogic,
  author = {Conrad Watt and Petar Maksimovi{\'c} and Neelakantan R. Krishnaswami and Philippa Gardner},
  title = {A Program Logic for First-Order Encapsulated {WebAssembly}},
  booktitle = {33rd European Conference on Object-Oriented Programming},
  series = {Leibniz International Proceedings in Informatics},
  volume = {134},
  pages = {9:1--9:30},
  year = {2019},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  doi = {10.4230/LIPIcs.ECOOP.2019.9}
}

@article{Rao2023IrisWasm,
  author = {Xiaojia Rao and A{\"i}na Linn Georges and Maxime Legoupil and Conrad Watt and Jean Pichon-Pharabod and Philippa Gardner and Lars Birkedal},
  title = {{Iris-Wasm}: Robust and Modular Verification of {WebAssembly} Programs},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {PLDI},
  articleno = {151},
  year = {2023},
  doi = {10.1145/3591265}
}

@inproceedings{Meier2025CertiCoqWasm,
  author = {Wolfgang Meier and Martin Jensen and Jean Pichon-Pharabod and Bas Spitters},
  title = {{CertiCoq-Wasm}: A Verified {WebAssembly} Backend for {CertiCoq}},
  booktitle = {Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  pages = {127--139},
  year = {2025},
  publisher = {Association for Computing Machinery},
  doi = {10.1145/3703595.3705879}
}

@article{Leroy2009CompCert,
  author = {Xavier Leroy},
  title = {Formal Verification of a Realistic Compiler},
  journal = {Communications of the ACM},
  volume = {52},
  number = {7},
  pages = {107--115},
  year = {2009},
  doi = {10.1145/1538788.1538814}
}

@article{Tan2019CakeML,
  author = {Yong Kiam Tan and Magnus O. Myreen and Ramana Kumar and Anthony Fox and Scott Owens and Michael Norrish},
  title = {The Verified {CakeML} Compiler Backend},
  journal = {Journal of Functional Programming},
  volume = {29},
  pages = {e2},
  year = {2019},
  doi = {10.1017/S0956796818000229}
}

@inproceedings{Pnueli1998TranslationValidation,
  author = {Amir Pnueli and Michael Siegel and Eli Singerman},
  title = {Translation Validation},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
  series = {Lecture Notes in Computer Science},
  volume = {1384},
  pages = {151--166},
  year = {1998},
  publisher = {Springer},
  doi = {10.1007/BFb0054170}
}

@inproceedings{Lopes2021Alive2,
  author = {Nuno P. Lopes and Juneyoung Lee and Chung-Kil Hur and Zhengyang Liu and John Regehr},
  title = {{Alive2}: Bounded Translation Validation for {LLVM}},
  booktitle = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
  pages = {65--79},
  year = {2021},
  publisher = {Association for Computing Machinery},
  doi = {10.1145/3453483.3454030}
}

@inproceedings{Necula1997PCC,
  author = {George C. Necula},
  title = {Proof-Carrying Code},
  booktitle = {Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  pages = {106--119},
  year = {1997},
  publisher = {Association for Computing Machinery},
  doi = {10.1145/263699.263712}
}

@inproceedings{Appel2001FoundationalPCC,
  author = {Andrew W. Appel},
  title = {Foundational Proof-Carrying Code},
  booktitle = {Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science},
  pages = {247--256},
  year = {2001},
  publisher = {IEEE},
  doi = {10.1109/LICS.2001.932501}
}

@inproceedings{Sewell2013KernelBinary,
  author = {Thomas Arthur Leck Sewell and Magnus O. Myreen and Gerwin Klein},
  title = {Translation Validation for a Verified {OS} Kernel},
  booktitle = {Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation},
  pages = {471--482},
  year = {2013},
  publisher = {Association for Computing Machinery},
  doi = {10.1145/2491956.2462183}
}

@inproceedings{Namjoshi2021SelfCertifying,
  author = {Kedar S. Namjoshi and Anton Xue},
  title = {A Self-Certifying Compilation Framework for {WebAssembly}},
  booktitle = {Verification, Model Checking, and Abstract Interpretation},
  series = {Lecture Notes in Computer Science},
  volume = {12597},
  pages = {127--148},
  year = {2021},
  publisher = {Springer},
  doi = {10.1007/978-3-030-67067-2_7}
}

@inproceedings{deMoura2021Lean4,
  author = {Leonardo de Moura and Sebastian Ullrich},
  title = {The {Lean} 4 Theorem Prover and Programming Language},
  booktitle = {Automated Deduction---CADE 28},
  series = {Lecture Notes in Computer Science},
  volume = {12699},
  pages = {625--635},
  year = {2021},
  publisher = {Springer},
  doi = {10.1007/978-3-030-79876-5_37}
}

@inproceedings{Limperg2023Aesop,
  author = {Jannis Limperg and Asta Halkj{\ae}r From},
  title = {{Aesop}: White-Box Best-First Proof Search for {Lean}},
  booktitle = {Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  pages = {253--266},
  year = {2023},
  publisher = {Association for Computing Machinery},
  doi = {10.1145/3573105.3575671}
}

@inproceedings{Yang2023LeanDojo,
  author = {Kaiyu Yang and Aidan Swope and Alex Gu and Rahul Chalamala and Peiyang Song and Shixing Yu and Saad Godil and Ryan J. Prenger and Animashree Anandkumar},
  title = {{LeanDojo}: Theorem Proving with Retrieval-Augmented Language Models},
  booktitle = {Advances in Neural Information Processing Systems 36},
  year = {2023},
  doi = {10.52202/075280-0944}
}

@article{Xin2024DeepSeekProver,
  author = {Huajian Xin and Daya Guo and Zhihong Shao and Zhizhou Ren and Qihao Zhu and Bo Liu and Chong Ruan and Wenda Li and Xiaodan Liang},
  title = {{DeepSeek-Prover}: Advancing Theorem Proving in {LLMs} through Large-Scale Synthetic Data},
  journal = {arXiv preprint arXiv:2405.14333},
  year = {2024},
  doi = {10.48550/arXiv.2405.14333}
}

@inproceedings{Thakur2024COPRA,
  author = {Amitayush Thakur and George Tsoukalas and Yeming Wen and Jimmy Xin and Swarat Chaudhuri},
  title = {An In-Context Learning Agent for Formal Theorem-Proving},
  booktitle = {Proceedings of the First Conference on Language Modeling},
  year = {2024},
  url = {https://openreview.net/forum?id=V7HRrxXUhN}
}

@inproceedings{Aniva2025Pantograph,
  author = {Leni Aniva and Chuyue Sun and Brando Miranda and Clark Barrett and Sanmi Koyejo},
  title = {{Pantograph}: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in {Lean} 4},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
  series = {Lecture Notes in Computer Science},
  volume = {15696},
  pages = {104--123},
  year = {2025},
  publisher = {Springer},
  doi = {10.1007/978-3-031-90643-5_6}
}

@inproceedings{Wang2024LEGOProver,
  author = {Haiming Wang and Huajian Xin and Chuanyang Zheng and Zhengying Liu and Qingxing Cao and Yinya Huang and Jing Xiong and Han Shi and Enze Xie and Jian Yin and Zhenguo Li and Xiaodan Liang},
  title = {{LEGO-Prover}: Neural Theorem Proving with Growing Libraries},
  booktitle = {Proceedings of the Twelfth International Conference on Learning Representations},
  year = {2024},
  url = {https://openreview.net/forum?id=3f5PALef5B}
}

@article{BerlotAttwell2024LibraryLearning,
  author = {Ian Berlot-Attwell and Frank Rudzicz and Xujie Si},
  title = {Library Learning Doesn't: The Curious Case of the Single-Use ``Library''},
  journal = {arXiv preprint arXiv:2410.20274},
  year = {2024},
  doi = {10.48550/arXiv.2410.20274}
}

@inproceedings{VanHattum2024VeriISLE,
  author = {Alexa VanHattum and Monica Pardeshi and Chris Fallin and Adrian Sampson and Fraser Brown},
  title = {Lightweight, Modular Verification for {WebAssembly}-to-Native Instruction Selection},
  booktitle = {Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems},
  pages = {231--248},
  year = {2024},
  publisher = {Association for Computing Machinery},
  doi = {10.1145/3617232.3624862}
}

@inproceedings{Johnson2021VeriWasm,
  author = {Evan Johnson and David Thien and Yousef Alhessi and Shravan Narayan and Fraser Brown and Sorin Lerner and Tyler McMullen and Stefan Savage and Deian Stefan},
  title = {Doveryai, no proveryai: {SFI} Safety for Native-Compiled {Wasm}},
  booktitle = {Proceedings of the Network and Distributed System Security Symposium},
  year = {2021},
  publisher = {Internet Society},
  doi = {10.14722/ndss.2021.24078}
}

@misc{TalosSoftware,
  author = {{Cajal Technologies}},
  title = {{Talos}: A {WebAssembly} Interpreter and Verification Framework in {Lean}},
  year = {2026},
  howpublished = {Software repository},
  note = {LeanExe evaluation revision bb3277e21c9786e3133d5c1601e34ebdc0bea4df},
  url = {https://github.com/cajal-technologies/talos}
}

@misc{LeanExeSoftware,
  author = {{LeanExe contributors}},
  title = {{LeanExe}: Compilation and Exact-Artifact Verification for {Lean} and {WebAssembly}},
  year = {2026},
  howpublished = {Software repository},
  note = {Manuscript snapshot 04f4170a141ef7bd289f81bc739f66d07471900d},
  url = {https://github.com/jsmorph/leanexe}
}

@misc{WasmTestsuite,
  author = {{WebAssembly Community Group}},
  title = {Official {WebAssembly} Specification Testsuite},
  year = {2026},
  howpublished = {Software repository},
  note = {LeanExe evaluation revision 9233a0a8d5920a8d32358ee915a3662ff3385029},
  url = {https://github.com/WebAssembly/testsuite}
}

@misc{WasmtimeSoftware,
  author = {{Bytecode Alliance}},
  title = {{Wasmtime}: A Standalone Runtime for {WebAssembly}},
  year = {2026},
  howpublished = {Software and documentation},
  note = {LeanExe evaluation version 44.0.0},
  url = {https://docs.wasmtime.dev/}
}

@article{Monniaux2022CompCertTCB,
  author = {David Monniaux and Sylvain Boulm{\'e}},
  title = {The Trusted Computing Base of the {CompCert} Verified Compiler},
  journal = {arXiv preprint arXiv:2201.10280},
  year = {2022},
  doi = {10.48550/arXiv.2201.10280}
}