Efficient parallel programming in Poly/ML and Isabelle/ML
David C. J. Matthews, Makarius Wenzel · 2010
The ML family of languages and LCF-style interactive theorem proving have been closely related from their beginnings about 30 years ago. Here we report on a recent project to adapt both the Poly/ML compiler and the Isabelle theorem prover to current multicore hardware. Checking theories and proofs in typical Isabelle application takes minutes or hours, and users expect to make efficient use of "home machines" with 2-8 cores, or more.