Registreerumine: Kursusele registreerumiseks deklarareerida selle kuulamine vastavalt kehtivale korrale dekanaadis, kuid saata ka meil Tarmo Uustalule. Tähtaeg: 5.9.2003.
Kood: ITT9200
Punkte: 2.0
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.
Kontrollivorm: eksam
Eksam: Eksamihinde saamiseks tuleb lahendada suurem komplekt koduülesandeid. Tähtaeg: E 6.10.2003.
Õppejõud: Thorsten Altenkirch, lecturer, School of Computer Science and Information Technology, University of Nottingham
Kontakt: Tarmo Uustalu, firstname(at)cs.ioc.ee, (0) 620 4250
Kursus toimub EITSA administreeritava riikliku programmi Tiigriülikool toel.
Thorsten Altenkirch
School of Computer Science and
Information Technology
University of Nottingham
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: