Seminarium będzie poświęcone wybranym tematom związanym z odpowiedniością
między systemami logicznymi a językami programowania i systemami typów, znaną
jako izomorfizm Curry'ego-Howarda. Punktem wyjścia będą "Lectures on the
Curry-Howard Isomorphism" M.H. Soerensena i P. Urzyczyna.
Wybrane zagadnienia:
Logika intuicjonistyczna i typowany rachunek lambda. Logika klasyczna i
operatory kontroli. Ekstrakcja programów z dowodów. Logiki wyższych rzędów i
PTSy (Pure Type Systems).
Wymagania: Logika dla informatyków, Metody programowania.
Mile widziane: Teoretyczne podstawy języków programowania.
