Andreas Abel (2007):
Syntactical strong normalization for intersection types with term rewriting rules.
In: Proceedings of HOR'07,
pp. 5–12.
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.
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.
Henk Barendregt, Wil Dekkers & Richard Statman (2013):
Lambda Calculus with Types.
Cambridge University Press,
doi:10.1017/CBO9781139032636.
Henk P. Barendregt (1984):
The Lambda Calculus: Its Syntax and Semantics,
revised edition.
North-Holland,
Amsterdam.
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.
Antonio Bucciarelli, Adolfo Piperno & Ivano Salvo (2003):
Intersection types and λ-definability.
Mathematical Structures in Computer Science 13,
pp. 15–53,
doi:10.1017/S0960129502003833.
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.
René David (2001):
Normalization without reducibility.
Annals of Pure and Applied Logic 107,
pp. 121–130,
doi:10.1016/S0168-0072(00)00030-0.
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.
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.
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.
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.
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.
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 http://hdl.handle.net/2433/140464.
(Unrefereed proceedings).
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.
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.
Femke van Raamsdonk & Paula Severi (1995):
On normalisation.
Technical Report CS-R9545.
CWI.
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.
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.
Silvio Valentini (2001):
An elementary proof of strong normalization for intersection types.
Archive for Mathematical Logic 40,
pp. 475–488,
doi:10.1007/s001530000070.
eptcs@eptcs.org