И. А. Кудрявцева
Цена: 50 руб.
Автором выделен класс λ-термов с рекурсивными типами, для которых предложен алгоритм, решающий задачу синтеза типа (TSP), причем в этот класс входят
термы с рангами k=2 и k=4. Для проверки правильности работы алгоритма используется интерпретатор GHCi-6.10.3 со встроенной системой решения задачи
TCP в системе λ2. Алгоритм решения задачи TSP в системе λ2 в стиле Карри для λ-термов с рекурсивным типом реализован на языке программирования Haskell.
Ключевые слова: система типов λ2 с сильным полиморфизмом в стиле Карри, λ-термы с рекурсивным типом, метод решения задачи синтеза типа (TSP)
для λ-терма с рекурсивными типами.
REFERENCES
1. Geuvers, H. Introduction to type theory. Language Engineering and Rigorous
Software Development, 2008, Vol. 5520, Series Lecture Notes in Computer Science,
Uruguay: Alfa Lernet summer school, pp. 1–56.
2. Pierce, B.C. Types and Programming Languages. Bronnikov, G., & Ott, A.
(Trans.), 2012, Moscow: Lambda press “Dobrosvet”.
3. Barendregt, H., Dekkers, W., & Statman, R. Lambda calculi with types. Handbook
of logic in computer science, 1993, Vol. 2, Oxford University Press.
4. Kfoury, A.J., & Wells, J.B. Principality and decidable type inference for finiterank intersection types. ACM Symposium on Principles of Programming Languages
(POPL), 1999, pp. 161–174. doi: 10.1145/292540.292556
5. Dowek, G., & Levy, J.-J. Introduction to the Theory of Programming Languages.
2013, Moscow: DMK Press.
6. Moskvin, D. Properties of simply typed system. Lecture 5. Simply typed lambda
calculus. 2011, Retrieved January 15, 2016, from http://compsciclub.ru/node/1003
