I am a Department of Energy Computational Science Graduate Fellow and PhD candidate at Cornell University working on formal methods, programming languages, and computer arithmetic. I design foundational tools with rigorous guarantees that make it convenient for programmers to reason about numerical accuracy and correctness. As part of the VeriNum research group, I maintain the VCFloat and LAProof libraries for the Coq Proof Assistant.

I am fortunate to be co-advised by David Bindel (Cornell) and Andrew Appel (Princeton).

I can be reached by email at ak2485@cornell.edu.

Affiliations

• Ph.D. student, Department of Computer Science, Cornell University [Fall 2020 - current]. Advisor: David Bindel
• Graduate student intern, Digital Foundations & Mathematics Department, Sandia National Laboratories [June 2021 - current]

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]

Fellowships

• Department of Energy Computational Science Graduate Fellowship [Fall 2020 - current]

Teaching Experience

• Lecturer, Cornell CS 1110 - Introduction to Computing Using Python [Summer 2020]

Education

• BSc with honors in astrophysics from UC Santa Cruz.