S. van Bakel (1992):
Complete restrictions of the Intersection Type Discipline.
Theoretical Computer Science 102(1),
pp. 135–163,
doi:10.1016/0304-3975(92)90297-S.
S. van Bakel (1995):
Intersection Type Assignment Systems.
Theoretical Computer Science 151(2),
pp. 385–435,
doi:10.1016/0304-3975(95)00073-6.
S. van Bakel (2004):
Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalising.
Notre Dame journal of Formal Logic 45(1),
pp. 35–63,
doi:10.1305/ndjfl/1094155278.
S. van Bakel (2008):
The Heart of Intersection Type Assignment; Normalisation proofs revisited.
Theoretical Computer Science 398,
pp. 82–94,
doi:10.1016/j.tcs.2008.01.020.
S. van Bakel (2010):
Sound and Complete Typing for λμ.
In: Proceedings of 5th International Workshop Intersection Types and Related Systems (ITRS'10), Edinburgh, Scotland,
Electronic Proceedings in Theoretical Computer Science 45,
pp. 31–44,
doi:10.4204/EPTCS.45.3.
S. van Bakel (2011):
Strict intersection types for the Lambda Calculus.
ACM Computing Surveys 43,
pp. 20:1–20:49,
doi:10.1145/1922649.1922657.
S. van Bakel, F. Barbanera & U. de'Liguoro (2011):
A Filter Model for λμ.
In: L. Ong: Proceedings of 10th International Conference on Typed Lambda Calculi and Applications (TLCA'11),
Lecture Notes in Computer Science 6690.
Springer Verlag,
pp. 213–228,
doi:10.1007/978-3-642-21691-6_18.
S. van Bakel, F. Barbanera & U. de'Liguoro (2012):
Characterisation of Strongly Normalising λμ-Terms.
In: Proceedings of 6th International Workshop Intersection Types and Related Systems (ITRS'12), Dubrovnik, Croatia, June 29th,
Electronic Proceedings in Theoretical Computer Science 121,
pp. 31–44,
doi:10.4204/EPTCS.121.1.
S. van Bakel, F. Barbanera & U. de'Liguoro (2015):
Intersection types for λμ.
Logical Methods in Computer Science.
To appear.
S. van Bakel & M.G. Vigliotti (2014):
A fully abstract semantics of λμ in the π-calculus.
In: Proceedings of Sixth International Workshop on Classical Logic and Computation 2014 (CL&C'14), Vienna, Austria,
Electronic Proceedings in Theoretical Computer Science 164,
pp. 33–47,
doi:10.4204/EPTCS.164.3.
H. Barendregt (1984):
The Lambda Calculus: its Syntax and Semantics,
revised edition.
North-Holland,
Amsterdam,
doi:10.2307/2274112.
H. Barendregt, M. Coppo & M. Dezani-Ciancaglini (1983):
A filter lambda model and the completeness of type assignment.
Journal of Symbolic Logic 48(4),
pp. 931–940,
doi:10.2307/2273659.
C. Böhm (1968):
Alcune propietá delle forme βη-normali nel λk-calcolo.
Pubblicazioni 696, Instituto Nazionale per le Applicazioni del Calcolo. Roma.
A. Church (1936):
A Note on the Entscheidungsproblem.
Journal of Symbolic Logic 1(1),
pp. 40–41,
doi:10.2307/2269326.
Ph. de Groote (1994):
On the Relation between the λμ-Calculus and the Syntactic Theory of Sequential Control.
In: Proceedings of 5th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'94),
Lecture Notes in Computer Science 822.
Springer Verlag,
pp. 31–43,
doi:10.1007/3-540-58216-9_27.
U. de'.5pt Liguoro (2016):
The Approximation Theorem for the Λμ-Calculus.
Mathematical Structures in Computer Science FirstView,
pp. 1–21,
doi:10.1017/S0960129515000286.
M. Parigot (1992):
An algorithmic interpretation of classical natural deduction.
In: Proceedings of 3rd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'92),
Lecture Notes in Computer Science 624.
Springer Verlag,
pp. 190–201,
doi:10.1007/BFb0013061.
W. Py (1998):
Confluence en λμ-calcul.
Thèse de doctorat.
Université de Savoie.
S. Ronchi Della Rocca & B. Venneri (1984):
Principal type schemes for an extended type theory.
Theoretical Computer Science 28,
pp. 151–169,
doi:10.1016/0304-3975(83)90069-5.
A. Saurin (2010):
Standardization and Böhm Trees for λμ-calculus.
In: M. Blume, N. Kobayashi & G. Vidal: Functional and Logic Programming, 10th International Symposium, (FLOPS'10), Sendai, Japan,
Lecture Notes in Computer Science 6009.
Springer Verlag,
pp. 134–149,
doi:10.1007/978-3-642-12251-4_11.
Th. Streicher & B. Reus (1998):
Classical logic: Continuation Semantics and Abstract Machines.
Journal of Functional Programming 11(6),
pp. 543–572,
doi:10.1007/BFb0026995.
C.P. Wadsworth (1976):
The Relation Between Computational and Denotational Properties for Scott's D_-Models of the Lambda-Calculus.
SIAM Journal on Computing 5(3),
pp. 488–521,
doi:10.1137/0205036.