[Club2] talk by Lars Hupel: Wed., June 25, 15:00, Room: Turing (00.09.38)

[Andrei Popescu]

Dear All,  

On Wednesday at the usual time Lars will give a rehearsal talk for his accepted CICM paper.  
 
Cheers, 
  Andrei  


Interactive Simplifier Tracing and Debugging in Isabelle
Lars Hupel
======================================================================
Wed., June 25, 15:00, Room: Turing (00.09.38)

The Isabelle proof assistant comes equipped with a very powerful tactic
for term simplification. While tremendously useful, the results of
simplifying a term not always match the user's expectation: sometimes,
the resulting term is not in the form the user expected, or the
simplifier fails to apply a rule. We describe a new, interactive tracing
facility which offers insight into the hierarchical structure of the
simplification with user-defined filtering, memoization and search. The
new simplifier trace is integrated into the Isabelle/jEdit Prover IDE.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20140623/ae28add5/attachment.html>