1. Andreas Abel (2007): Syntactical strong normalization for intersection types with term rewriting rules. In: Proceedings of HOR'07, pp. 5–12.
  2. Steffen van Bakel (1992): Complete restrictions of the intersection type discipline. Theoretical Computer Science 102, pp. 135–163, doi:10.1016/0304-3975(92)90297-S.
  3. Steffen van Bakel (2004): Cut-elimination in the strict intersection type assignment system is strongly normalizing. Notre Dame Journal of Formal Logic 45, pp. 35–63, doi:10.1305/ndjfl/1094155278.
  4. Henk Barendregt, Wil Dekkers & Richard Statman (2013): Lambda Calculus with Types. Cambridge University Press, doi:10.1017/CBO9781139032636.
  5. Henk P. Barendregt (1984): The Lambda Calculus: Its Syntax and Semantics, revised edition. North-Holland, Amsterdam.
  6. Gerard Boudol (2003): On strong normalization in the intersection type discipline. In: Proceedings of TLCA'03, Lecture Notes in Computer Science 2701. Springer-Verlag, pp. 60–74, doi:10.1007/3-540-44904-3_5.
  7. Antonio Bucciarelli, Adolfo Piperno & Ivano Salvo (2003): Intersection types and λ-definability. Mathematical Structures in Computer Science 13, pp. 15–53, doi:10.1017/S0960129502003833.
  8. Mario Coppo, Mariangiola Dezani-Ciancaglini & Betti Venneri (1981): Functional characters of solvable terms. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 27, pp. 45–58, doi:10.1002/malq.19810270205.
  9. René David (2001): Normalization without reducibility. Annals of Pure and Applied Logic 107, pp. 121–130, doi:10.1016/S0168-0072(00)00030-0.
  10. Mariangiola Dezani-Ciancaglini, Elio Giovannetti & Ugo de'Liguoro (1998): Intersection types, λ-models, and Böhm trees. In: Theories of Types and Proofs, MSJ Memoirs 2. Mathematical Society of Japan, Tokyo, pp. 45–97.
  11. Mariangiola Dezani-Ciancaglini, Furio Honsell & Yoko Motohama (2001): Approximation theorems for intersection type systems. Journal of Logic and Computation 11, pp. 395–417, doi:10.1093/logcom/11.3.395.
  12. Felix Joachimski & Ralph Matthes (2003): Short proofs of normalization for the simply-typed λ-calculus, permutative conversions and Gödel's T. Archive for Mathematical Logic 42, pp. 59–87, doi:10.1007/s00153-002-0156-9.
  13. Fairouz Kamareddine, Vincent Rahli & Joe B. Wells (2012): Reducibility proofs in the λ-calculus. Fundamenta Informaticae 121, pp. 121–152, doi:10.3233/FI-2012-773.
  14. Assaf J. Kfoury & Joe B. Wells (1995): New notions of reduction and non-semantic proofs of strong β-normalization in typed λ-calculi. In: Proceedings of LICS'95. IEEE Computer Society Press, pp. 311–321, doi:10.1109/LICS.1995.523266.
  15. Kentaro Kikuchi (2009): On general methods for proving reduction properties of typed lambda terms. In: Proof theoretical study of the structure of logic and computation, RIMS Kôkyûroku 1635, pp. 33–50. Available at (Unrefereed proceedings).
  16. Ralph Matthes (2000): Characterizing strongly normalizing terms of a λ-calculus with generalized applications via intersection types. In: Proceedings of ICALP Satellite Workshops 2000. Carleton Scientific, pp. 339–354.
  17. Garrel Pottinger (1980): A type assignment for the strongly normalizable λ-terms. In: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, London, pp. 561–577.
  18. Femke van Raamsdonk & Paula Severi (1995): On normalisation. Technical Report CS-R9545. CWI.
  19. Femke van Raamsdonk, Paula Severi, Morten Heine B. Sørensen & Hongwei Xi (1999): Perpetual reductions in λ-calculus. Information and Computation 149, pp. 173–225, doi:10.1006/inco.1998.2750.
  20. William W. Tait (1967): Intensional interpretations of functionals of finite type I. The Journal of Symbolic Logic 32, pp. 198–212, doi:10.2307/2271658.
  21. Silvio Valentini (2001): An elementary proof of strong normalization for intersection types. Archive for Mathematical Logic 40, pp. 475–488, doi:10.1007/s001530000070.

Comments and questions to:
For website issues: