Scalar System F for linear-algebraic -calculus: towards a quantum physical logic

DOI10.1016/J.ENTCS.2011.01.033MaRDI QIDQ2825375zbMATH OpenOpenAlexWikidataFDO

Authors Pablo Arrighi, Alejandro Díaz-Caro

Publication date 7 October 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2011.01.033

zbMATH Keywords

quantum logictype theoryCurry-Howard isomorphismprobabilistic lambda calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logical foundations of quantum mechanics; quantum logic (quantum-theoretic aspects) (81P10)

Recommendations

• A System F accounting for scalars
• A type system for the vectorial aspect of the linear-algebraic lambda-calculus
• The vectorial \(\lambda\)-calculus
• Linear-algebraic λ-calculus: higher-order, encodings, and confluence.
• Confluence via strong normalisation in an algebraic \(\lambda\)-calculus with rewriting

Cites work

• scientific article; zbMATH DE number 1256737 (Why is no real title available?)
• An algebra of pure quantum programming
• Bounded linear logic: A modular approach to polynomial-time computability
• Functional and Logic Programming
• Lectures on the Curry-Howard isomorphism
• Linear logic
• Linear-algebraic λ-calculus: higher-order, encodings, and confluence.
• Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer
• Probabilistic  -calculus and Quantitative Program Analysis
• Quantum programming languages: survey and bibliography

Cited in

(6)

• Linear-algebraic λ-calculus: higher-order, encodings, and confluence.
• A type system for the vectorial aspect of the linear-algebraic lambda-calculus
• A System F accounting for scalars
• Realizability in the unitary sphere
• Linear lambda-calculus is linear
• The vectorial \(\lambda\)-calculus

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Scalar System F for linear-algebraic \(\lambda\)-calculus: towards a quantum physical logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2825375)