[Club2] talk by Dan Matichuck Thursday, July 10, 13:00, Room: Turing (00.09.38)

[Andrei Popescu]

Greetings, 


On Thursday, July 10, Dan Matichuck will visit us and give a talk about Eisbach, a tactic language for Isar that he’s been developing.  Please note the unusual time and day of the week. 


Cheers, 

  Andrei 

Eisbach: An Isabelle Proof Method Language
Daniel Matichuk
======================================================================
Thu., July 10, 13:00, Room: Turing (00.09.38)

Currently, to write automation for Isabelle, end-users are required to shed the high-level view provided by Isar and learn the particulars of programming in Isabelle/ML. The cost of this context
 switch is quite high, resulting in a tendency for users to simply “deal with pain” and write proofs with obvious or duplicated logic. As proof developments become larger, the cost of this repeated reasoning grows.
In this talk I present Eisbach, an in-development extension of Isar that gives users the ability to write proof methods while maintaining a high degree of abstraction. Most notably, existing (and new) methods can be invoked within an Eisbach method, with their usual syntax. At its most basic level, Eisbach allows a combination of proof methods to be named and abstracted over terms, facts and other methods. Additional mechanisms are provided for control flow using higher order matching, as well as integration with attributes and dynamic facts. Implicit focusing provides methods with a consistent structured view of subgoals, allowing hypotheses to be referenced as if they were local facts, as well as fixing quantified
 parameters.
Surprisingly powerful methods can be written with these simple features, and their implementation can be understood by casual Isabelle users and experts alike.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20140704/2d697ac9/attachment.html>