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.
History
Table of Contents
1. Introduction -- 2. Background and related work -- 3. Design -- 4. Implementation -- 5. Discussion -- 6. Conclusion -- 7. Abbreviations -- Appendices -- Bibliography.
Notes
Empirical thesis.
Bibliography: pages 85-86
Awarding Institution
Macquarie University
Degree Type
Thesis bachelor honours
Degree
BSc (Hons), Macquarie University, Faculty of Science and Engineering, School of Engineering
Department, Centre or School
School of Engineering
Year of Award
2016
Principal Supervisor
Anthony Sloane
Rights
Copyright Ken Hosogoe 2016.
Copyright disclaimer: http://mq.edu.au/library/copyright