Logika i obliczenia

Izomorfizm Curry'ego-Howarda

Wyklad monograficzny, II semestr 2004/5


Materialy pomocnicze do wykladu (PostScript)

M.H. Sorensen, P. Urzyczyn,
Lectures on the Curry-Howard Isomorphism,
Elsevier, 2006 (?)
Wersja robocza, nie przeznaczona do rozpowszechniania

Rozdzial 1 (beztypowy rachunek lambda)
Rozdzial 2 (intuicjonistyczny rachunek zdan)
Rozdzial 3 (rachunek lambda z typami prostymi)
Rozdzial 4 (izomorfizm Curry'ego-Howarda)
Rozdzial 5 (rachunek kombinatorow)
Rozdzial 6 (logika klasyczna)
Rozdzial 7 (rachunek sekwentow)
Rozdzial 8 (logika pierwszego rzedu)
Rozdzial 9 (arytmetyka Peano i Heytinga)
Rozdzial 10 (system T)
Rozdzial 11 (logika zdaniowa drugiego rzedu i polimorficzny rachunek lambda)
Rozdzial 12 (arytmetyka drugiego rzedu)
Rozdzial 13 (typy zalezne)
Rozdzial 14 (rachunek konstrukcji itp.)
Dodatek (rozne definicje itp.)

Materialy dodatkowe:

Wyklad z rachunku lambda po polsku


Prosze o zglaszanie bledow i uwag do tekstu poczta elektroniczna.
Za poprawki dziekuje Pani Agnieszce Kozubek, Panom Marcinowi Dziubinskiemu, Filipowi Noworycie i Leszkowi Kolodziejczykowi, i oczywiscie Konradowi Zdanowskiemu.
Za poprawke drugiego rzedu dziekuje Panu Piotrowi Majewskiemu.
P.U.