References

  1. 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.
  2. S. van Bakel (1995): Intersection Type Assignment Systems. Theoretical Computer Science 151(2), pp. 385–435, doi:10.1016/0304-3975(95)00073-6.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. S. van Bakel (2016): Approximation and (Head) Normalisation for λμ using Strict Intersection Types. Available at http://www.doc.ic.ac.uk/~svb/Research/Papers/Lmu-Strict.pdf.
  8. 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.
  9. 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.
  10. S. van Bakel, F. Barbanera & U. de'Liguoro (2015): Intersection types for λμ. Logical Methods in Computer Science. To appear.
  11. 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.
  12. H. Barendregt (1984): The Lambda Calculus: its Syntax and Semantics, revised edition. North-Holland, Amsterdam, doi:10.2307/2274112.
  13. 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.
  14. C. Böhm (1968): Alcune propietá delle forme βη-normali nel λk-calcolo. Pubblicazioni 696, Instituto Nazionale per le Applicazioni del Calcolo. Roma.
  15. A. Church (1936): A Note on the Entscheidungsproblem. Journal of Symbolic Logic 1(1), pp. 40–41, doi:10.2307/2269326.
  16. H.B. Curry & R. Feys (1958): Combinatory Logic 1. North-Holland, Amsterdam.
  17. 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.
  18. U. de'.5pt Liguoro (2016): The Approximation Theorem for the Λμ-Calculus. Mathematical Structures in Computer Science FirstView, pp. 1–21, doi:10.1017/S0960129515000286.
  19. 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.
  20. W. Py (1998): Confluence en λμ-calcul. Thèse de doctorat. Université de Savoie.
  21. 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.
  22. 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.
  23. 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.
  24. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org