Formal meta-level analysis framework for quantum programming languages

DOI10.1016/j.entcs.2018.10.012zbMath1433.68078OpenAlexW2899277158WikidataQ113317503 ScholiaQ113317503MaRDI QIDQ2333324

Mohamed Yousri Mahmoud, Amy P. Felty

Publication date: 12 November 2019

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

zbMATH Keywords

linear logichybridCoqquantum lambda calculus

Mathematics Subject Classification ID

Quantum computation (81P68) Theory of programming languages (68N15) Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Unnamed Item, Formalization of metatheory of the Quipper quantum programming language in a linear logic

Uses Software

• Coq
• HYBRID
• Quipper
• YALLA
• qGCL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Formalized meta-theory of sequent calculi for substructural logics
• On quantum lambda calculi: a foundational perspective
• The representational adequacy of <scp>Hybrid</scp>
• Logic Programming with Focusing Proofs in Linear Logic
• Parametric higher-order abstract syntax for mechanized semantics
• A Double Effect λ-calculus for Quantum Computation
• A lambda calculus for quantum computation with classical control
• Reasoning with higher-order abstract syntax in a logical framework