论文标题
COQ中的正式线编辑器
Formalizing line editors in Coq
论文作者
论文摘要
文本编辑器代表了作者使用的基本工具之一 - 软件开发人员，书籍作者，数学家。文本编辑器必须按预期工作，因为它应该允许用户完成工作。我们首先引入文本编辑器的一小部分 - 行编辑器。接下来，我们将给出一个完整的文本编辑器的具体定义（规范）。之后，我们将在COQ中提供线路编辑器的实现，然后我们将证明它是一个完整的文本编辑器。
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.
