Web Interfaces for Proof Assistants

详细信息    查看全文

• 作者：Cezary Kaliszyk
• 关键词：Proof Assistant ; Interface ; Web ; Coq ; Asynchronous DOM modification
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2007
• 出版时间：15 May 2007
• 年：2007
• 卷：174
• 期：2
• 页码：49-61
• 全文大小：407 K

文摘

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/.