Geodesic
On the type correctness of polymorphic $\lambda$-terms. 2
Proceedings of the Yerevan State University. Physical and mathematical sciences, no. 1 (2010), pp. 37-46 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

In this paper the polymorphic lambda terms are considered, where no type information is provided for the variables. The aim of this work is to prove that presented typification algorithm [1] typifies such terms in most common way.
Keywords: type, skeleton, expansion, principal typing.
Mots-clés : term, constraint 
@article{UZERU_2010_1_a6,
     author = {A. H. Arakelyan},
     title = {On the type correctness of polymorphic $\lambda$-terms.~2},
     journal = {Proceedings of the Yerevan State University. Physical and mathematical sciences},
     pages = {37--46},
     year = {2010},
     number = {1},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/UZERU_2010_1_a6/}
}
TY  - JOUR
AU  - A. H. Arakelyan
TI  - On the type correctness of polymorphic $\lambda$-terms. 2
JO  - Proceedings of the Yerevan State University. Physical and mathematical sciences
PY  - 2010
SP  - 37
EP  - 46
IS  - 1
UR  - http://geodesic.mathdoc.fr/item/UZERU_2010_1_a6/
LA  - en
ID  - UZERU_2010_1_a6
ER  - 
%0 Journal Article
%A A. H. Arakelyan
%T On the type correctness of polymorphic $\lambda$-terms. 2
%J Proceedings of the Yerevan State University. Physical and mathematical sciences
%D 2010
%P 37-46
%N 1
%U http://geodesic.mathdoc.fr/item/UZERU_2010_1_a6/
%G en
%F UZERU_2010_1_a6
A. H. Arakelyan. On the type correctness of polymorphic $\lambda$-terms. 2. Proceedings of the Yerevan State University. Physical and mathematical sciences, no. 1 (2010), pp. 37-46. http://geodesic.mathdoc.fr/item/UZERU_2010_1_a6/

[1] A. H. Arakelyan, “On the type correctness of polymorphic $\lambda$-terms. part 1”, Proceedings of the YSU, Phys. Math. Sciences, 2009, no. 3, 42–51 | MR

[2] R. Milner, “A theory of type polymorphism in programming”, Journal of Computer and System Sciences, 17 (1978), 348–375 | DOI | MR | Zbl

[3] J.B. Wells, “The essence of principal typings” (Proc. 29th Intl Coll. Automata, Languages, and Programming), LNCS, 2380, Springer-Verlag, 2002 | MR | Zbl

[4] T. Jim, “What are Principal Typings and What are They Good for?”, Conf. Rec. POPL '96: 23rd ACM Symp. Princ. of Prog. Langs, 1996.

[5] S. Carlier, J.B. Wells, “Type Inference with Expansion Variables and Intersection Types in System E and an Exact Correspondence with $\beta$-reduction”, Proc. 6th Intl Conf. Principles $\$ Practice Declarative Programming, 2004

[6] S. Carlier, J. Polakow, J.B. Wells, A.J. Kfoury, “System $E$: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types”, In Programming Languages $\$ Systems (13th European Symp. Programming), LNCS, 2986, Springer-Verlag, 2004 | Zbl

[7] H.P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North Holand, Amsterdam, 1981 | MR | Zbl