Web site: arxiv.org/abs/2006.03525
Category: Office
Subcategory: Text Editors
Platform: Cross-platform
License: unknown
Interface: CLI
Wikipedia:
First release: 2020
Formal-Ed – a formalized line editor in Coq. It provides an implementation of a line editor in Coq, and then prove that it is a complete text editor.
“Collapsed” Coq code to reduce the page size, changed title from “text editors” to “line editors”.
The Rocq Prover (previously known as Coq) is an interactive theorem prover first released in 1989. It allows the expression of mathematical assertions, mechanical checking of proofs of these assertions, assists in finding formal proofs using proof automation routines and extraction of a certified program from the constructive proof of its formal specification.
