Aine eesmärk on tutvustada tüübiteooria aluseid suunatuna sõltuvate tüüpidega programmeerimisele ja programmide üle arutlemisele ning matemaatilise ja loogikalise arutelu formaliseerimisele.

The students will learn basics of type theory, aimed at programming and reasoning about programs using dependent types, and at the formalization of mathematical and logical reasoning.

Õppeaine läbinud üliõpilane:
- programmeerib iseseisvalt sõltuvate tüüpidega funktsionaalses programmeerimiskeeles;
- formaliseerib algoritme ning konstruktsioone matemaatikast ja programmeerimisteooriast, kasutades sõltuvaid tüüpe;
- rakendab loogikalisi ning tüübiteoreetilisi konstruktsioone erinevate ülesannete lahendamisel tarkvara formaalses verifitseerimises.

After completing the course the student:
- independently programs in a dependently-typed functional programming language;
- formalizes algorithms and mathematical and programming constructs using dependent types;
- applies logical and type-theoretical constructions to solve various problems in formal verification of software.

Kursus käsitleb järgmisi teemasid:
- funktsionaalne programmeerimine lihtsate ja sõltuvate tüüpidega
- loogika ja struktuurse tõestusteooria alused
- arvutatavus ja lambda-arvutus
- tõestusassistent Agda
- homotoopiline tüübiteooria

The course covers the following topics:
- functional programming with simple and dependent types
- basics of logic and structural proof theory
- lambda calculus and computability
- the proof assistant Agda
- homotopy type theory

Eristav hindamine (eksam).

Graded assessment (exam).

Artiklite lugemine

Reading articles

Samuel Mimram: Program = Proof.
Additional literature on the course web page.

-

not specified