Serwisy internetowe Uniwersytetu Warszawskiego Nie jesteś zalogowany | zaloguj się
katalog przedmiotów - pomoc

Logika i teoria typów

Informacje ogólne

Kod przedmiotu: 1000-2M13LTT Kod Erasmus / ISCED: 11.3 / (0612) Database and network design and administration
Nazwa przedmiotu: Logika i teoria typów
Jednostka: Wydział Matematyki, Informatyki i Mechaniki
Grupy: Przedmioty monograficzne dla III - V roku informatyki
Przedmioty obieralne dla informatyki
Strona przedmiotu: http://www.mimuw.edu.pl/~urzy/LTT
Punkty ECTS i inne: 6.00
zobacz reguły punktacji
Język prowadzenia: angielski
Rodzaj przedmiotu:

monograficzne
Skrócony opis:

Wykład obejmie wprowadzenie do różnych systemów z typami i ich interpretacji logicznych w duchu paradygmatu ,,formuły-typy", zwanego też izomorfizmem Curry'ego-Howarda. W szczególności mowa będzie o logice intuicjonistycznej, liniowej i teorio-typowych podstawach wnioskowania wspomaganego komputerowo.
Pełny opis:

* Powtórzenie z rachunku lambda.

* Wprowadzenie do logiki intuicjonistycznej.

* Izomorfizm Curry'ego-Howarda.

* Logika jako gra dialogowa.

* Podstawy logiki liniowej.

* Logika klasyczna i sterowanie nielokalne.

* Polimorfizm.

* Typy zależne.

* Rachunek konstrukcji i jego uogólnienia (PTS).

* System Coq

* Typy indukcyjne i rekurencyjne.

* Wprowadzenie do homotopijnej teorii typów
Literatura:

* Sorensen, M., Urzyczyn, P., Lectures on the Curry-Howard Isomorphism

* Materiały własne dostępne w sieci.
Efekty uczenia się:

Wiedza:

* Zna podstawy logiki intuicjonistycznej i liniowej.

* Zna obliczeniowe interpretacje różnych logik, w tym logiki klasycznej.

* Rozróżnia paradygmaty teorio-dowodowe.

* Zna siłę wyrazu różnych rachunków z typami i wie jakim logikom odpowiadają.

* Zna podstawy systemu Coq.

Umiejętności

* Potrafi interpretować konstrukcje logiczne jako zadania obliczeniowe.

* Potrafi napisać prosty dowód w systemie Coq.

Kompetencje.

* Rozumie związki pomiędzy zjawiskami obliczeniowymi i logicznymi.

* Ma przygotowanie do samodzielnego poznawania systemów z typami

i komputerowo wspomaganego wnioskowania.
Metody i kryteria oceniania:

Aby zaliczyć przedmiot należy zaliczyć ćwiczenia i zdać egzamin.

Ocena końcowa będzie wystawiona na podstawie egzaminu.

Aby zaliczyć ćwiczenia należy koniecznie zaliczyć prace domowe. O zaliczeniu ćwiczeń decyduje prowadzący ćwiczenia.

Do egzaminu zerowego mogą przystąpić osoby, które zaliczyły prace domowe i zgłosiły gotowość do egzaminu najpóźniej 7 stycznia.

Zajęcia w cyklu "Semestr zimowy 2020/21" (zakończony)

Okres: 2020-10-01 - 2021-01-31
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Ćwiczenia, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Paweł Urzyczyn
Prowadzący grup: Paweł Urzyczyn, Daria Walukiewicz-Chrząszcz
Strona przedmiotu: https://moodle.mimuw.edu.pl/course/view.php?id=564
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin
Uwagi:

https://moodle.mimuw.edu.pl/course/view.php?id=564

Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.