[Club2] Invitation: A refactoring tool for Isabelle/jEdit: automatic renaming... @ Wed Mar 18, 2015 14:00 - 15:00 (Club2)

[julianbrunner at gmail.com]

You have been invited to the following event.

Title: A refactoring tool for Isabelle/jEdit: automatic renaming of theorem  
and constant names in a Isabelle library
Speaker: Marcel Lotze
Type: Bachelor's Thesis Talk

Abstract:

The goal of this thesis was to explore automatic renaming of constant and  
theorem names in Isabelle/jEdit.

Isabelle/jEdit is an IDE for the automatic theorem prover Isabelle. In this  
environment, one theory is represented by one editable document that is  
split internally into commands according to the rules of the Isar language.  
These commands are given to a prover processrunning in the background and  
the prover in turn provides the IDE with various information about the  
processed commands.

Markup data provided by the prover describes entities that have been  
processed by the prover's parser and correspond to parts of the commands  
that were given to the prover, such as type names or constants. In the  
course of this thesis an extension to the Isabelle/jEdit code was developed  
that allowed to perform automated renaming of some name-space element  
definitions and references in Isabelle/Isar documents based on these entity  
descriptions.

Heuristics had to be implemented because information provided by the prover  
process is not comprehensive and unambiguous enough for an automated  
renaming feature that would never produce imperfect Isar code.
When: Wed Mar 18, 2015 14:00 - 15:00 Berlin
Where: MI 00.09.038 (Turing)
Calendar: Club2
Who:
     * Julian Brunner - creator
     * club2 at mailbroy.informatik.tu-muenchen.de
     * Marcel Lotze

Event details:  
https://www.google.com/calendar/event?action=VIEW&eid=NG1uNWxmOWIzZm1sMzllc2ZqdDF2M3BmMm8gY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWUwMTlkOThiMzE2NTg4Njk5Y2Y0NzQ0NDg0ZjBhODI5ZWYzZTA2YmE&ctz=Europe/Berlin&hl=en

Invitation from Google Calendar: https://www.google.com/calendar/

You are receiving this courtesy email at the account  
club2 at mailbroy.informatik.tu-muenchen.de because you are an attendee of  
this event.

To stop receiving future updates for this event, decline this event.  
Alternatively you can sign up for a Google account at  
https://www.google.com/calendar/ and control your notification settings for  
your entire calendar.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20150312/7b058680/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2706 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20150312/7b058680/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2761 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20150312/7b058680/attachment.bin>