Implementing Euclid's straightedge and compass constructions in type theory. - Ariel Kellison; Mark Bickford; Robert L. Constable (Ann. Math. Artif. Intell., 2019)

Verified Numerical Methods for Ordinary Differential Equations. - Ariel E. Kellison; Andrew W. Appel (NSV/FoMLAS@CAV, 2022)

Towards Verified Rounding Error Analysis for Stationary Iterative Methods. - Ariel Kellison; Mohit Tekriwal; Jean-Baptiste Jeannin; Geoffrey C. Hulette (Correctness@SC, 2022)

A machine-checked direct proof of the Steiner-lehmus theorem. - Ariel Kellison (CPP, 2022)

LAProof: A Library of Formal Proofs of Accuracy and Correctness for Linear Algebra Programs. - Ariel E. Kellison; Andrew W. Appel; Mohit Tekriwal; David Bindel (ARITH, 2023)

Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method. - Mohit Tekriwal; Andrew W. Appel; Ariel E. Kellison; David Bindel; Jean-Baptiste Jeannin (CICM, 2023)

VCFloat2: Floating-Point Error Analysis in Coq. - Andrew W. Appel; Ariel Kellison (CPP, 2024)

Numerical Fuzz: A Type System for Rounding Error Analysis. - Ariel E. Kellison; Justin Hsu (Proc. ACM Program. Lang., 2024)

Bean: A Language for Backward Error Analysis. - Ariel E. Kellison; Laura Zielinski; David Bindel; Justin Hsu (Proc. ACM Program. Lang., 2025)

Type-Based Approaches to Rounding Error Analysis. - Ariel E. Kellison (CoRR, 2025)