响应式Web界面的证明助手体系结构的原型实现及其关键特性

理论计算机科学电子笔记174（2007）49-61www.elsevier.com/locate/entcs校对助理Cezary Kaliszyk1Radboud University Nijmegen，荷兰摘要本文描述了一种为证明助手创建响应式Web界面的体系结构。该体系结构将当前的web开发技术与本地证明器接口的功能相结合，创建一个完全在Web浏览器中可用的界面，但类似于本地界面。提出的解决方案的安全性，可用性和效率问题进行了描述。提出了根据我们的架构创建的Coq证明助手[8]的Web接口的原型实现。 可在www.example.com上http://hair-dryer.cs.ru.nl:1024/。关键词：Proof Assistant，接口，Web，Coq，异步DOM修改1介绍1.1动机现在人们越来越习惯于一直连接到互联网。 因此，网络成为人们使用的计算机的一部分。因此，出现了一种趋势，即仅通过访问某些网页就可以提供服务。这样，人们就不再需要在自己的计算机上安装此类服务的软件。例子包括电子邮件、日历、聊天客户端、文字处理器和地图的商业服务通常通过网络接口提供。另一方面，在科学领域，例子并不多。 特别是在 并没有真正实现证明助手的Web接口要使用证明助手，需要安装一些软件。安装过程通常很复杂。例如，要在Linux系统上安装Isabelle [17]，这是最流行的证明助手之一，需要一个特定版本的 PolyML ， 一 个 HOL 堆 和 Isabelle 本 身 。 要 使 用 接 口 访 问 证 明 程 序 ， 需 要ProofGeneral [4]和支持的Emacs版本之一与1电子邮件：cek@cs.ru.nl1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.02150C. Kaliszyk/Electronic Notes in Theoretical Computer Science 174（2007）49Debian我们不得不降级Linux内核以支持PolyML。上面描述的过程已经很复杂了，更不用说其他操作系统和架构，额外的理想补丁和库，或者不太常用的证明器。这是一个问题。碰巧的是，计算机科学家更喜欢使用已安装的旧版本的证明器，而不是通过相同的过程进行升级。数学家甚至可能远离计算机辅助证明，只是因为安装的复杂性。我们希望有一个快速的界面，这是只提供一个Web浏览器. 我们想以统一的方式访问各种证明助手及其版本，而无需安装任何东西，甚至无需插件。接口的外观和行为应该像本地接口一样，以证明助手。我们希望有可能创建网页，显示教程和证明，但这是绑定到证明本身，在那里用户可以与真正的系统进行交互。服务器的提供商可能会安装修补版本的证明器，允许用户以简单的方式尝试其功能。我们希望证明助手的库可以集中使用，这样想要查看它们的用户就不需要下载或安装任何东西。这个接口应该允许以类似维基的方式集中1.2我们的方法该解决方案是一个客户端-服务器架构，具有由浏览器解释的最小轻量级客户端、专用HTTP服务器和它们之间基于HTTP的后台通信。我们架构的关键元素是异步DOM修改技术（有时称为AJAX-异步-异步JavaScript和XML或Web应用程序）。 客户端部分在服务器上，当用户访问界面页面时，它被浏览器下载，浏览器能够解释它而无需任何安装。当在服务器上完成修改时，使用浏览器访问接口的用户不需要做任何事情。 每次用户访问证明程序时，都使用服务器上当前安装的证明程序版本。用户可以访问安装在服务器上的任何证明器，即使是在进行连接的平台上不工作将文件保存在中央服务器上允许从任何位置访问它们，只需通过网络浏览器访问界面页面。中央存储库简化了证明开发中的合作，通过类似维基的机制取代CVS等版本控制系统，其中保留远程和本地副本，其中唯一的副本是远程副本。我们的方法是作为一个架构来创建Web接口证明助理，但它并不限于他们。所解决的问题与创建具有状态的Web界面程序有关，包括撤销机制，并且它们的界面可以面向用户。我们的体系结构可以应用于例如面向buffer的编程语言，如Epigram[15]。C. Kaliszyk/Electronic Notes in Theoretical Computer Science 174（2007）49511.3相关工作已经有一些提供远程访问证明器的实验。它们都不允许在不安装额外软件的情况下进行有效访问LogiCoq [18]是Coq [8]的Web接口。它提供了一个窗口，可以在其中插入整个Coq buffer的内容并提交它们进行验证。它用标准HTTP请求发送整个缓冲器并刷新整个页面。因此，人们可以有效地工作，只有微小的证据。Omega系统的Web界面[7]需要在用户的机器上安装Mozart解释器。Web浏览器的使用是最小的，整个界面是用Mozart编写的。Mozart的安装仅适用于某些平台，这也使得解决方案受到限制。有一些Java小程序具有内置的证明助手功能。示例可能包括G4IP [19]或逻辑网关[12]。在Unix环境中安装浏览器插件以支持Java并不简单，并且将证明程序限制为Java小程序是不可取的。与证明助手相关的Web界面， WEB值得一提。特别是• Helm [3]-（Hypertextual Electronic Library of Mathematics）一个网络界面，允许证明助手可视化可用的库• Whelp [2] -基于内容的搜索引擎，用于在证明助手库中查找定理，支持需要匹配和/或键入的查询• ActiveMath [16] -一个基于Web的数学学习框架，使用Java小程序与使用OMDoc的中央服务器进行通信[13]。有一些商业Web接口和框架在非科学领域使用异步DOM修改我们的架构与现有的网络接口定理证明器的新颖之处在于，它允许创建一个接口的证明器，它可以看起来和行为非常像那些由国家的最先进的本地接口，但可以通过访问一个网页浏览器，而无需安装任何额外的软件，甚至没有插件。由于这种架构，用于传输信息的网络不会减慢交互速度。使用异步DOM修改来创建证明助手接口的想法以前从未被应用过。1.4内容在本文的其余部分，我们介绍了创建Web界面的技术，我们将使用（第2节）和内部的本地证明接口，我们试图模仿（第3节），其次是介绍新的架构（第4节）和描述其安全性和有效性（第5节）。 我们提出了我们的实现原型（第6节）。最后，我们总结并提出了未来工作的愿景（第7节）。52C. Kaliszyk/Electronic Notes in Theoretical Computer Science 174（2007）492异步DOM调制的概念随着网络变得越来越普遍，网页设计师和浏览器实现者为网页添加了新的功能。文本文件已被替换超链接文件，后来包括图像，语言特定和数学字符，样式和动态元素。W3C联盟是负责Web标准化的组织，它定义了这些元素作为标准，因此它们在所有浏览器中以类似的方式实现。自90年代后期以来，浏览器已经开始支持与我们的研究相关的以下技术：JavaScript，DOM [14]和XmlHttp [20]。 近年来，这三种技术的结合使用变得越来越流行，因为它们允许创建响应式Web界面。在本文档中，我们将这三种技术的组合使用称为 人们可以找到描述这种技术的其他名称，如AJAX或Web应用程序。JavaScript是一种脚本编程语言，由Netscape于1995年创建，用于向用HTML编写的页面添加某些动态功能。它已被大多数浏览器迅速采用，现在甚至被一些文本模式浏览器（如w3m和Links）以及手机浏览器支持。 它经常在互联网网站上使用。DOM（文档对象模型）[14]是一个API（应用程序编程接口），用于管理HTML和XML文档，允许修改其结构和内容。最新的浏览器支持通过JavaScript实现的W3CDOM可访问性。它通常用于在网页上添加动态元素，例如下拉菜单或当鼠标移动时会发生变化的图像。XmlHttp [20]是一种可由Web浏览器脚本语言访问的API，用于在Web服务器之间传输数据。它在内部使用HTTP请求。XmlHttp请求在Web浏览器用户不知情的情况下发送到服务器。对于每个XmlHttp请求，都必须提供一个回调，以便在接收到来自服务器的响应时执行。请求的发送可以可选地是异步的。XmlHttp已经在大多数浏览器中可用了一段时间，并且最近在W3C规范草案中进行了描述异步DOM修改是一种Web开发技术，它使用上述三种技术来创建响应式Web界面。这样的界面是网页，其中特定事件（按键和鼠标移动）由JavaScript事件捕获。用JavaScript编码的最小客户端部分处理本地事件，如菜单打开或在缓冲区中键入。需要来自服务器的附加信息的事件在异步XmlHttp请求中发送。由于请求是在后台完成的，因此不会中断用户在本地的工作。 当响应到达时，它被用来修改绘图页上.与传统的网页相比，使用异步DOM调制可以向服务器发送最少的信息，只接收所需的信息，并刷新网页的一小部分网络C. Kaliszyk/Electronic Notes in Theoretical Computer Science 174（2007）4953开销和页面刷新被最小化，从而创建比经典的基于web的界面快许多倍的界面。这样，如果网络延迟是合理的，则接口可以非常类似于本地接口。在高网络延迟的情况下，异步请求允许用户在本地工作，同时请求额外的数据。使用异步DOM修改的例子有：在单个页面内操作的webmail和日历，在拖动时下载所需部分的地图，以及web聊天客户端。所有标准的网络浏览器都支持这种网络界面，特别是所有基于Gecko的浏览器，Microsoft Internet Explorer版本5，Opera版本8，Konqueror版本3.2，Safari版本1.2，甚至Nokia S60浏览器版本3。文本模式浏览器和视障人士浏览器3Proof Assistant在 本 节 中 ， 我 们 将 描 述 证 明 助 手 的 本 地 接 口 的 内 部 结 构 。 我 们 选 择 这 个ProofGeneral [4]有两个原因。首先，它是一个独立于证明者的证明助手接口。 第二，它是受欢迎的，因为它是普遍的，因为它是建立在高度可配置的Emacs文本编辑器上的。ProofGeneral的界面为用户提供了两个缓冲器：包含证明脚本的可编辑缓冲器和证明器状态缓冲器。ProofGeneral依赖于证明助手来递增地处理命令。它不区分策略模式证明和声明模式证明。状态改变和非状态改变的Coq命令被区分开，以使证明脚本仅具有相关部分并允许查询。界面根据上述区别为关键字着色，并使用背景色标记部分业务流程，以指示状态的验证。可能的状态包括：已被证明者接受的表达式，正在被验证的表达式，以及可编辑的非验证表达式。ProofGeneral提供了一个证明回复机制。证明器本身必须提供撤销机制。用户可以选择一个点在bumper去，和ProofGeneral问题的证明步骤和撤销步骤，以证明，才能达到这个程度ProofGeneral负责从光盘上的文件中提供校样脚本 向证明者证明并拯救布泽尔州 其他磁盘操作存在于某些证明器中，如证明编译，程序提取或自动创建文档，ProofGeneral不处理。当前版本的ProofGeneral主要是用Emacs Lisp实现的，与编辑本身紧密相连。通过设置一些变量，可以很容易地使ProofGeneral适应新的证明助手。 如果这还不够，ELisp代码可以被利用其他接口的证明或基本类似的功能。在某些界面中，如PCoq [1]或IsaWin，可以使用额外的可视化机制，例如术语注释。其中一些机制在ProofGeneral中不可用54C. Kaliszyk/Electronic Notes in Theoretical Computer Science 174（2007）49Web浏览器JavaScriptWeb服务器用户用户用户用户XmlHttp回调Dom按键和点击提交页面接口的用户这个限制来自Emacs编辑器。4一般架构我们的架构的两个核心元素是：一个专门的Web服务器和一个通信机制（图1）。①的人。Fig. 1. 总体架构。Web服务器提供普通文件，并能够响应特殊的HTTP请求（见4.2）。主界面在服务器上是一个普通的HTML文件。当用户使用浏览器访问页面时，页面需要某些JavaScript文件，然后由浏览器下载和解释。这是客户端部分。客户端部分和服务器之间的通信是通过第2节中描述的机制完成的。HTTP请求在后台创建。 结果用于就地更新页面。只有少量的信息在客户端和服务器之间传输。传输是异步完成的，使接口具有响应性。4.1客户机部分客户端部分生成一个网页，该网页最初向用户呈现一个可编辑的缓冲区和一个空的响应缓冲区。（菜单或工具栏也是必要的，C. Kaliszyk/Electronic Notes in Theoretical Computer Science 174（2007）4955交互，但它们是网页的正常元素）。Buffer是以HTML IFrames2实现的。所有修改IFrame的键都被指定给一个特殊的功能。通过在此函数中不允许更改缓冲器的锁定部分来实现缓冲器当用户想要验证缓冲器的一部分时，这一部分被锁定并发送到服务器。由于该请求是后台请求，因此即使需要一段时间，用户也可以继续工作。当响应到达时，两个缓冲器的内容被修改。响应可能是成功的，然后可编辑缓冲器的部分被标记为“已验证”，并且响应缓冲器显示新的证明器状态。 如果 命令失败，可编辑缓冲器的部分被解锁，并显示错误。 可编辑缓冲器的部分在其状态更改时使用背景颜色进行标记，就像在ProofGeneral中所做该接口包括一个证明重放机制，其创建方式与在本地接口中完成的方式类似。当用户想去商店的某个地方时，这个信息会被传递到服务器。服务器将命令发送到客户端的prover会话，并将结果通知接口。以类似的方式，接口包括一个中断机制，允许停止证明器界面包括文件交互功能。文件可以在服务器上加载和保存。为了实现互操作性，可以提供从本地计算机下载文件和上传文件。为了证明开发效率，可以提供模板和查询4.2服务器部分服务器包括标准HTTP文件服务功能。使用它，用户的浏览器下载客户端部分。服务器还可以处理已登录的用户可用的特殊消息。会话机制用于支持多个客户端。会话是在用户登录系统时创建的，并通过cookie机制维持。每个用户的会话都与特定的证明器会话相关联。服务器将证明器作为子进程运行，并通过标准输入和输出与它们通信。 证明会话在长时间不活动后终止（如果用户没有关闭页面，则客户端部分可以从头重放证明脚本上面提到的特殊消息包括：将一个给定的完整表达式传递给证明器进行验证，在证明器中发出一个撤销命令，保存一个文件，加载一个文件，以及中断（停止证明器计算）。 来自客户端的命令首先被传递给服务器，服务器将其传输证明者服务器会分析证明者的回复，只有状态更改才会发送给客户端。 状态变化包括两个部分：标记的变化编辑部和证明人状态部的新内容来自服务器的回复以异步方式传递回客户端。这意味着，服务器不会立即响应来自客户端的HTTP请求。2IFrame是一个HTML标签，它在页面中包含一个浮动框架，可以选择编辑。56C. Kaliszyk/Electronic Notes in Theoretical Computer Science 174（2007）49但是当接收到来自证明器的应答或者达到超时时。服务器保存一个被要求处理数据的证明器池，并等待来自其中任何一个的回答。 等待进程不会阻塞服务器，即可以同时处理其他客户5安全性和效率5.1用户侧用户运行的所有代码都在Web浏览器中解释。因此，恶意或病毒感染的证明者只能通过利用系统或浏览器错误来攻击客户端。用户端代码执行的效率我们的实验表明，使用Internet Explorer进行客户端DOM更改的速度大约是使用Mozilla Firefox的两倍（通常用户仍然看不到）。 很难说这是由于Internet Explorer中的安全检查较少还是呈现页面的质量较差（没有抗锯齿）5.2服务器端在任何集中式环境中，服务器的安全性、可用性和效率都很重要。标准的安全措施包括备份服务器，以备在主服务器发生故障时接管网络传输，并定期备份 用户文件。在本小节中，我们将只描述运行Web接口的服务器所特有的问题和解决方案。出现了三种问题：资源的安全性、可用性和平等共享。首先，利用我们架构中的漏洞可能会导致黑客控制服务器。其次，在集中式环境中，文件的唯一副本位于服务器上。服务器的不可用使用户不仅无法工作，而且无法访问他们的文件。 最后，当用户访问同一服务器时，其资源是共享的。 如果一个特定的证明器使用了所有的内存或CPU，其他用户将无法工作。为了提供安全性，服务器以非特权用户的身份在chroot3权限仅包括读取服务器文件和执行prover。 每个证明器类型都作为不同的用户运行（使用文件setuid机制），该机制仅具有对证明者的库的读权限，并且仅具有到存储证明者的证明脚本的目录。为了不允许存储过多的数据，可以使用文件配额对于允许系统交互的证明器，有时可以禁用此功能。特别是，对于基于ML的证明器，可以禁用下降到顶层。 如果服务器管理员不信任证明器的实现，可以使用内核的安全版本来禁用不相关的系统调用。在3chroot是一个系统调用，防止进程访问特殊根目录之外的任何文件。C. Kaliszyk/Electronic Notes in Theoretical Computer Science 174（2007）4957在这种情况下，即使是在ML内部实现的语言也可以在不改变证明器本身的情况下使用。为了确保资源的平等共享，可以使用CPU配额和内存配额机制运行证明程序进程。可以更改调度策略（例如，使用nice系统调用），以使服务器进程优先于证明器进程。不同的证明器具有不同的CPU和内存要求，在设置限制时应考虑当许多用户想要访问接口时，单个服务器的资源可能不充足。在一组机器上运行服务器很简单，通过ssh在不同的计算机上调用作为子进程的证明器。可以实现负载平衡机制。服务器部分和客户端部分之间的通信可以通过HTTPS提供接口6原型的实现我们已经实现了一个Web界面的最小原型，它遵循所提出的架构。 该接口允许使用Coq证明助手[8]，一个网络浏览器，但它的外观和行为（图2）都像CoqIde开发的浏览器 的ProofGeneral。图二.原型的屏幕截图，显示使用Coq证明。编辑的验证部分布泽尔是彩色的，而且是锁着的。状态缓冲器显示证明的状态，没有Coq警告。58C. Kaliszyk/Electronic Notes in Theoretical Computer Science 174（2007）49我们的服务器是一个400行的OCaml程序，它提供两个HTML文件和一些JavaScript文件。它还支持特殊的POST请求，用于验证和撤消命令以及加载和保存文件。它使用OCamlHttpd库来实现Web服务器功能。我们的客户端包含10KB的JavaScript和2KB的HTML。大多数客户端代码负责锁定缓冲器和识别Coq表达式。为了保护我们的原型，服务器在一个最小的chroot环境中运行。证明器子进程不应干扰主服务器进程。从Coq到OCaml顶层的下降被禁用。对接口的访问受密码保护，以避免为网络蜘蛛创建证明器会话网络蜘蛛只能看到保存的证明脚本。我们的原型包括一个1kB的文件，它应该创建一个统一的层，与不同的浏览器一起工作。我们还没有使它像异步DOM修改那样通用。特别是我们的原型与基于Gecko的浏览器（Mozilla，Firefox，Galeon，. . .）.它与Internet Explorer 6和Opera 9一起工作，缺少一些键绑定（这些浏览器将它们分配给内部函数）。它还不适用于基于KHTML的浏览器（Konqueror，Safari）和上述的旧版本我们已经测试了我们的实现虽然很难客观地衡量对用户行为的响应性，但我们的实验表明，在合理的网络延迟下，其响应性非常好。原型是一个Coq Web接口，但没有太多专门针对Coq的代码。 客户端部分包括对Coq注释和完整表达式的识别 发送。 服务器部分包括识别成功和失败，以及撤销机制对于来自ProofGeneral的所有ELisp代码，可以提供等效的JavaScript正则表达式处理。 因此，使这三件事适应其他证明器应该很简单，这就是为什么我们相信根据我们的架构实现一个支持不同证明器的接口可以很容易地完成。客 户 端 部 分 必 须 克 服 浏 览 器 之 间 的 小 差 异 。 特 别 是 ， 它 包 括 为XmlHttpRequest创建、事件绑定和DOM创建统一层的函数，这些函数在所有当前支持的浏览器上都以相同的方式工作。6.1可能的用途我们的界面可以用来创建交互式教程呈现证明助手。我们已经创建了一个特殊的证明脚本，其中包括一个稍微修改过的官方Coq教程版本。描述性的部分已经被放在注释中（包括HTML格式），并且对校对助手的命令已经被 留下了评论。 进入这样一个页面的用户可以只阅读教程并在Coq环境中执行命令，但也可以用它做自己的实验。使用策略的重要证明脚本在没有中间层的情况下C. Kaliszyk/Electronic Notes in Theoretical Computer Science 174（2007）4959证 明 国家 。 因 此 ， 在 网 络上 呈 现 的 证 明通 常 伴 随 着一 些 通 常 由 Coqdoc或TeXmacs自动生成的证明状态。 可以使用Web界面（即使在只读模式下）交互式地呈现这样的证明。通过这种方式，阅读校样的用户选择要查看的校样状态。服务器上可以包含外部校样助理库在我们的服务器中，我们包含了C-CoRN（Nijmegen的Constructive Coq Repository）[10]。这种许可证可以在服务器上开发在这种方法中，访问者总是可以看到和测试当前版本，而无需下载和编译库。改进和实验版本的证明器通常需要修补证明助手源代码的特定版本。在给定的基础设施下，向其他人展示这样一个修改后的版本是很容易的。服务器版本包括Coq的声明性证明语言扩展[9]。7结论我们提出了一个架构来创建简单，轻量级和快速的Web界面 证明助手。这样的接口在该领域是一个新事物。 我们的解决方案可与现代Web浏览器配合使用，无需安装任何额外的软件。安装和更新过程仅在服务器上完成，用户不需要 做任何事它是完全独立于平台通信机制使网络的使用最小化，从而使接口能够响应本地接口。与其他客户端-服务器解决方案相比，唯一的限制是对Web浏览器的依赖。幸运的是，Web浏览器包括完整的脚本语言，允许在客户端实现几乎所有可能的接口功能。特别是浏览器的内部编辑器与本地编辑器相比很弱。 可以在JavaScript中实现对更多键绑定的处理， 编辑器类似于本地编辑器。大多数用于证明助手的最先进的本地接口的特性都可以通过这种方式模仿。 实现的编辑器的效率在JavaScript中，将依赖于浏览器对它的解释。我们还不能找到这样的编辑。我们认为，一个集中的环境，通过Web界面访问的证明，是不受限制的本地接口相比，我们提出的架构是在计算机科学的发展趋势的精神。7.1今后工作我们的主要重点是将建议的架构扩展为一个完整的类似wiki的架构。这需要一个版本控制机制和在服务器上合并用户的更改。此外，证据显示和搜索机制是强制性的。编辑冲突可以用类似于维基软件的方式解决。例如，如果文件被更改，用户希望保存它，则会显示差异。60C. Kaliszyk/Electronic Notes in Theoretical Computer Science 174（2007）49我们想看看我们的解决方案与通用证明者交互协议PGIP [5]的匹配程度该协议是基于XML的，因此它的一部分甚至可以由服务器直接传递给浏览器，因为浏览器已经能够解析XML。另一方面，协议可能包含太多的信息，因为它被设计为作为一个本地人。最后，我们想创建一个实现，其中包括我们提出的架构的所有功能。想法包括：提供其他证明器，使其与支持异步DOM修改的所有浏览器兼容，实现break机制，自动编译Coq文件，添加语法突出显示，并提供更好的安全性。引用[1] Amerkad，A.，Y.贝尔托湖Pottier和L. Rideau，PCoq中的数学和证明演示，Rapport de Recherche 4313，Inria，Sophia Antipolis（2001）。[2] Alberti，A.，F. 圭迪角S.科恩，E。Tassi和S. Zacchiroli，一个基于内容的数学搜索引擎：Whelp。，in ： J.- C.Filli ， C.Paulin-Mohring 和 B.Werner， 编 辑 ， TYPE S ， LectureNotesinComputerScience3839（2004），pp. 17http://www.bononia.it/ -32，URL：www.example.com[3] Alberti，A.，L. 帕多瓦尼角S. 科恩和我。Schena，Helm和语义数学网。，在：R. J. Boulton和P.B.Jackson，editors，TPHOLs，Lecture Notes in Computer Science2152（2001），pp.59http://helm.cs.unibo.it/smweb.ps.gz。[4] 阿斯皮纳尔，D.， Proof General：一个用于开发证据的通用工具。，in：S.Graf和M.I. Schwartzbach，编辑，TACAS，计算机科学讲义1785（2000），pp.38比42[5] 阿斯皮纳尔，D.，C.LuéthandD.Winterstein，一种用于交互式编程的框架，in：D. Aspinall，editor，Proceedings of the ETAPS-05 Workshop on User Interfaces for Theorem Provers（ETAPS-05），Edinburgh，2005，p. 十五岁，网址：http://proofgeneral.inf.ed.ac.uk/Kit/docs/pgipimp.pdf网站。[6] Audebaud，P.和L.Rideau，Texmacs作为正式开发的创作工具。，Electr.注意Theor。Comput. Sci. 103（2004），pp.27比48[7] Benzm uüller ，C.，L. Cheikhrouhou，黑腹杜父鱼D. Fehrer，A. Fiedler，X. Huang，M. Ker ber，M.Kohlhase，K. KOnrad，A. Meier ， E. Melis ， W. Schaarschleman ， J. H. Siekmann 和 V. Sorge ， Omega ： Towards amathematical assistant。，in：W. McCune，editor，CADE，Lecture Notes in Computer Science1249（1997）. 252- 255[8] Coq开发团队，网址：http://coq.inria.fr/doc-eng.html网站。[9] Corbineau，P.，Coq的声明性证明语言（2006），URL：http://www.cs.ru.nl/，Corbineau/mmode.en.html。[10] 克鲁斯-菲利佩湖H. Geuvers和F. Wiedijk，C-CoRN，Nijmegen的建设性Coq库。，在：A. Alzheiti，G. Bancerek和A. Trybulec，editors，MKM，Lecture Notes in Computer Science3119（2004），pp.88比103[11] Davies，J.，“Wiki Brainstorming and Problems with Wiki Based Collaboration，”Master's thesis，University of York（2004）.[12] 戈特沙尔角，逻辑网关（2005），网址：http://logik.phl.univie.ac.at/chris/gateway/.[13] Kohlhase，M.，Omdoc：为数学知识的管理、分发和教学建立互联网标准。，in：J. A. Campbell和E.Roanes-Lozano，editors，AISC，Lecture Notes in Computer Science1930（2000）.32比52[14] LeHors，A.， P. 埃埃厄特湖。 哦，G。Nicol，J. Robie，M. Champion和S. Byrne，DomObjectModel（DOM）Level 3 Core Specification，Version 1，W3C Recommendation（2004）.C. Kaliszyk/Electronic Notes in Theoretical Computer Science 174（2007）4961[15] McBride ， C. ， Epigram ： 使 用 依 赖 类 型 的 实 用 编 程 。 V. Vene 和 T. Uustalu ， editors ， AdvancedFunctional Programming，Lecture Notes in Computer Science3622（2004）.130- 170[16] Melis，E.， J. Büdenbend，G. 戈瓜泽山口 Libbre cht和C. 在活动数学中学习、知识、知识的表达和管理。，Ann. 数学第内特尔38（2003），pp.47比64[17] Nipkow，T.，L. C. Paulson和M. Wenzel，[18] 波蒂尔湖，LogiCoq（1999年），网址：http://wims.unice.fr/wims/wims.cgi?模块=U3/logic/logicoq。[19] Urban ， C. ， 证 明 搜 索 在 命 令 式 编 程 语 言 pizza 中 的 实 现 。 ， in ： H.C. M. de Swart ， editor ，TABLEAUX，Lecture Notes in Computer Science1397（1998），pp.313-319[20] Web API工作组，XMLHttpRequest对象，技术报告，W3C（2006），URL：http：//www.w3.org/TR/XMLHttpRequest/网站。