The languages of Isabelle: Isar, ML, and Scala

EPFL IC Tresor talks

by Makarius Wenzel More than 20 years ago, Isabelle was introduced by Larry Paulson as a “logical framework”, to facilitate experimentation with various calculi according to general ideas of higher-order Natural Deduction. Over time the system has widened its scope, to become a general platform for building applications based on formal logic, with fully formal proof checking by a trusted kernel. We give an overview of the Isabelle platform of 2009 from the perspective of the main languages involved: Isar (Intelligible semi-automated reasoning), Standard ML, and Scala/JVM. Isabelle/Isar is presented to end-users as a language for human-readable proofs (and specifications). It is firmly rooted on the Pure logical framework, and imposes certain policies on core inferences by means of rich extra-logical infrastructure. Thus Isar enhances the original framework of primitive proof rules towards one of structured proof texts. The concrete proof language can be seen as an application of more general principles provided internally: the greater part of the Isar language is implemented as derived elements. Further “domain specific proof languages” can be implemented as well. Isabelle/ML is both the implementation language and extension language of the framework. Isabelle follows the original “LCF-approach” (Robin Milner, 1979). This means that the key notions are modeled as abstract datatypes in ML, and users may implement extensions on top without affecting soundness. Isabelle/ML is embedded into the Isar source language such that the proof context is available at compile time. Antiquotations within ML source allow robust references to formal entities. Using Poly/ML, the baseline performance for typical symbolic computations is very good; recent moves towards multicore support improve upon this further. In Isabelle2009, both theories and proofs are scheduled in parallel by the system, with reasonable scalability for current home machines (4-8 cores). Isabelle/Scala has been recently added as a wrapper around the Isabelle/Isar/ML process. The idea is to reach out into the “real world”, as represented by the JVM platform with its existing facilities for user interfaces, web services etc. Thus we overcome the traditional TTY-based interaction with the raw ML process, replacing it by an editor-oriented proof document model with rich markup provided by the prover in the background. The existing concepts of parallel proof checking are eventually generalized towards an asynchronous interaction model that is expected to increase end-user productivity significantly. This general API for “Isabelle system programming” in Scala is used in our ongoing implementation of Isabelle/jEdit.