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

Voir la notice de l'article

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

[1] 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

[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. 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

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