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

[Andrei Popescu]

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.






On Thursday, February 20, 2014 3:43 PM, Christoph Traut <trautc at in.tum.de> wrote:
 
Greetings

Since the talk is about my bachelor's thesis, title and abstract are 
pretty much the same as in my thesis.

The title is "Pattern-Based Subterm Selection in Isabelle", the abstract 
is as follows:

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 sub-
terms 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 selec-
tion] 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.


Christoph



On 18.02.2014 11:55, Lars Noschinski wrote:
> Hi Andrei,
>
> Christoph will give a talk about this Bachelor thesis on Wednesday,
> March 5, at 13:30. Estimated duration including questions is 30 minutes.
>
> @Christoph: Please send Andrei title and abstract of your talk till Friday.
>
>     -- Lars
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20140227/bfbe2fda/attachment.html>