ProofWeb

RU SURF VU

Motivation

The initial idea came from Henk Barendregt, who envisioned a web-portal for formalization of mathematics, that would include Wiki functionality. We already had proof checkers, and libraries for them, but there were no useful web interfaces to them. Possible uses of our the interface already include:

Implementation

The system consists of a server part and a client part:

Security

Security is particularly important in a centralized approach. The current implementation already provides security by the following means:

Possible other security enhancements include cpu, memory and disc quotas, further virtualization (Xen and similar solutions) and automatic recreation of the filesystem.

Other provers

The interface has been initially created as a web interface for Coq, then for Isabelle and now includes preliminary support for Lego, Plastic, Matita and Hol Light. The functionality that is prover specific is:

In principle adapting the interface to work with a prover with which proof-general is able to work, should be straight-forward.

Ideas and suggestions (more are welcome)

Screenshots

screenshot-coq-firefox
Coq in Firefox
screenshot-lego-opera
Lego in Opera
screenshot-coq-ie
Coq in IE
screenshot-plastic-konqueror
Plastic in Konqueror