Emmy: A Proof Assistant for Reasoning about Programs
Junfeng Xu · Zenodo (CERN European Organization for Nuclear Research) · 2019
We present Emmy, a proof assistant optimised for teaching and learning, that fills the gap between existing teaching tools and powerful practical theorem provers. Emmy supports a many-sorted first-order logic in which recursive functions, data structures, and arithmetic operations can be expressed. Emmy can express and prove the properties of many computer programs, in addition to theorems in propositional and first-order logic. To make it convenient for students to start using Emmy, we also developed a web-based interface for Emmy, which has been proven in tests to be easy to learn. Alternatively, the users may also write proofs in an LISP-like DSL, and check their proofs by ‘running’ them using Emmy’s interpreter. Since we intend to use Emmy in the teaching of the reasoning about programs course, we demonstrated the proving power of Emmy with regard to the course materials. The results are satisfying: we believe that Emmy has enough proving power to be used in actual teaching.