Theorem Provers: One Size Fits All?

Download

• Paper
• Poster
• Code

Abstract

Theorem provers are important tools for people working in formal verification. There are a myriad of interactive systems available today, with varying features and approaches motivating their development. These design choices impact their usability, alongside the problem domain in which they are employed. We test-drive two such provers — Coq and Idris2 — by proving the correctness of insertion sort, before providing a qualitative evaluation of their performance. We then compare their community and library support. This work helps users to make an informed choice of system, and highlight approaches in other systems that developers might find useful.

This work was completed as part of COMP2560 (Studies in Advanced Computing R&D) at the Australian National University, and presented at the 2023 ANU Computing Showcase.

Citation

Oates, H., Yun, G., Gurusinghe, N., 2023. “Theorem Provers: One Size Fits All?”. URL: harrisonoates.com/papers/comp2560itp/COMP2560TheoremProvers.pdf

@inproceedings{Oates2023,
  author    = {Harrison Oates and Geun Yun and Nikhila Gurusinghe},
  title     = {Theorem Provers: One Size Fits All?},
  year      = {2023},
  url       = {harrisonoates.com/papers/comp2560itp/COMP2560TheoremProvers.pdf}
}