IntelliSense Integration for Coq Theorem Prover
Adam Abonyi · Digital Repository (National Repository of Grey Literature) · 2012
Computer-assisted (interactive) theorem provers are software tools that help with the development of formal proofs. While theorem provers are constantly evolving and have started to be used more often over the last decade, the development tools used for creating computer-assisted proofs have not improved as much and they do not offer features that are common to other modern development tools. This thesis aims to improve the state of the art of development tools for interactive theorem provers, namely Coq. We integrate the Coq interactive theorem prover into an existing modern development environment and bring the benefits of modern tools to interactive proving. Improving the development tools could help popularize computer-assisted theorem proving and thus improve the quality of software by simplifying formal verification and by allowing development of verified hardware.