READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking

Makarius Wenzel

The LCF tradition of interactive theorem proving, which was started by Milner in the 1970-ies, appears to be tied to the classic READ-EVAL-PRINT-LOOP of sequential and synchronous evaluation of prover commands. We break up this loop and retrofit the read-eval-print phases into a model of parallel and asynchronous proof processing. Thus we explain some key concepts of the Isabelle/Scala approach to prover interaction and integration, and the Isabelle/jEdit Prover IDE as front-end technology. We hope to open up the scientific discussion about non-trivial interaction models for ITP systems again, and help getting other old-school proof assistants on a similar track.

In Cezary Kaliszyk and Christoph Lüth: Proceedings 10th International Workshop On User Interfaces for Theorem Provers (UITP 2012), Bremen, Germany, July 11th 2012, Electronic Proceedings in Theoretical Computer Science 118, pp. 57–71.
Published: 5th July 2013.

ArXived at: http://dx.doi.org/10.4204/EPTCS.118.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org