Formalizing line editors in Coq
Logic in Computer Science
2020-06-12 v2
Abstract
Text editors represent one of the fundamental tools that writers use - software developers, book authors, mathematicians. A text editor must work as intended in that it should allow the users to do their job. We start by introducing a small subset of a text editor - line editor. Next, we will give a concrete definition (specification) of what a complete text editor means. Afterward, we will provide an implementation of a line editor in Coq, and then we will prove that it is a complete text editor.
Cite
@article{arxiv.2006.03525,
title = {Formalizing line editors in Coq},
author = {Boro Sitnikovski},
journal= {arXiv preprint arXiv:2006.03525},
year = {2020}
}
Comments
"Collapsed" Coq code to reduce the page size, changed title from "text editors" to "line editors". Associated files are available at https://github.com/bor0/formal-ed