Refereed Publications

  1. Carl Kwan, Quang Dao, and Justin Thaler. “Verifying Jolt zkVM Lookup Semantics”. Submitted. Preprint: https://ia.cr/2024/1841.

  2. Carl Kwan and Warren Hunt. “Automatic Verification of Right-Greedy Numerical Linear Algebra Algorithms”. Oct. 2024. In: Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design (FMCAD 2024). pp. 242–250. doi: 10.34727/2024/isbn.978-3-85448-065-5_30.

  3. Carl Kwan and Warren Hunt. “Formalizing the Cholesky Factorization Theorem”. Sep. 2024. In: 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 25:1-25:16. doi: 10.4230/LIPIcs.ITP.2024.25

  4. Carl Kwan, Yutong Xin, and William D. Young. “CHERI Concentrate in ACL2”. Nov. 2023. In: Electronic Proceedings in Theoretical Computer Science 393, pp. 6–10. doi: 10.4204/EPTCS.393.2. Best Student Paper Award — 2nd Place.

  5. Carl Kwan. “Classical LU Decomposition in ACL2”. Nov. 2023. In: Electronic Proceedings in Theoretical Computer Science 393, pp. 1–5. doi: 10.4204/EPTCS.393.1.

  6. Carl Kwan, Yan Peng, and Mark R. Greenstreet. May 2020. “Cauchy-Schwarz in ACL2(r) Abstract Vector Spaces”. In: Electronic Proceedings in Theoretical Computer Science 327, pp. 90–92. doi: 10.4204/EPTCS.327.8.

  7. Carl Kwan and Mark R. Greenstreet. Oct. 2018. “Convex Functions in ACL2(r)”. In: Electronic Proceedings in Theoretical Computer Science 280, pp. 128–142. doi: 10.4204/eptcs.280.10.

  8. Carl Kwan and Mark R. Greenstreet. Oct. 2018. “Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r)”. In: Electronic Proceedings in Theoretical Computer Science 280, pp. 111–127. doi: 10.4204/eptcs.280.9.

Invited

  1. Carl Kwan. Jan. 4, 2022. Towards Formalized Matrix Analysis and Algorithms. International Symposium on Artificial Intelligence and Mathematics Fort Lauderdale, FL. January 3–5, 2022. url: https://isaim2022.cs.ou.edu/papers/ISAIM2022_Formalization_Kwan.pdf.

Technical Reports

  1. Carl Kwan. Apr. 23, 2018. Choosing Metrics for Translating Embeddings in Recommender Systems. url: http://cs.utexas.edu/~carlkwan/papers/choosing-metrics-transe.pdf.

  2. Carl Kwan. Apr. 20, 2018. Galois Theory and Questions of Feasibility in Graph Drawing. url: http://cs.utexas.edu/~carlkwan/papers/galois-graph-drawing.pdf.

Unpublished

  1. Carl Kwan. “Some ACL2(r) Matrix Norms”. In Preparation.