Rachunek lambda stanowi jądro wszystkich języków funkcyjnych, a także wielu systemów wspierających dowodzenie twierdzeń. Kluczowym zagadnieniem w tym kontekście staje się poprawna i efektywna implementacja β-redukcji, mechanizmu modelującego aplikację funkcji, a także operacji wyszukiwania kolejnego β-redeksu zgodnie z wybraną strategią redukcji. O ile w przypadku typowych języków funkcyjnych redukcja przyjmuje postać ewaluacji termu do słabej postaci normalnej, dowolnej λ-abstrakcji, w przypadku zamkniętych termów czystego rachunku lambda, to w przypadku porównywania typów zależnych przez systemy wspomagające dowodzenie twierdzeń wymagana jest pełna normalizacja termów, w tym termów otwartych, w ciele λ-abstrakcji.
Tematem seminarium jest przegląd wybranych zagadnień związanych z procedurami redukującymi λ-termy. Wśród omawianych zagadnień znajdą się m. in. syntaktyczne ewaluatory i normalizatory bezpośrednio implementujące określoną strategię redukcji (semantyka redukcyjna, maszyny abstrakcyjne), autointerpretery (ang. self-interpreters), a także ewaluatory w kluczowy sposób wykorzystujące mechanizm redukcji w meta-języku (ewaluatory i normalizatory wyższego rzędu, w tym te realizujące model NbE - normalizacji przez ewaluację). W szczególności, sporo miejsca poświęcimy konstrukcji, poprawności i analizie maszyn abstrakcyjnych.
**Literatura (wybrane prace):**
1. Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, Jan Midtgaard: A functional correspondence between evaluators and abstract machines. PPDP 2003: 8-19
2. Małgorzata Biernacka, Olivier Danvy:
A concrete framework for environment machines. ACM Trans. Comput. Log. 9(1): 6 (2007)
3. Ulrich Berger, Helmut Schwichtenberg:
An Inverse of the Evaluation Functional for Typed Lambda-Calculus. LICS 1991: 203-211
4. Klaus Aehlig, Felix Joachimski:
Operational aspects of untyped Normalisation by Evaluation. Math. Struct. Comput. Sci. 14(4): 587-611 (2004)
5. Torben Æ. Mogensen:
Efficient Self-Interpretations in Lambda Calculus. J. Funct. Program. 2(3): 345-363 (1992)
6. Pierre Crégut:
Strongly reducing variants of the Krivine abstract machine. High. Order Symb. Comput. 20(3): 209-230 (2007)
7. Benjamin Grégoire, Xavier Leroy:
A compiled implementation of strong reduction. ICFP 2002: 235-246
8. Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza:
Distilling abstract machines. ICFP 2014: 363-376
9. Beniamino Accattoli, Giulio Guerrieri:
Abstract machines for Open Call-by-Value. Sci. Comput. Program. 184 (2019)
10. Martín Abadi, Luca Cardelli, Pierre-Louis Curien, Jean-Jacques Lévy:
Explicit Substitutions. J. Funct. Program. 1(4): 375-416 (1991)
