References

  1. 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.
  2. S. van Bakel (1992): Complete restrictions of the Intersection Type Discipline. Theoretical Computer Science 102(1), pp. 135–163.
  3. 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.
  4. S. van Bakel (2010): Completeness and Soundness results for X with Intersection and Union Types. To appear in: Fundamenta Informaticae.
  5. S. van Bakel & U. de'Liguoro (2008): Logical equivalence for subtyping object and recursive types. Theory of Computing Systems 42(3), pp. 306–348.
  6. S. van Bakel & M. Fernández (1997): Normalization Results for Typeable Rewrite Systems. Information and Computation 2(133), pp. 73–116.
  7. 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.
  8. S. van Bakel & P. Lescanne (2008): Computation with Classical Sequents. Mathematical Structures in Computer Science 18, pp. 555–609.
  9. F. Barbanera, M. Dezani-Ciancaglini & U. de'Liguoro (1995): Intersection and Union Types: Syntax and Semantics. Information and Computation 119(2), pp. 202–230.
  10. H. Barendregt (1984): The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam.
  11. 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.
  12. A. Church (1936): A Note on the Entscheidungsproblem. Journal of Symbolic Logic 1(1), pp. 40–41.
  13. M. Coppo & M. Dezani-Ciancaglini (1978): A New Type Assignment for Lambda-Terms. Archive für Mathematischer Logic und Grundlagenforschung 19, pp. 139–156.
  14. 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.
  15. H.B. Curry & R. Feys (1958): Combinatory Logic 1. North-Holland, Amsterdam.
  16. R. Davies & F. Pfenning (2001): A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science 11(4), pp. 511–540.
  17. 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.
  18. 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.
  19. 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.
  20. G. Gentzen (1935): Investigations into logical deduction. In: The Collected Papers of Gerhard Gentzen. Ed M. E. Szabo, North Holland, 68ff (1969).
  21. 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.
  22. B. Harper & M. Lillibridge (1991): ML with callcc is unsound. Post to TYPES mailing list, July 8.
  23. H. Herbelin (2005): C'est maintenant qu'on calcule: au cœur de la dualité. Mémoire de habilitation. Université Paris 11.
  24. J.R. Hindley (1997): Basic Simple Type Theory. Cambridge University Press.
  25. 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.
  26. S. Maffeis (2005): Sequence Types for the pi-calculus. Electronic Notes in Theoretical Computer Science 136, pp. 117–132.
  27. R. Milner, M. Tofte, R. Harper & D. MacQueen (1990): The Definition of Standard ML. MIT Press. Revised edition.
  28. 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.
  29. 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.
  30. M. Parigot (1993): Classical Proofs as Programs. In: Kurt Gödel Colloquium, pp. 263–276. Presented at TYPES Workshop, 1992.
  31. 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.
  32. 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.
  33. A.K. Wright (1995): Simple imperative polymorphism. Lisp and Symbolic Computation 8(4), pp. 343–355.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org