Courses – Fakultet tehničkih nauka u Novom Sadu

Subject: Introduction to interactive theorem provers (17.0M513)

Native organizations units: Department of Fundamentals Sciences

Type of studies	Title
Master Academic Studies	Mathematics in Engineering (Year: 1, Semester: Summer)
Master Academic Studies	Information Engineering (Year: 1, Semester: Summer)
Master Academic Studies	Information and Analytics Engineering (Year: 1, Semester: Summer)

General information:

Category	Professional-applicative
Scientific or art field	Teorijska i primenjena matematika
ECTS	5

Gaining knowledge and practical work with interactive theorem provers Coq, ISABELL / HOL. Involving in scientific research.

Knowledge about fundamental notions and results in the field of functional programming languages theorem proofs. Participating in research in the particular aspect of the subject area, based on student`s interests and in cooperation with researchers in the country 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. 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
B. Pierece: Software Foundation	Software Foundation	2004	(online http://www.cis.upenn.edu/~bcpierce/sf/)	English
L. C. Paulson, Isabelle:	A Generic Theorem Prover	1994	Springer-Verlag, Berlin	English
The COQ Proof Assitant	:	2018	(online http://coq.inria.fr/)	English