References

  1. Mart\'ın Abadi, Luca Cardelli, Pierre-Louis Curien & Jean-Jacques Lévy (1991): Explicit Substitutions. Journal of Functional Programming 1(4), pp. 375–416, doi:10.1017/S0956796800000186.
  2. Stephen Adams (1993): Efficient Sets - A Balancing Act. Journal of Functional Programming 3(4), pp. 553–561, doi:10.1017/S0956796800000885.
  3. Amal Ahmed, Andrew W. Appel, Christopher D. Richards, Kedar N. Swadi, Gang Tan & Daniel C. Wang (2010): Semantic foundations for typed assembly languages. ACM Transactions on Programming Languages and Systems 32(3), doi:10.1145/1709093.1709094.
  4. Henk Barendregt (1984): The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam.
  5. Nick Benton, Gavin M. Bierman, Valeria de Paiva & Martin Hyland (1993): A Term Calculus for Intuitionistic Linear Logic. In: Marc Bezem & Jan Friso Groote: Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, Lecture Notes in Computer Science 664. Springer-Verlag, pp. 75–90, doi:10.1007/BFb0037099.
  6. Mathieu Boespflug (2010): Conversion by Evaluation. In: Manuel Carro & Ricardo Peña: Practical Aspects of Declarative Languages, 12th International Symposium, PADL 2010, Madrid, Spain, January 18-19, 2010. Proceedings, Lecture Notes in Computer Science 5937. Springer-Verlag, pp. 58–72, doi:10.1007/978-3-642-11503-5_7.
  7. N. G. de Bruijn (1972): Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 34, pp. 381–392, doi:10.1016/1385-7258(72)90034-0.
  8. Iliano Cervesato & Frank Pfenning (2003): A Linear Spine Calculus. Journal of Logic and Computation 13(5), pp. 639–688, doi:10.1093/logcom/13.5.639.
  9. Thierry Coquand (1996): An Algorithm for Type-Checking Dependent Types. In: Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction (July 17–21, 1995, Kloster Irsee, Germany), Science of Computer Programming 26. Elsevier, pp. 167–177, doi:10.1016/0167-6423(95)00021-6.
  10. Maribel Fernández, Ian Mackie & François-Régis Sinot (2005): Lambda-Calculus with Director Strings. Applicable Algebra in Engineering, Communication and Computing 15(6), pp. 393–437, doi:10.1007/s00200-005-0169-9.
  11. Matthew Fluet & Stephen Weeks (2001): Contification Using Dominators. In: Proceedings of the sixth ACM SIGPLAN International Conference on Functional Programming (ICFP 2001), pp. 2–13, doi:10.1145/507635.507639.
  12. Jean-Yves Girard (1987): Linear Logic. Theoretical Computer Science 50, pp. 1–102, doi:10.1016/0304-3975(87)90045-4.
  13. Benjamin Grégoire & Xavier Leroy (2002): A compiled implementation of strong reduction. In: Proceedings of the seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002, SIGPLAN Notices 37. ACM Press, pp. 235–246, doi:10.1145/581478.581501.
  14. INRIA (2010): The Coq Proof Assistant Reference Manual, version 8.3 edition. INRIA. Available at http://coq.inria.fr/.
  15. Delia Kesner & Stéphane Lengrand (2007): Resource operators for lambda-calculus. Information and Computation 205(4), pp. 419–473, doi:10.1016/j.ic.2006.08.008.
  16. Nicolai Kraus (2011): A Lambda Term Representation Based on Linear Ordered Logic. Bachelor's thesis. Department of Computer Science, Ludwig-Maximilians-University Munich.
  17. Chuck Liang, Gopalan Nadathur & Xiaochu Qi (2005): Choices in representation and reduction strategies for lambda terms in intensional contexts. Journal of Automated Reasoning 33(2), pp. 89–132, doi:10.1007/s10817-004-6885-1.
  18. Conor McBride & James McKinna (2004): The view from the left. Journal of Functional Programming 14(1), pp. 69–111, doi:10.1017/S0956796803004829.
  19. Gopalan Nadathur (1999): A Fine-Grained Notation for Lambda Terms and Its Use in Intensional Operations. Journal of Functional and Logic Programming 1999(2). Available at http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1999/A99-02/A99-02.html.
  20. Gopalan Nadathur (2001): The Metalanguage lambda-Prolog and Its Implementation. In: Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings, pp. 1–20, doi:10.1007/3-540-44716-4_1.
  21. Ulf Norell (2007): Towards a Practical Programming Language Based on Dependent Type Theory. Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden.
  22. Frank Pfenning & Carsten Schürmann (1999): System Description: Twelf - A Meta-Logical Framework for Deductive Systems. In: Harald Ganzinger: Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, Lecture Notes in Computer Science 1632. Springer-Verlag, pp. 202–206, doi:10.1007/3-540-48660-7_14.
  23. Jeff Polakow & Frank Pfenning (1999): Natural Deduction for Intuitionistic Non-communicative Linear Logic. In: Jean-Yves Girard: Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings, Lecture Notes in Computer Science 1581. Springer-Verlag, pp. 295–309, doi:10.1007/3-540-48959-2_21.
  24. François-Régis Sinot (2005): Director Strings Revisited: A Generic Approach to the Efficient Representation of Free Variables in Higher-order Rewriting. Journal of Logic and Computation 15(2), pp. 201–218, doi:10.1093/logcom/exi010.
  25. Kevin Watkins, Iliano Cervesato, Frank Pfenning & David Walker (2003): A concurrent logical framework I: Judgements and properties. Technical Report. School of Computer Science, Carnegie Mellon University, Pittsburgh.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org