Uniwersytet Warszawski - Centralny System UwierzytelnianiaNie 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:

Egzamin

Zajęcia w cyklu "Semestr letni 2018/19" (zakończony)

Okres: 2019-02-16 - 2019-06-08
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
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin
Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.