A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus

Conference object, Article, Preprint English OPEN

Arrighi, Pablo; Díaz-Caro, Alejandro; Valiron, Benoît;

(2011)

Publisher: Open Publishing Association

Journal: Electronic Proceedings in Theoretical Computer Science (issn: 2075-2180)

Publisher copyright policies & self-archiving

Related identifiers: doi: 10.4204/EPTCS.88.1
Subject: [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO] | [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] | Mathematics | Electronic computers. Computer science | Computer Science - Logic in Computer Science | QA1-939 | QA75.5-76.95

In Proceedings DCM 2011, arXiv:1207.6821; International audience; We describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the part of the language emulating linear operators and vectors, i.e. it is able to statically describe the... View more

References (17)
17 references, page 1 of 2
1
2
[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 http://arxiv.org/abs/quant-ph/0409065.
[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, editors: 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 http://arxiv.org/abs/0903.3741.
[3] Pablo Arrighi & Gilles Dowek (2008): Linear-algebraic lambda-calculus: higher-order, encodings, and confluence. In Andrei Voronkov, editor: 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 http://arxiv.org/abs/quant-ph/ 0612199.
[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 http://arxiv.org/abs/1005.2897.
[6] Alejandro D´ıaz-Caro & Barbara Petit (2012): Linearity in the non-deterministic call-by-value setting. In Luke Ong & Ruy de Queiroz, editors: Proceedings of WoLLIC-2012, Lecture Notes in Computer Science 7456, Springer, pp. 216-231. Available at http://arxiv.org/abs/1011.3542. 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 http://www.paultaylor.eu/stable/ Proofs+Types.html.
[9] Jean-Pierre Jouannaud & He´le`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 Mode`les. E´ tudes et Recherches en Informatique, Masson.

Similar Research Results (9)

publication A System F accounting for scalars (2009)	98%
publication Linearity in the non-deterministic call-by-value setting (2012)	95%
publication The Vectorial $\lambda$-Calculus (2013)	95%
publication Linear-algebraic lambda-calculus (2005)	91%
other Approximations of Isomorphism and Logics with Linear-Algebraic Operators (2019)	82%
publication A Linear-algebraic Proof of Hilbert's Ternary Quartic Theorem (2019)	80%
publication Linear VSS and Distributed Commitments Based on Secret Sharing and Pairwise Checks (2002)	78%
publication Approximations of Isomorphism and Logics with Linear-Algebraic Operators (2019)	74%
publication Optimal rate list decoding over bounded alphabets using algebraic-geometric codes (2017)	71%

Related Organizations (1)
University of Paris 13 (Paris North)
88%
Metrics

Share - Bookmark

Download from
INRIA a CCSD electronic archive server via INRIA a CCSD electronic archive server (Conference object, 2011)
Electronic Proceedings in Theoretical Computer Science via DOAJ-Articles (Article, 2012)
arXiv.org e-Print Archive via arXiv.org e-Print Archive (Preprint, 2010)
Hyper Article en Ligne via Hyper Article en Ligne (Conference object, 2011)
HAL-ENS-LYON via HAL-ENS-LYON (Conference object, 2011)
View more
Cite this publication