READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking
Logic in Computer Science
2013-07-09 v1 Artificial Intelligence
Human-Computer Interaction
Abstract
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.
Keywords
Cite
@article{arxiv.1307.1944,
title = {READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking},
author = {Makarius Wenzel},
journal= {arXiv preprint arXiv:1307.1944},
year = {2013}
}
Comments
In Proceedings UITP 2012, arXiv:1307.1528