Workshop: Introduction to Theorem Proving with Isabelle/HOL

Details

!!! THIS IS EXACTLY THE SAME WORKSHOP AS ON NOVEMBER 4, 2019 !!!

Due to the big success of our last workshop we're bringing back the Introduction to Isabelle workshop for one more iteration, so people who couldn't make it last time have a chance to attend. If you've already taken part in the workshop in November 2019, please don't come to this one! There's an advanced course in the works right now for those who want to learn more after going through one of the introduction workshops. Further news soon to follow.

But now for the description of this event:

Did you ever want to write *correct* code? Welcome to the world of proving your code correct with Isabelle/HOL. Bring your laptop! We start out with some basic functional programming, implementing a list. Then, we will show properties about our code. In particular, we will show that reversing a list twice gives back the original list.

Are you willing to spend some hours reversing a list twice? Be warned that Isabelle/HOL has a very steep learning curve. Also, be warned that -- once you feel comfortable -- theorem proving is highly addictive.

You will NEED to bring a laptop with at least 8G of RAM and Isabelle installed. You can get Isabelle here: https://isabelle.in.tum.de/

Language: English and German

Speaker: Cornelius Diekmann

Duration: about 4h (!!)

This workshop is limited to 40 people. If you can't make it, please be sure to update your RSVP as soon as possible, especially if there's a waitlist.

!!! This is a Google hosted event. We need real names for attendees so we can ensure entry to Google premises. Please fill out this form even if you were waitlisted: https://forms.gle/A6Fcsw3XyFpznHJE6 !!!

There will be snacks :-)

You will NEED to bring a laptop with at least 8G of RAM and Isabelle installed. You can get Isabelle here: https://isabelle.in.tum.de/

Photo by Simon Lackerbauer.