Przykładowe projekty
Zakres projektu może ulegać rozszerzeniu, ale najlepiej jest zacząć od
zdefiniowania podstawowego, małego zadania i potem je rozwijać.
-
Prolog i unifikacja pierwszego rzędu.
-
Język MiniML: semantyka statyczna i dynamiczna, kompilacja.
Literatura: F. Pfenning,
"Computation and deduction", rozdziały 2-4,6.
-
Formalizacja i dowód poprawności transformacji programów funkcyjnych,
np. closure conversion, defunctionalization, A-translation,
lambda-lifting.
Wybrana literatura:
- A. Appel, "Continuation-passing, Closure-passing Style".
- P. Steckler, M. Wand, "Lightweight Closure Conversion".
- Y. Minamide, G. Morrisett, R. Harper, "Typed Closure Conversion".
- J. Reynolds, "Definitional Interpreters for Higher-Order Programming Languages".
- O. Danvy, L. Nielsen, "Defunctionalization at Work".
- F. Pottier, N. Gauthier, "Polymorphic typed defunctionalization and concretization".
- L. Nielsen, "A Denotational Investigation of Defunctionalization".
- A. Banerjee, N. Heintze, J. Riecke, "Design and Correctness of
Program Transformations Based on Control-Flow Analysis".
- A. Fischbach, J. Hannan, "Specification and Correctness of Lambda Lifting".
-
Weryfikacja dowodów twierdzeń logiki pierwszego rzędu w rachunku
sekwentów (ew. modulo teorie równościowe), za pomocą techniki "proof
by reflection".
-
Rachunek lambda i maszyna SECD.
Literatura: G. Plotkin, "Call-by-Name, Call-by Value and the Lambda Calculus".
-
Rachunek obiektów.
Literatura: M. Abadi, L. Cardelli, "A theory of primitive objects".
-
Język z funkcjami o wielu punktach powrotu.
Literatura: O. Shivers, D. Fisher, "Multi-return Function Call".
|