Logika i teoria typów
Informacje ogólne
Kod przedmiotu: | 1000-2M13LTT |
Kod Erasmus / ISCED: |
11.3
|
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 Przedmioty obieralne na studiach drugiego stopnia na kierunku bioinformatyka |
Strona przedmiotu: | http://www.mimuw.edu.pl/~urzy/LTT |
Punkty ECTS i inne: |
6.00
|
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 (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 8 stycznia 2023. 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. |
Zajęcia w cyklu "Semestr zimowy 2022/23" (zakończony)
Okres: | 2022-10-01 - 2023-01-29 |
![]() |
Typ zajęć: |
Ćwiczenia, 30 godzin
Wykład, 30 godzin
|
|
Koordynatorzy: | Paweł Urzyczyn | |
Prowadzący grup: | Paweł Urzyczyn, Daria Walukiewicz-Chrząszcz | |
Lista studentów: | (nie masz dostępu) | |
Zaliczenie: | Egzamin | |
Uwagi: |
Wykład będzie odbywać się zdalnie, a ćwiczenia stacjonarnie. |
Właścicielem praw autorskich jest Uniwersytet Warszawski.