Seminarium: Izomorfizm Curry'ego-Howarda
Seminarium będzie poświęcone teoretycznym podstawom izomorfizmu Curry'ego-Howarda, rozumianego jako odpowiedniość między systemami logicznymi a językami programowania z typami (aka "proofs-as-programs", "formulas-as-types").
Propozycje tematów:
  1. [A. Balicki] Rachunek lambda z typami prostymi i system dedukcji naturalnej dla logiki minimalnej. [Chap. 2,3,4] [!,☆]
  2. Logika kombinatorów. [Chap. 5] [☆]
  3. Rachunek sekwentów. [Chap. 7] [☆]
  4. Logika pierwszego rzędu i typy zależne. Arytmetyka Heytinga i Peano. [Chap. 8, 9, 13] [!,☆☆]
  5. System T. [Chap. 10] [☆]
  6. Logika drugiego rzędu i polimorfizm. Arytmetyka drugiego rzędu. [Chap. 11,12] [!, ☆☆]
  7. PTSy (pure type systems). [Chap. 14] [!, ☆☆☆]
  8. Logika klasyczna i operatory sterowania. [Chap. 6] [☆☆]
  9. Realizability interpretation. Ekstrakcja programów. [☆☆☆]
  10. Monadyczny język Moggiego i logika modalna. [☆☆☆]
Podstawowa lektura to "Lectures on the Curry-Howard isomorphism" autorstwa M. H. Sørensena i P. Urzyczyna.