@inproceedings(AltenkirchGrattageLICS05,
 author       = "Thorsten Altenkirch and Jonathan J. Grattage",
 year         = "2005",
 title        = "A functional quantum programming language",
 booktitle    = "Proceedings of {LICS}-2005",
 publisher    = "IEEE Computer Society",
 pages        = "249--258",
 doi          = "10.1109/LICS.2005.1",
 url          = "http://arxiv.org/abs/quant-ph/0409065",
)
@inproceedings(ArrighiDiazcaroQPL09,
 author       = "Pablo Arrighi and Alejandro D{\'\i }az-Caro",
 year         = "2011",
 title        = "Scalar system {F} for linear-algebraic lambda-calculus: towards a quantum physical logic",
 editor       = "Bob Coecke and Prakash Panangaden and Peter Selinger",
 booktitle    = "Proceedings of {QPL}-2009",
 series       = "Electronic Notes in Theoretical Computer Science",
 volume       = "270/2",
 publisher    = "Elsevier",
 pages        = "219--229",
 doi          = "10.1016/j.entcs.2011.01.033",
 url          = "http://arxiv.org/abs/0903.3741",
)
@inproceedings(ArrighiDowekRTA08,
 author       = "Pablo Arrighi and Gilles Dowek",
 year         = "2008",
 title        = "Linear-algebraic lambda-calculus: higher-order, encodings, and confluence",
 editor       = "Andrei Voronkov",
 booktitle    = "Proceedings of {RTA}-2008",
 series       = "Lecture Notes in Computer Science",
 volume       = "5117",
 publisher    = "Springer",
 pages        = "17--31",
 doi          = "10.1007/978-3-540-70590-1\_2",
 url          = "http://arxiv.org/abs/quant-ph/0612199",
)
@book(Barendregt92,
 author       = "Henk P. Barendregt",
 year         = "1992",
 title        = "Lambda-calculi with types",
 series       = "Handbook of Logic in Computer Science",
 volume       = "{II}",
 publisher    = "Oxford University Press",
)
@inproceedings(DiazcaroPerdrixTassonValironHOR10,
 author       = "Alejandro D\'iaz-Caro and Simon Perdrix and Christine Tasson and Beno\^it Valiron",
 year         = "2010",
 title        = "Equivalence of algebraic lambda-calculi",
 booktitle    = "Proceedings of the 5th International Workshop on Higher-Order Rewriting, {HOR}-2010",
 address      = "Edinburgh, UK",
 pages        = "6--11",
 url          = "http://arxiv.org/abs/1005.2897",
)
@inproceedings(DiazcaroPetitWoLLIC12,
 author       = "Alejandro D\'iaz-Caro and Barbara Petit",
 year         = "2012",
 title        = "Linearity in the non-deterministic call-by-value setting",
 editor       = "Luke Ong and Ruy de Queiroz",
 booktitle    = "Proceedings of {WoLLIC}-2012",
 series       = "Lecture Notes in Computer Science",
 volume       = "7456",
 publisher    = "Springer",
 pages        = "216--231",
 url          = "http://arxiv.org/abs/1011.3542",
 note         = "To appear",
)
@article(EhrhardRegnierTCS03,
 author       = "Thomas Ehrhard and Laurent Regnier",
 year         = "2003",
 title        = "The differential lambda-calculus",
 journal      = "Theoretical Computer Science",
 volume       = "309",
 number       = "1",
 pages        = "1--41",
 doi          = "10.1016/S0304-3975(03)00392-X",
)
@book(GirardLafontTaylor89,
 author       = "Jean-Yves Girard and Yves Lafont and Paul Taylor",
 year         = "1989",
 title        = "Proofs and Types",
 series       = "Cambridge Tracts in Theoretical Computer Science",
 volume       = "7",
 publisher    = "Cambridge University Press",
 url          = "http://www.paultaylor.eu/stable/Proofs+Types.html",
)
@article(JouannaudKirchnerSIAM86,
 author       = "Jean-Pierre Jouannaud and H\'el\`ene Kirchner",
 year         = "1986",
 title        = "Completion of a set of rules modulo a set of equations",
 journal      = "SIAM Journal on Computing",
 volume       = "15",
 number       = "4",
 pages        = "1155--1194",
 doi          = "10.1145/800017.800519",
)
@book(Krivine90,
 author       = "Jean-Louis Krivine",
 year         = "1990",
 title        = "Lambda-calcul: Types et Mod{\`e}les",
 series       = "{\'E}tudes et Recherches en Informatique",
 publisher    = "Masson",
)
@inproceedings(TassonTLCA09,
 author       = "Christine Tasson",
 year         = "2009",
 title        = "Algebraic totality, towards completeness",
 editor       = "Pierre-Louis Curien",
 booktitle    = "Proceedings of {TLCA}-2009",
 series       = "Lecture Notes in Computer Science",
 volume       = "5608",
 publisher    = "Springer",
 pages        = "325--340",
 doi          = "10.1007/978-3-642-02273-9\_24",
 url          = "http://arxiv.org/abs/0912.2349",
)
@book(terese03,
 author       = "{TeReSe}",
 year         = "2003",
 title        = "Term Rewriting Systems",
 series       = "Cambridge Tracts in Theoretical Computer Science",
 volume       = "55",
 publisher    = "Cambridge University Press",
)
@manual(ManualCOQ,
 author       = "{The Coq Development Team}",
 year         = "2010",
 title        = "Reference Manual",
 edition      = "8.3",
 organization = "INRIA",
 url          = "http://coq.inria.fr/doc",
)
@article(tonder04lambda,
 author       = "Andr{\'e} van Tonder",
 year         = "2004",
 title        = "A Lambda-calculus for quantum computation",
 journal      = "SIAM Journal of Computing",
 volume       = "33",
 pages        = "1109--1135",
 doi          = "10.1137/S0097539703432165",
 url          = "http://arxiv.org/abs/quant-ph/0307150",
)
@inproceedings(ValironQPL10,
 author       = "Beno{\^\i }t Valiron",
 year         = "2010",
 title        = "Orthogonality and algebraic lambda-calculus",
 booktitle    = "Proceedings of the 7th International Workshop on Quantum Physics and Logic, {QPL}-2010",
 address      = "Oxford, UK",
 pages        = "169--175",
 url          = "http://www.cs.ox.ac.uk/people/bob.coecke/QPL_proceedings.html",
)
@misc(BenCoqProof,
 author       = "Beno\^it Valiron",
 year         = "2011",
 title        = "Local confluence of the algebraic fragment: proof in COQ",
 url          = "http://www.monoidal.net/vectorial-lvec-coqproof.tar.bz2",
)
@article(VauxMSCS09,
 author       = "Lionel Vaux",
 year         = "2009",
 title        = "The algebraic lambda-calculus",
 journal      = "Mathematical Structures in Computer Science",
 volume       = "19",
 number       = "5",
 pages        = "1029--1059",
 doi          = "10.1017/S0960129509990089",
 url          = "http://hal.archives-ouvertes.fr/hal-00379750",
)