Seminarium poświęcone jest zagadnieniom związanym z obliczeniową interpretacją logiki klasycznej, ze szczególnym uwzględnieniem roli kontynuacji. Poruszane na seminarium tematy dotyczą zarówno formalnych systemów wnioskowania w logice klasycznej, takich jak systemy dedukcji naturalnej czy rachunek sekwentów i ich własności, m. in. normalizacji dowodów oraz związków z logiką intuicjonistyczną, jak i teorii redukcji rachunku lambda wzbogaconego o operatory sterowania takie jak call/cc. Tematyka seminarium obejmuje również transformacje do stylu kontynuacyjnego, ekstrakcję programów z dowodów klasycznych oraz poszukiwanie dowodów w logice klasycznej.
**Wymagania wstępne**
Jest to przedmiot zaawansowany, przeznaczony dla studentów zainteresowanych logiką i systemami formalnymi. Wymagana jest podstawowa dojrzałość matematyczna oraz znajomość treści z przedmiotów takich jak Logika dla informatyków, Metody programowania, Programowanie funkcyjne, Teoretyczne podstawy języków programowania (rachunek lambda, dedukcja naturalna, typy proste, system F, formuły jako typy).
**Wybrana literatura**
Timothy Griffin:
A Formulae-as-Types Notion of Control. POPL 1990: 47-58
Chetan R. Murthy:
Extracting Constructive Content From Classical Proofs. Cornell University, USA, 1990
Michel Parigot:
Lambda-Mu-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. LPAR 1992: 190-201
Philip Wadler:
Call-by-value is dual to call-by-name. ICFP 2003: 189-201
Franco Barbanera, Stefano Berardi:
Extracting Constructive Content from Classical Logic via Control-like Reductions. TLCA 1993: 45-59
Franco Barbanera, Stefano Berardi:
A Strong Normalization Result for Classical Logic. Ann. Pure Appl. Log. 76(2): 99-116 (1995)
Pierre-Louis Curien, Hugo Herbelin:
The duality of computation. ICFP 2000: 233-243
Daniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne:
Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: Extending the Coppo-Dezani heritage. Theor. Comput. Sci. 398(1-3): 114-128 (2008)
Zena M. Ariola, Hugo Herbelin, Amr Sabry:
A proof-theoretic foundation of abortive continuations. High. Order Symb. Comput. 20(4): 403-429 (2007)
Zena M. Ariola, Hugo Herbelin:
Control reduction theories: the benefit of structural substitution. J. Funct. Program. 18(3): 373-419 (2008)
Paul Downen, Zena M. Ariola:
A tutorial on computational classical logic and the sequent calculus. J. Funct. Program. 28: e3 (2018)
