01whole.pdf (13.92 MB)
Atom editor support for the Coq proof assistant
thesisposted on 2022-03-28, 16:58 authored by Ken Hosogoe
Interactive theorem proves are important tools which aid in the creation of formal proofs, specification and software verification. The current state of proof assistant IDEs are dated, and missing features that could be offered by modern IDEs. This project will design and implement and Atom package to provide support for the Coq proof assistant. The project evaluated IDEs and proof assistants for various features to implement. Identified features were syntax highlighting, auto completion, IDE to Coq interaction (PIDE) and linting. These features were designed and implemented. This project was able to create a package that implements basic support for the Coq proof assistant for the Atom source code editor.