Ariel E. Kellison


I am a Ph.D. candidate in computer science at Cornell University, co-advised by David Bindel (Cornell) and Andrew Appel (Princeton). I develop methods to formally guarantee the accuracy and correctness of numerical software. As part of the VeriNum research group, I maintain the VCFloat and LAProof libraries for the Coq Proof Assistant.

I can be reached by email at


Selected Publications

2024. Numerical Fuzz: A Type System for Rounding Error Analysis. Ariel E. Kellison and Justin Hsu. To appear in the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Copenhagen, Denmark. [Paper]

2024. VCFloat2: Floating-point Error Analysis in Coq. Andrew W. Appel and Ariel E. Kellison. In proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), London, UK. [Paper]

2023. LAProof: A Library of Formal Proofs of Accuracy and Correctness for Linear Algebra Programs. Ariel E. Kellison, Andrew W. Appel, Mohit Tekriwal, and David Bindel. In proceedings of the 30th IEEE International Symposium on Computer Arithmetic (ARITH), Portland, OR, USA. [Paper]

Selected Reports

2024. The first tri-lab workshop on formal verification: Capabilities, challenges, research opportunities, and exemplars. S. D. Pollard, J. M. Aytac, A. Kellison, I. Laguna, S. Nedunuri, S. Reis, M. J. Sottile, and H. K. Thornquist. Technical report, Sandia National Laboratories. [Report]


Teaching Experience