Z.M. Ariola & H. Herbelin (2003):
Minimal Classical Logic and Control Operators.
In: Proceedings of Automata, Languages and Programming, 30th International Colloquium, ICALP'03, 2003,
Lecture Notes in Computer Science 2719.
Springer,
pp. 871–885.
S. van Bakel (1992):
Complete restrictions of the Intersection Type Discipline.
Theoretical Computer Science 102(1),
pp. 135–163.
S. van Bakel (2010):
Completeness and Partial Soundness Results for Intersection & Union Typing for `l`m"767Eμ.
Annals of Pure and Applied Logic 161,
pp. 1400–1430.
S. van Bakel (2010):
Completeness and Soundness results for X with Intersection and Union Types.
To appear in: Fundamenta Informaticae.
S. van Bakel & U. de'Liguoro (2008):
Logical equivalence for subtyping object and recursive types.
Theory of Computing Systems 42(3),
pp. 306–348.
S. van Bakel & M. Fernández (1997):
Normalization Results for Typeable Rewrite Systems.
Information and Computation 2(133),
pp. 73–116.
S. van Bakel, S. Lengrand & P. Lescanne (2005):
The language X: Circuits, Computations and Classical Logic.
In: Proceedings of Ninth Italian Conference on Theoretical Computer Science (ICTCS'05),
Lecture Notes in Computer Science 3701.
Springer Verlag,
pp. 81–96.
S. van Bakel & P. Lescanne (2008):
Computation with Classical Sequents.
Mathematical Structures in Computer Science 18,
pp. 555–609.
F. Barbanera, M. Dezani-Ciancaglini & U. de'Liguoro (1995):
Intersection and Union Types: Syntax and Semantics.
Information and Computation 119(2),
pp. 202–230.
H. Barendregt (1984):
The Lambda Calculus: its Syntax and Semantics.
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.
A. Church (1936):
A Note on the Entscheidungsproblem.
Journal of Symbolic Logic 1(1),
pp. 40–41.
M. Coppo & M. Dezani-Ciancaglini (1978):
A New Type Assignment for Lambda-Terms.
Archive für Mathematischer Logic und Grundlagenforschung 19,
pp. 139–156.
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,
pp. 233–243.
R. Davies & F. Pfenning (2001):
A judgmental reconstruction of modal logic.
Mathematical Structures in Computer Science 11(4),
pp. 511–540.
D. Dougherty, S. Ghilezan & P. Lescanne (2004):
Intersection and Union Types in the `l`m"767Eμ-calculus.
In: Electronic Proceedings of 2nd International Workshop Intersection Types and Related Systems (ITRS'04),
Electronic Notes in Theoretical Computer Science 136,
pp. 228–246.
D. Dougherty, S. Ghilezan & P. Lescanne (2008):
Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage.
Theoretical Computer Science 398.
J. Dunfield & F. Pfenning (2003):
Type Assignment for Intersections and Unions in Call-by-Value Languages.
In: Proceedings of 6th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'03),
pp. 250–266.
G. Gentzen (1935):
Investigations into logical deduction.
In: The Collected Papers of Gerhard Gentzen.
Ed M. E. Szabo, North Holland, 68ff (1969).
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.
B. Harper & M. Lillibridge (1991):
ML with callcc is unsound.
Post to TYPES mailing list, July 8.
H. Herbelin (2005):
C'est maintenant qu'on calcule: au cœur de la dualité.
Mémoire de habilitation.
Université Paris 11.
J.R. Hindley (1997):
Basic Simple Type Theory.
Cambridge University Press.
S. Lengrand (2003):
Call-by-value, call-by-name, and strong normalization for the classical sequent calculus.
In: 3rd Workshop on Reduction Strategies in Rewriting and Programming (WRS 2003),
Electronic Notes in Theoretical Computer Science 86.
Elsevier.
S. Maffeis (2005):
Sequence Types for the pi-calculus.
Electronic Notes in Theoretical Computer Science 136,
pp. 117–132.
R. Milner, M. Tofte, R. Harper & D. MacQueen (1990):
The Definition of Standard ML.
MIT Press.
Revised edition.
C.-H. L. Ong & C.A. Stewart (1997):
A Curry-Howard foundation for functional computation with control.
In: Proceedings of the 24th Annual ACM Symposium on Principles Of Programming Languages,
pp. 215–227.
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.
M. Parigot (1993):
Classical Proofs as Programs.
In: Kurt Gödel Colloquium,
pp. 263–276.
Presented at TYPES Workshop, 1992.
M. Parigot (1993):
Strong Normalization for Second Order Classical Natural Deduction.
In: Proceedings of Eighth Annual IEEE Symposium on Logic in Computer Science, 19-23 June 1993,
pp. 39–46.
B.C. Pierce (1991):
Programming with Intersection Types and Bounded Polymorphism.
Ph.D. thesis.
Carnegie Mellon University, School of Computer Science, Pitssburgh.
CMU-CS-91-205.
A.K. Wright (1995):
Simple imperative polymorphism.
Lisp and Symbolic Computation 8(4),
pp. 343–355.