Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam (revised edn.) (1984)
Carlier, S., Polakow, J., Wells, J.B., Kfoury, A.J.: System E: Expansion variables for flexible typing with linear and non-linear types and intersection types. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986. Springer, Heidelberg (2004)
Carlier, S., Wells, J.B.: Expansion: the crucial mechanism for type inference with intersection types: A survey and explanation. In: Proc. 3rd Int'l Workshop Intersection Types & Related Systems (ITRS 2004), July 19, 2005. The ITRS 2004 proceedings of Elec. Notes in Theoret. Comp. Sci., vol. 136 (2005)
Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Principal type schemes and λ-calculus semantics. In: Hindley, J.R., Seldin, J.P. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, London (1980)
Coquand, T.: Completeness theorems and lambda-calculus. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461. Springer, Heidelberg (2005)
Goos, G., Hartmanis, J. (eds.): λ - Calculus and Computer Science Theory. LNCS, vol. 37. Springer, Heidelberg (1975)
Hindley, J.R.: The simple semantics for Coppo-Dezani-Sallé types. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137. Springer, Heidelberg (1982)
Hindley, J.R.: The completeness theorem for typing λ-terms. Theoretical Computer Science 22 (1983)
Hindley, J.R.: Curry's types are complete with respect to F-semantics too. Theoretical Computer Science 22 (1983)
Hindley, J.R.: Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, vol. 42. Cambridge University Press, Cambridge (1997)
Kamareddine, F., Nour, K.: A completeness result for a realisability semantics for an intersection type system. Ann. Pure Appl. Logic 146(2-3) (2007)
Kamareddine, F., Nour, K., Rahli, V., Wells, J.B.: A complete realisabil-ity semantics for intersection types and infinite expansion variables (2008), http://www.macs.hw.ac.uk/∼fairouz/papers/drafts/compsem-big.pdf
Kamareddine, F., Nour, K., Rahli, V., Wells, J.B.: Realisability semantics for intersection type systems and expansion variables. In: ITRS 2008 (2008), http://www.macs.hw.ac.uk/∼fairouz/papers/conference-publications/ semone.pdf
Krivine, J.: Lambda-Calcul : Types et Modèles. Etudes et Recherches en Informa-tique. Masson (1990)