Oferta dydaktyczna Instytutu Informatyki

Poniższa lista przedstawia przedmioty, które są uczone w Instytucie Informatyki, niektóre z nich co roku, niektóre z mniejszą częstotliwością Każdy student Instytutu Informatyki studiuje wg indywidualnego toku studiów, wybierając (zgodnie z pewnymi zasadami) z tej listy swoje przedmioty.

Jeżeli zastanawiasz się nad studiami u nas, jeżeli chcesz wiedzieć, czy na Uniwersytecie można zostać inżynierem, jeżeli interesuje Cię 1000 zł stypendium miesięcznie - zapraszamy na naszą stronę główną

Logika i weryfikacja

Nazwa angielska (title in English): Logic and Verification
Prowadzący (lecturer): Hans de Nivelle
Liczba punktów (ECTS): 9
Liczba punktów 2007 (ECTS since 2007): 6
Rodzaj (type): zaawansowany
Rodzaj od 2007 (type since 2007): informatyczny.I2
Liczba godzin (hours in semester):
wykład:30
ćwiczenia+pracownia:30
Egzamin (exam): tak
Możliwe zajęcia w języku angielskim (can be taught in English): tak
Przedmiot zostal uaktualniony na biezacy rok (updated): nie
Semestr (semester): letni

Wymagania (prerequisites)

Opis (description)

(Course will be taught together with Malgorzata Biernacka)

First we introduce higher-order logic, after that we introduce minimal representations of higher-order logic (Church's type theory, forall-implies fragment) intuitionistic higher-order logic, and the Curry-Howard isomorphism.

Using two proof assistents (Coq, based on Curry-Howard isomorphism and intuitionistic Higher-Order Logic, and the system HOL-light, based on Church's theory theory and Higher-Order Logic) we will introduce the techniques that are needed for verifying mathematical proofs and correctness of algorithms.

During the lectures there will be demonstrations and exercises. The course ends with a bigger verification project that the student can chooose, using one of the systems.

The course will be partially taught in English, partially in Polish.

Literatura (references)

Jeżeli jesteś zainteresowany studiowaniem w naszym instytucie, zapraszamy na stronę poświęconą tegorocznej rekrutacji.

Nazwa użytkownika (user name):
Hasło (password):