Z.M. Ariola & H. Herbelin (2003):
Minimal Classical Logic and Control Operators.
In: J.C.M. Baeten, J.K. Lenstra, J. Parrow & G.J. Woeginger: Proceedings of Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003,
Lecture Notes in Computer Science 2719.
Springer Verlag,
pp. 871–885,
doi:10.1007/3-540-45061-0_68.
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 (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 (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 & P. Lescanne (2008):
Computation with Classical Sequents.
Mathematical Structures in Computer Science 18,
pp. 555–609,
doi:10.1017/S0960129508006762.
F. Barbanera & S. Berardi (1996):
A Symmetric Lambda Calculus for Classical Program Extraction.
Information and Computation 125(2),
pp. 103–117,
doi:10.1006/inco.1996.0025.
H. Barendregt (1984):
The Lambda Calculus: its Syntax and Semantics,
revised edition.
North-Holland,
Amsterdam.
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.
A. Church (1936):
A Note on the Entscheidungsproblem.
Journal of Symbolic Logic 1(1),
pp. 40–41,
doi:10.2307/2269326.
M. Coppo & M. Dezani-Ciancaglini (1978):
A New Type Assignment for λ-Terms.
Archiv für Mathematische Logic und Grundlagen Forschung 19,
pp. 139–156,
doi:10.1007/BF02011875.
M. Coppo, M. Dezani-Ciancaglini & B. Venneri (1980):
Principal type schemes and λ-calculus semantics.
In: J.R. Hindley & J.P. Seldin: To H.B. Curry, Essays in combinatory logic, lambda-calculus and formalism.
Academic press, New York,
pp. 535–560.
P.-L. Curien & H. Herbelin (2000):
The Duality of Computation.
In: Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP'00),
ACM Sigplan Notices 35.9.
ACM,
pp. 233–243,
doi:10.1145/351240.351262.
G. Gentzen (1935):
Investigations into logical deduction.
In: The Collected Papers of Gerhard Gentzen.
Ed M. E. Szabo, North Holland, 68ff (1969).
S. Ghilezan (1996):
Strong Normalization and Typability with Intersection Types.
Notre Dame journal of Formal Logic 37(1),
pp. 44–52,
doi:10.1305/ndjfl/1040067315.
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.
H. Herbelin & A. Saurin (2010):
λμ-calculus and λμ-calculus: a Capital Difference.
Manuscript.
J.-L Krivine (1993):
Lambda calculus, types and models.
Ellis Horwood.
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.
M. Parigot (1997):
Proofs of Strong Normalisation for Second Order Classical Natural Deduction.
Journal of Symbolic Logic 62(4),
pp. 1461–1479,
doi:10.2307/2275652.
G. Pottinger (1980):
A Type Assignment for the Strongly Normalizable λ-terms.
In: J.P. Seldin & J.R. Hindley: To H. B. Curry, Essays in Combinatory Logic, Lambda-Calculus and Formalism.
Academic press, New York,
pp. 561–577.
A. Saurin (2008):
On the Relations between the Syntactic Theories of λμ-Calculi.
In: M. Kaminski & S. Martini: Computer Science Logic, 22nd International Workshop (CSL'08), Bertinoro, Italy,
Lecture Notes in Computer Science 5213.
Springer Verlag,
pp. 154–168,
doi:10.1016/j.entcs.2005.11.072.
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.1017/S0956796898003141.
W. Tait (1967):
Intensional Interpretations of Functionals of Finite Type I.
Journal of Symbolic Logic 32(2),
pp. 198–212,
doi:10.2307/2271658.
eptcs@eptcs.org