W ramach seminarium będziemy poszukiwać związków pomiędzy systemami logicznymi
a językami programowania i systemami typów. Odpowiedniość ta jest znana jako
izomorfizm Curry'ego-Howarda, a także w formie sloganu "dowody jako programy"
(czyli jeśli dowodzimy przez indukcję to tak naprawdę piszemy program
rekurencyjny w języku funkcyjnym).
Punktem wyjścia będą klasyczne "Lectures on the Curry-Howard Isomorphism" M.H.
Soerensena i P. Urzyczyna.
Przykładowe zagadnienia:
Logika intuicjonistyczna i typowany rachunek lambda. Rachunek kombinatorów i
system Hiberta. Logika klasyczna i operatory sterowania. Ekstrakcja programów
z dowodów. Logiki wyższych rzędów i PTSy (Pure Type Systems). Pewne logiki
substrukturalne i odpowiadające im warianty rachunku lambda.
Wymagania: Logika dla informatyków, Metody programowania.
Mile widziane: Teoretyczne podstawy języków programowania.
