Web Interfaces for Proof Assistants

This article describes an architecture for creating responsive web interfaces for proof assistants. The architecture combines current web development technologies with the functionality of local prover interfaces, to create an interface that is available completely within a web browser, but resembles and behaves like a local one. Security, availability and efficiency issues of the proposed solution are described. A prototype implementation of a web interface for the Coq proof assistant [Coq Development Team, “The Coq Proof Assistant Reference Manual Version 8.0,” INRIA-Rocquencourt (2005), URL: http://coq.inria.fr/doc-eng.html] created according to our architecture is presented. Access to the prototype is available on http://hair-dryer.cs.ru.nl:1024/.