Ariel E. Kellison


I am a Ph.D. student in computer science at Cornell University, co-advised by David Bindel (Cornell) and Andrew Appel (Princeton). My current research primarily focuses on applying formal methods techniques to scientific and numerical software.



2022. Verified Numerical Methods for Ordinary Differential Equations. Ariel E. Kellison and Andrew W. Appel. NSV’22: 15th International Workshop on Numerical Software Verification, August 2022. [Paper]

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

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)[Paper]

2021. Formal Methods-Based Certification Frameworks for Scientific Computing Applications. Ariel Kellison, Geoff C. Hulette, John Bender, Samuel D. Pollard, and Heidi K. Thornquist. ASCR Workshop on Cybersecurity and Privacy for Scientific Computing Ecosystems, U.S. Department of Energy, Office of Advanced Scientific Computing Research, November 2021.

2019. Implementing Euclid’s Straightedge and Compass Constructions in Type Theory. Ariel E. Kellison, Mark Bickford, and Robert Constable. Annals of Mathematics and Artificial Intelligence. [Paper]


Teaching Experience


I hold a BS with honors in astrophysics from UC Santa Cruz.