Registreerumine: Kursusele registreerumiseks deklarareerida selle kuulamine vastavalt kehtivale korrale dekanaadis, kuid saata ka meil Tarmo Uustalule. Tähtaeg: 5.9.2003.
Tunde: kokku 16, sh loenguid 8, harjutusi 4, praktikume 4
Tunniplaan: loengud/harjutused neljal päeval - E 8.9., K 10.9., R 12.9., E 15.9.2003 - 14.00-16.30 Küberneetika Majas ruum B101.
Eksam: Eksamihinde saamiseks tuleb lahendada suurem komplekt koduülesandeid. Tähtaeg: E 6.10.2003.
Kontakt: Tarmo Uustalu, firstname(at)cs.ioc.ee, (0) 620 4250
Martin-Löf's Type Theory is a constructive alternative to conventional Set Theory as a foundation of reasoning. It is at the same time a logical language and a programming language, using the identifications
Proofs = Programs
Propositions = Types
Type Theory is highly relevant for Computer Science since it offers precisely the right language to talk about constructions such as programs and the appropriate structuring mechanisms. Reasoning within Type Theory is supported by implementations of proof assistants realizing different flavours of Type Theory such as Alfa, Coq, LEGO and NUPRL. Type Theory not only provides an integrated logic to reason about ordinary programs it also offers an interesting novel programming paradigm witnessed by prototypical languages such as DML, Cayenne and Epigram.
The course gives an introduction to the basic concepts of Type Theory and will introduce tools for formal reasoning such as tutch (tutorial proof checker) and LEGO. We plan to cover the following topics: