Courses – Fakultet tehničkih nauka u Novom Sadu

Subject: Interactive theorem provers (17.DOM71)

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

General information:

Category	Scientific-professional
Scientific or art field	Applied Computer Science and Informatics Teorijska i primenjena matematika
ECTS	10

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

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.

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.

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.

Authors	Title	Year	Publisher	Language
Nipkow, T., Paulson, L., Wenzel, M.	Isabelle/HOL : A Proof Assistant for Higher-Order Logic	2002	Springer, Berlin	English
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