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 [8] created according to our architecture is presented. Access to the prototype is available on http://hair-dryer.cs.ru.nl:1024/. Key words: Proof Assistant, Interface, Web, Coq, Asynchronous DOM modification

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Cezary Kaliszyk
• Keywords: Architecture, ENTCS 2007, Proof Assistant, Web Development Technologies