01whole.pdf (13.92 MB)
Download file

Atom editor support for the Coq proof assistant

Download (13.92 MB)
thesis
posted on 28.03.2022, 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.

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

Language

English

Extent

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

Former Identifiers

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

Usage metrics

Keywords

Exports