Logika i teoria typów

Informacje ogólne

Kod przedmiotu:	1000-2M13LTT
Kod Erasmus / ISCED:	11.3 Kod klasyfikacyjny przedmiotu składa się z trzech do pięciu cyfr, przy czym trzy pierwsze oznaczają klasyfikację dziedziny wg. Listy kodów dziedzin obowiązującej w programie Socrates/Erasmus, czwarta (dotąd na ogół 0) – ewentualne uszczegółowienie informacji o dyscyplinie, piąta – stopień zaawansowania przedmiotu ustalony na podstawie roku studiów, dla którego przedmiot jest przeznaczony. / (0612) Database and network design and administration Kod ISCED - Międzynarodowa Standardowa Klasyfikacja Kształcenia (International Standard Classification of Education) została opracowana przez UNESCO.
Nazwa przedmiotu:	Logika i teoria typów
Jednostka:	Wydział Matematyki, Informatyki i Mechaniki
Grupy:	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:	(brak) Podstawowe informacje o zasadach przyporządkowania punktów ECTS: roczny wymiar godzinowy nakładu pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się dla danego etapu studiów wynosi 1500-1800 h, co odpowiada 60 ECTS; tygodniowy wymiar godzinowy nakładu pracy studenta wynosi 45 h; 1 punkt ECTS odpowiada 25-30 godzinom pracy studenta potrzebnej do osiągnięcia zakładanych efektów uczenia się; tygodniowy nakład pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się pozwala uzyskać 1,5 ECTS; nakład pracy potrzebny do zaliczenia przedmiotu, któremu przypisano 3 ECTS, stanowi 10% semestralnego obciążenia studenta. 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 (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.

Przedmiot nie jest oferowany w żadnym z aktualnych cykli dydaktycznych.

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