[Club2] Updated Invitation: Proof Automation Tool for Isabelle/HOL @ Fri Dec 18, 2015 11:45 - 12:30 (Club2)

[julianbrunner at gmail.com]

This event has been changed.

Title: Proof Automation Tool for Isabelle/HOL
Speaker: Yutaka Nagashima from Data61 in Sydney

Abstract:

In this talk, we present our new proof automation tools for Isabelle which  
produce efficient proof-scripts if they successfully discharge given  
proof-obligations.
Our automation tools are fully embedded in Isabelle, enabling seamless  
invocation from Isabelle/jEdit.

Furthermore, we present our framework for proof automation. This framework  
allows Isabelle users to specify their own proof-search procedures  
succinctly as data structures.
"Succinctly" is the keyword here; our monadic interpretation of tactics  
makes our framework compositional and abstracts the core of framework away  
from the implementation details.

This ongoing work has already demonstrated that our approach successfully  
discharges a set of small-scale proof-obligations that could not be proved  
by the existing proof-automation tools in Isabelle.
Finally, we explain our plan to improve our automation tools and framework,  
so that our approach can solve larger-scale proof-obligations. (changed)
When: Fri Dec 18, 2015 11:45 - 12:30 Berlin (changed)
Where: MI 00.09.038 (Turing)
Calendar: Club2
Who:
     * julianbrunner at gmail.com - creator
     * club2 at mailbroy.informatik.tu-muenchen.de
     * yutaka.nagashima at nicta.com.au

Event details:  
https://www.google.com/calendar/event?action=VIEW&eid=ZG84aDlkMmpyZzQxZTlsNjFmaGw1dGJ1NGsgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTk5ZGY0YjhiZThhMzA1ODRmYmEwNmJmMGYwZjQwZTlhYmFhMjViZDk&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.

Forwarding this invitation could allow any recipient to modify your RSVP  
response. Learn more at  
https://support.google.com/calendar/answer/37135#forwarding
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20151210/0aaf4eaa/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2462 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20151210/0aaf4eaa/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2515 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20151210/0aaf4eaa/attachment.bin>