Workshop: Introduction to Theorem Proving with Isabelle/HOL

Without further ado:

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/YVKH8WT6dTrAyYH56 !!!

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 Roman Mager on Unsplash.