Ariel E. Kellison

Logo

I am finishing my PhD in computer science at Cornell in fall 2024! I’ll be joining the Digital Foundations & Mathematics Department at Sandia National Laboratories as a postdoctoral researcher in December of 2024.

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.

During my PhD, I was co-advised by David Bindel (Cornell) and Andrew Appel (Princeton). I was supported by the Department of Energy Computational Science Graduate Fellowship.

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

Affiliations

Drafts and Ongoing Work

2024. Bean: A Language for Backward Error Analysis. Ariel E. Kellison, Laura Zielinksi, David Bindel, and Justin Hsu.

Selected Publications

2024. Numerical Fuzz: A Type System for Rounding Error Analysis. Ariel E. Kellison and Justin Hsu. In proceedings of 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

Teaching Experience

Education