01whole.pdf (13.92 MB)
Download file

Atom editor support for the Coq proof assistant

Download (13.92 MB)
posted 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.


Table of Contents

1. Introduction -- 2. Background and related work -- 3. Design -- 4. Implementation -- 5. Discussion -- 6. Conclusion -- 7. Abbreviations -- Appendices -- Bibliography.


Empirical thesis. Bibliography: pages 85-86

Awarding Institution

Macquarie University

Degree Type

Thesis bachelor honours


BSc (Hons), Macquarie University, Faculty of Science and Engineering, School of Engineering

Department, Centre or School

School of Engineering

Year of Award


Principal Supervisor

Anthony Sloane


Copyright Ken Hosogoe 2016. Copyright disclaimer: http://mq.edu.au/library/copyright




1 online resource (xv, 86 pages diagrams, tables)

Former Identifiers

mq:70349 http://hdl.handle.net/1959.14/1262817

Usage metrics