Friday 4 November 2016, 10:30: Towards Hybrid Theorem Proving Interfaces, Emilio Jesús Gallego Arias (Mines ParisTech).

Abstract. (Joint work with B. Pin and P. Jouvelot.)

We will present recent work in jsCoq, a port of the Coq proof assistant to the HTML5 platform, and SerAPI, a low-level interface for Coq based on automatic datatype serialization.

jsCoq aims to enrich regular documents --- such as math proofs, books, or teaching material --- with interactive theorem proving capabilities.

jsCoq provides a self-contained, complete Coq system that can be run in the browser, without external components or servers. The idea is to distribute the Coq environment and libraries with the document, avoiding painful installation and compatibility problems. Popular Coq teaching texts are supported, as well as many popular third party libraries. Running two different Coq versions is as easy as opening two browser tabs.

The current working prototype(s) can be accessed at https://github.com/ejgallego/jscoq; note that they still are in heavy development.

The new browser environment provides a rich set of JavaScript libraries and API that allow for new modes of document navigation and display, however, we quickly hit some limitations of the current Coq architecture --- still mainly targeted at console display.

In order to overcome this limitation, and based in our experience implementing the first version of jsCoq, we have developed, SerAPI, a new Coq protocol for UIs based on serialization. SerAPI is at the core of the second version of jsCoq, and intends to provide general advanced UI support to interested Coq IDEs.