JsCoq : Towards Hybrid Theorem Proving Interfaces

Emilio J. Gallego Arias, Benoit Pin, Pierre Jouvelot

MINES ParisTech, PSL Research University, France

2 July 2016 - Coimbra
User Interfaces for Theorem Provers

A picture is worth a thousand words
A web page is worth a million!

Typical Coq Example

Lets add some math

$$ \sum_{i = m + a}^{n-1} F(i) + \sum_{i = m}^{(n-a)-1)} F(i)$$


Accessible Theorem Proving

Interactive Theorem Proving

Problems in Education
"The Youtube Epoch"

Interactive Theorem Proving

Problems with the Platforms


A Serverless, Opinionated Project

Target a concrete user base, develop proper foundations.


What we don't want to do:

  1. Fork coq.
  2. Invent anything.
  3. Look like an IDE.
  4. Write code. Write User Interfaces.
Yet we've done a bit of all of the above.

Demo Time !

Try it yourself!

Many more developments supported, but they all (yet) look the same, we hope this changes!

We are Work-in-Progress™

How does it Work?

4 Modular Components:

The Coq Worker



The Document Provider

Document Extraction:

Document-Level Model:

The Document Manager

Responsible of the Prover-level Model.

The Panel

What's Next:

SerAPI: @github

Other Clients:

New Coq Document/Documentation Model


Open Source @ github.com/ejgallego/jscoq !