在 Coq 中形式化行编辑器
计算机科学中的逻辑
2020-06-12 v2
摘要
文本编辑器是作者——软件开发人员、书籍作者、数学家——使用的基本工具之一。文本编辑器必须按预期工作，即它应允许用户完成其工作。我们首先介绍文本编辑器的一个小子集——行编辑器。接下来，我们将给出完整文本编辑器的具体定义（规范）。之后，我们将在 Coq 中提供行编辑器的实现，然后证明它是一个完整的文本编辑器。
引用
@article{arxiv.2006.03525,
title = {Formalizing line editors in Coq},
author = {Boro Sitnikovski},
journal= {arXiv preprint arXiv:2006.03525},
year = {2020}
}
备注
"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