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

TL;DR

This paper introduces a novel model for parallel and asynchronous proof-checking in interactive theorem proving, breaking the traditional sequential read-eval-print loop to improve interaction and integration.

Contribution

It presents a new approach to proof processing that enables parallel and asynchronous interaction in ITP systems, exemplified by Isabelle/Scala and Isabelle/jEdit.

Findings

Key concepts of parallel proof processing are explained.

The approach improves prover interaction and integration.

It opens discussion for non-trivial interaction models in ITP.

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.