Uniwersytet Warszawski - Centralny System Uwierzytelniania
Strona główna

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 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 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.

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 2022/23" (jeszcze nie rozpoczęty)

Okres: 2022-10-01 - 2023-01-29
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
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin
Uwagi:

Wykład będzie odbywać się zdalnie, a ćwiczenia stacjonarnie.

Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.
Krakowskie Przedmieście 26/28
00-927 Warszawa
tel: +48 22 55 20 000 https://uw.edu.pl/
kontakt deklaracja dostępności USOSweb 6.8.0.0-1 (2022-08-01)