Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 16:00 - 17:00 at CPP - Invited Talk Chair(s): Cătălin Hriţcu

I report on a new course Verified Functional Data Structures and Algorithms taught at the Technical University Munich. The course first intoduces students to interactive theorem proving with the Isabelle proof assistant. Then it covers a range of standard data structures, in particular search trees and priority queues: it is shown how to express these data structures functionally and how to reason about their correctness and running time in Isabelle.

Sun 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:00
Invited TalkCPP at CPP
Chair(s): Cătălin Hriţcu MPI-SP

Streamed session: https://youtu.be/PAxUO84tUE8

Invited Talk: Teaching Algorithms and Data Structures with a Proof Assistant
Tobias Nipkow Technische Universität München
Media Attached File Attached