I. A. Kudryavtseva
Price: 50 руб.
The class of λ-terms with recursive type is determined by the author. It is proposed an algorithm for them, which solve type synthesis problem (TSP). This class consists of terms with ranks k=2 and k=4. For testing validity of the algorithm operation it is used the interpreter GHCi-6.10.3 with integrated task solution system TSP in system λ2. The algorithm of task solution TSP in system λ2 in the Carry’s style for λ-terms with recursive type is implemented in Haskell.
Keywords: system of λ2-types with tight polymorphism in the Carry’s style, λ-terms with recursive type, method of task solution TSP for λ-term with recursive type.
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
