EPFLTV - EPFL video portal

The languages of Isabelle: Isar, ML, and Scala

<a href="//www.macromedia.com/go/getflashplayer">Click to install the plugin</a>
Click on the arrow for full screen - ESC to leave (except Linux)
Makarius Wenzel sep. 10, 2009 1h0mn13s
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.
From:Fabien Salvi
Event type:Congress&Conferences
Channel:EPFL IC Tresor Talks (37)
Video type:Flash video
       icon
Video number:605
Embed this video on your web site:
URL of this video

Post a comment

Related video

illustration Compiler verification for fun and profit - 2014-10-22
illustration Challenges in Bit-Precise Reasoning - 2014-10-21
illustration Induction for SMT Solvers - 2015-01-12
illustration Model Interpretation and Compilation by Partial Evaluation - 2010-04-20
illustration Model Checking High level Petri Nets - 2010-03-05
illustration A Framework For Automatic Verification of Programming Exercises - 2010-01-08
illustration Complete Program Synthesis for Linear Arithmetics - 2010-01-27
illustration From Single-threaded to Multithreaded - 2010-01-07
illustration Automatic Inference of Synchronization - 2009-12-15
illustration Automated Termination Analysis of Programs using Dependency Pairs - 2009-10-22
illustration The languages of Isabelle: Isar, ML, and Scala - 2009-09-10
illustration TPTP, TSTP, CASC, etc. - Automated Reasoning in Practice - 2009-05-12
illustration Flyspeck II - The Basic Linear Programs - 2008-12-12
illustration An Improved Algorithm for Three-Color Parity Games - 2008-11-06
illustration Solving Parity Games in Practice - 2008-10-09