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

summer semester 2023 | Last update: 12.01.2023 | Place course on memo list

Department:

Department of Computer Science

Instructor:

assoz. Prof. Dr. René Thiemann, +43 512 507 53234

Course number:

703315

Title:

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

Type/hours:

VU 3

ECTS credits:

Period:

weekly

Mode of repetition:

annually

Language of instruction:

English

Learning Outcome:

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.

Contents:

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

Privacy notice:

course will be recorded

OLAT:

https://lms.uibk.ac.at/url/RepositoryEntry/5373624454

Link:

http://cl-informatik.uibk.ac.at/teaching/ss23/itpIsa

Start:

see dates

allocated to study field

Faculty of Mathematics, Computer Science and Physics

Master's Programme Computer Science according to the Curriculum 2021 (120 ECTS-Credits, 4 semesters)

Elective Modules (50 ECTS-Credits)

Elective Module 7: Logic and Learning (10 ECTS-credits, 6 hours)

Sustainable development goals

SDG 4 - Quality education: Ensure inclusive and equitable quality education and promote lifelong learning opportunities for all.
SDG 9 - Industry, Innovation, and Infrastructure: Build resilient infrastructure, promote inclusive and sustainable industrialization, and foster innovation.

Dates

Group 0	Export course dates of this group as iCalendar (.ics) Help
Date	Time	Location
Thu 2023-03-09	09.15 - 12.00	rr 20 rr 20	Barrier-free
Thu 2023-03-16	09.15 - 12.00	rr 20 rr 20	Barrier-free
Thu 2023-03-23	09.15 - 12.00	rr 20 rr 20	Barrier-free
Thu 2023-03-30	09.15 - 12.00	rr 20 rr 20	Barrier-free
Thu 2023-04-20	09.15 - 12.00	rr 20 rr 20	Barrier-free
Thu 2023-04-27	09.15 - 12.00	rr 20 rr 20	Barrier-free
Thu 2023-05-04	09.15 - 12.00	rr 20 rr 20	Barrier-free
Thu 2023-05-11	09.15 - 12.00	rr 20 rr 20	Barrier-free
Thu 2023-05-25	09.15 - 12.00	rr 20 rr 20	Barrier-free
Thu 2023-06-01	09.15 - 12.00	rr 20 rr 20	Barrier-free
Thu 2023-06-15	09.15 - 12.00	rr 20 rr 20	Barrier-free
Thu 2023-06-22	09.15 - 12.00	rr 20 rr 20	Barrier-free
Thu 2023-06-29	09.15 - 12.00	rr 20 rr 20	Barrier-free