READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking
This work addresses the problem of slow and rigid interaction models in interactive theorem proving systems, aiming to modernize old-school proof assistants, though it appears incremental as it builds on existing LCF traditions.
The paper tackles the sequential and synchronous nature of proof-checking in interactive theorem proving by breaking up the READ-EVAL-PRINT loop into a parallel and asynchronous model, resulting in the development of the Isabelle/Scala approach and Isabelle/jEdit Prover IDE to enable more efficient prover interaction.
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.