[Club2] Reminder: Bachelor thesis talk by Christoph Traut today, Wed., March 5, 13:30, Room: Turing (01.11.018)

[Andrei Popescu]

On Thursday, February 27, 2014 1:08 PM, Andrei Popescu <uuomul at yahoo.com> wrote:
 
Dear All,  

The coming Wednesday, Lars Noschinski's student Christoph Traut will give his Bachelor 
thesis talk on extending Isabelle's subst method.  Please note the time: half an 
hour earlier than usually.   
 
Cheers, 
  Andrei 


Pattern-Based Subterm Selection in Isabelle
Christoph Traut
======================================================================
Wed., March 5, 13:30, Room: Turing (01.11.018)


This thesis describes how the subst proof method of the interactive
theorem prover Isabelle was extended with a simple pattern language, 
that allows users to describe subterms in a robust and intuitive way. 
This work was greatly influenced by the language of patterns described 
by Gonthier and Tassi in [3, A language of patterns
 for subterm selection] 
for the SSREFLECT proof shell extension of the Coq system. Also,
based on these patterns, an option to perform instantiations in the 
rewrite rule during substitution was added.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20140305/d0b26b94/attachment.html>