1. Thorsten Altenkirch & Jonathan J. Grattage (2005): A functional quantum programming language. In: Proceedings of LICS-2005. IEEE Computer Society, pp. 249–258, doi:10.1109/LICS.2005.1. Available at
  2. Pablo Arrighi & Alejandro Díaz-Caro (2011): Scalar system F for linear-algebraic lambda-calculus: towards a quantum physical logic. In: Bob Coecke, Prakash Panangaden & Peter Selinger: Proceedings of QPL-2009, Electronic Notes in Theoretical Computer Science 270/2. Elsevier, pp. 219–229, doi:10.1016/j.entcs.2011.01.033. Available at
  3. Pablo Arrighi & Gilles Dowek (2008): Linear-algebraic lambda-calculus: higher-order, encodings, and confluence. In: Andrei Voronkov: Proceedings of RTA-2008, Lecture Notes in Computer Science 5117. Springer, pp. 17–31, doi:10.1007/978-3-540-70590-1_2. Available at
  4. Henk P. Barendregt (1992): Lambda-calculi with types. Handbook of Logic in Computer Science II. Oxford University Press.
  5. Alejandro Díaz-Caro, Simon Perdrix, Christine Tasson & Benoît Valiron (2010): Equivalence of algebraic lambda-calculi. In: Proceedings of the 5th International Workshop on Higher-Order Rewriting, HOR-2010, Edinburgh, UK, pp. 6–11. Available at
  6. Alejandro Díaz-Caro & Barbara Petit (2012): Linearity in the non-deterministic call-by-value setting. In: Luke Ong & Ruy de Queiroz: Proceedings of WoLLIC-2012, Lecture Notes in Computer Science 7456. Springer, pp. 216–231. Available at To appear.
  7. Thomas Ehrhard & Laurent Regnier (2003): The differential lambda-calculus. Theoretical Computer Science 309(1), pp. 1–41, doi:10.1016/S0304-3975(03)00392-X.
  8. Jean-Yves Girard, Yves Lafont & Paul Taylor (1989): Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press. Available at
  9. Jean-Pierre Jouannaud & Hélène Kirchner (1986): Completion of a set of rules modulo a set of equations. SIAM Journal on Computing 15(4), pp. 1155–1194, doi:10.1145/800017.800519.
  10. Jean-Louis Krivine (1990): Lambda-calcul: Types et Modèles. Études et Recherches en Informatique. Masson.
  11. Christine Tasson (2009): Algebraic totality, towards completeness. In: Pierre-Louis Curien: Proceedings of TLCA-2009, Lecture Notes in Computer Science 5608. Springer, pp. 325–340, doi:10.1007/978-3-642-02273-9_24. Available at
  12. TeReSe (2003): Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science 55. Cambridge University Press.
  13. The Coq Development Team (2010): Reference Manual, 8.3 edition. INRIA. Available at
  14. André van Tonder (2004): A Lambda-calculus for quantum computation. SIAM Journal of Computing 33, pp. 1109–1135, doi:10.1137/S0097539703432165. Available at
  15. Benoît Valiron (2010): Orthogonality and algebraic lambda-calculus. In: Proceedings of the 7th International Workshop on Quantum Physics and Logic, QPL-2010, Oxford, UK, pp. 169–175. Available at
  16. Benoît Valiron (2011): Local confluence of the algebraic fragment: proof in COQ. Available at
  17. Lionel Vaux (2009): The algebraic lambda-calculus. Mathematical Structures in Computer Science 19(5), pp. 1029–1059, doi:10.1017/S0960129509990089. Available at

Comments and questions to:
For website issues: