703315 VU Logic and Learning B: Interactive Theorem Proving in Isabelle/HOL

summer semester 2022 | Last update: 09.01.2022 Place course on memo list
703315
VU Logic and Learning B: Interactive Theorem Proving in Isabelle/HOL
VU 3
5
weekly
annually
English

Understanding of interactive theorem proving; ability to specify programs and proofs in the Isabelle/HOL proof assistant; acquisition of the ability to independently educate themselves in the field.

This course provides knowledge about interactive theorem proving with a focus on the Isabelle proof assistant using higher-order logic (HOL). The following topics will be discussed:

  • higher-order logic
  • Isabelle's proof language Isar
  • natural deduction in Isabelle
  • functional programming in Isabelle
  • inductive definitions
  • code generation
  • selection of advanced topics
see dates
Group 0
Date Time Location
Thu 2022-03-10
09.15 - 12.00 rr 18 rr 18 Barrier-free
Thu 2022-03-17
09.15 - 12.00 rr 18 rr 18 Barrier-free
Thu 2022-03-24
09.15 - 12.00 rr 18 rr 18 Barrier-free
Thu 2022-03-31
09.15 - 12.00 rr 18 rr 18 Barrier-free
Thu 2022-04-07
09.15 - 12.00 rr 18 rr 18 Barrier-free
Thu 2022-04-28
09.15 - 12.00 rr 18 rr 18 Barrier-free
Thu 2022-05-05
09.15 - 12.00 rr 18 rr 18 Barrier-free
Thu 2022-05-12
09.15 - 12.00 rr 18 rr 18 Barrier-free
Thu 2022-05-19
09.15 - 12.00 rr 18 rr 18 Barrier-free
Thu 2022-06-02
09.15 - 12.00 rr 18 rr 18 Barrier-free
Thu 2022-06-09
09.15 - 12.00 rr 18 rr 18 Barrier-free
Thu 2022-06-23
09.15 - 12.00 rr 18 rr 18 Barrier-free
Thu 2022-06-30
09.15 - 12.00 rr 18 rr 18 Barrier-free