[Club2] Invitation: Automatic Asymptotics in Isabelle/HOL @ Wed May 24, 2017 14:00 - 15:00 (CEST) (club2 at mailbroy.informatik.tu-muenchen.de)

[julianbrunner at gmail.com]

You have been invited to the following event.

Title: Automatic Asymptotics in Isabelle/HOL
Speaker: Manuel Eberl
Type: Rehearsal Talk

Abstract:
Isabelle/HOL is an interactive theorem prover (also called ‘proof  
assistant'); it provides a logical environment in which mathematical  
concepts can be defined and theorems about them can be proven. The system  
guides and assists the user in writing formal proofs, while every step of  
the proof is computer-checked, which minimises the possibility of mistakes.

This talk will give a brief overview of Isabelle/HOL, followed by a more  
detailed excursion into my project of bringing more tools for asymptotic  
analysis into Isabelle/HOL; in particular, this includes a procedure to  
automatically prove limits and ‘Big-O' estimates of real-valued functions  
similarly to computer algebra systems like Mathematica and Maple – but  
while proving every step of the process correct.
When: Wed May 24, 2017 14:00 – 15:00 Berlin
Where: MI 00.09.038 (Turing)
Calendar: club2 at mailbroy.informatik.tu-muenchen.de
Who:
     * Julian Brunner - creator
     * club2 at mailbroy.informatik.tu-muenchen.de

Event details:  
https://www.google.com/calendar/event?action=VIEW&eid=dmR1ZDM0ZGp2YmY5YzZpYnBxcGxvOTdqdTAgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWI4ZDE2YWJlNDNmN2Q2ODM5NmY4Y2Y1NGE4NDdmNDZlNjBmM2VkNTc&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/20170519/1ac7f0f2/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2010 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20170519/1ac7f0f2/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2055 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20170519/1ac7f0f2/attachment.bin>