Teaching algorithms and data structures with a proof assistant (invited talk)
| Autor: | Tobias Nipkow |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
050101 languages & linguistics
Correctness Computer science Programming language 05 social sciences Proof assistant 02 engineering and technology computer.software_genre Data structure Running time Technical university ComputingMilieux_COMPUTERSANDEDUCATION 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Priority queue computer Range (computer programming) |
| Zdroj: | CPP |
| DOI: | 10.1145/3437992.3439910 |
| Popis: | We report on a new course Verified Functional Data Structures and Algorithms taught at the Technical University of Munich. The course first introduces 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|