Courses – Fakultet tehničkih nauka u Novom Sadu

Subject: Interactive theorem provers (17.DOM71)

Native organizations units: No data

Type of studies	Title
Doctoral Academic Studies	Mathematics in Engineering (Godina: 2, Winter)
Doctoral Academic Studies	Mathematics in Engineering (Godina: 1, Winter)

General information:

Category	Scientific-professional
Scientific or art field	Teorijska i primenjena matematika
Interdisciplinary	Yes
ECTS	10

Educational goal:

To acquire knowledge in theoretical foundations of interactive theorem provers. Practical work with interactive theorem provers Coq, ISABELL / HOL. Student involvement in scientific research.

Educational outcome:

Knowledge about theoretical foundations and practical work with interactive theorem proofs. Participating in research in the particular aspect of the subject area, based on student`s interests and in cooperation with researchers from the region and abroad.

Course content:

Theoretical foundations of interactive theorem provers, aka proof assistants. Basic notions of type theory. Simly typed systems. Basic definitions and properties. Confluency and normalisation porperties. Polymorphic types. The strong normalisation theorem, its proof and importance as a Goedel sentence. Dependent types. Theory of constructions (Coquand). Introduction to basic concepts of interactive theorem proving. Proof assistants: COQ and ISABELLE.

Teaching methods:

The presentation of the theoretical part during the lectures is followed by the characteristic examples which contribute to better understanding of the subject matter. The students are expected to individually study the additional literature which they discuss with the . subject teacher at the consultation classes.

Literature:

Authors	Title	Year	Publisher	Language
Nipkow, T., Paulson, L., Wenzel, M.	Isabelle/HOL : A Proof Assistant for Higher-Order Logic	2002	Springer, Berlin	English
Zoran Ognjanović, Silvia Gilezan	Teorijsko računarstvo	2018		Serbian language
Benjamin Pierce	Software Foundations	2018	https://softwarefoundations.cis.upenn.edu/current/index.html	English
COQ Team	The COQ Proof Assitant	2018	https://coq.inria.fr/	English