Logika i teoria typów 1000-2M13LTT
* 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
Rodzaj przedmiotu
Koordynatorzy przedmiotu
Efekty kształcenia
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.
Kryteria oceniania
Aby zaliczyć przedmiot należy zaliczyć ćwiczenia i zdać egzamin (pisemny, stacjonarny).
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..
W przypadku zaliczania przedmiotu przez doktoranta, dodatkowym
elementem zaliczenia będzie zapoznanie się z oryginalnym artykułem
naukowym i rozmowa z wykładowcą na temat tego artykułu.
Literatura
* Sorensen, M., Urzyczyn, P., Lectures on the Curry-Howard Isomorphism
* Materiały własne dostępne w sieci.
Uwagi
|
W cyklu 2024Z:
Wykład będzie odbywać się zdalnie, a ćwiczenia stacjonarnie. |
Więcej informacji
Więcej informacji o poziomie przedmiotu, roku studiów (i/lub semestrze) w którym się odbywa, o rodzaju i liczbie godzin zajęć - szukaj w planach studiów odpowiednich programów. Ten przedmiot jest związany z programami:
Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb: