### Ariel Kellison

**Program Years:**2020-2024**Academic Institution:**Cornell University**Field of Study:**Computer Science**Academic Advisor:**David Bindel**Practicum(s):**

Sandia National Laboratories, California (2021)**Degree(s):**

B.S. Astrophysics, University of California, Santa Cruz, 2010

#### Current Status

**Status:**Graduate Student**Research Area:**Computer Science**Personal URL:**https://ak-2485.github.io/

#### Publications

VCFloat2: Floating-Point Error Analysis in Coq. Andrew Appel and Ariel Kellison. 2024. In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024).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), September 2023.

Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method. Mohit Tekriwal, Andrew W. Appel, Ariel E. Kellison, Jean-Baptiste Jeannin, and David Bindel. To appear in proceedings of the 16th Conference on Intelligent Computer Mathematics (CICM), September 2023.

Towards Verified Rounding-Error Analysis for Stationary Iterative Methods. Ariel E. Kellison, Mohit Tekriwal, Jean-Baptiste Jeannin, and Geoffrey Hulette. Correctness 2022: Sixth International Workshop on Software Correctness for HPC Applications, November 2022.

Verified Numerical Methods for Ordinary Differential Equations. Ariel E. Kellison and Andrew W. Appel. In Proceedings of the 15th International Workshop on Numerical Software Verification, NSV 2022. Haifa, Israel, August 2022.

A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem. Ariel E. Kellison. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022. Philadelphia, USA, January 2022.

Global Stochastic Optimization of Stellarator Coil Configurations. Silke Glas, Misha Padidar, Ariel E. Kellison, and David Bindel. Journal of Plasma Physics, April 2022.

Implementing Euclid's Straightedge and Compass Constructions in Type Theory.

Ariel E. Kellison, Mark Bickford, and Robert Constable. Annals of Mathematics and Artificial Intelligence, April 2019.