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

DOI10.1007/s10817-019-09527-xzbMath1468.68330arXiv1812.03624OpenAlexW2904404870WikidataQ127635232 ScholiaQ127635232MaRDI QIDQ2331074

Mohamed Yousri Mahmoud, Amy P. Felty

Publication date: 25 October 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1812.03624

zbMATH Keywords

linear logichigher-order abstract syntaxCoqHybridquantum programming languagesProto-Quipper

Mathematics Subject Classification ID

Quantum computation (81P68) Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (4)

Towards substructural property-based testing ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Formalization of metatheory of the Quipper quantum programming language in a linear logic ⋮ A focused linear logical framework and its application to metatheory of object logics

Uses Software

• Coq
• HYBRID
• Beluga
• Twelf
• Abella
• Quipper
• Forest
• QML
• Lolli

Cites Work

• Unnamed Item
• Unnamed Item
• 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
• Forum: A multiple-conclusion specification logic
• Quantum implicit computational complexity
• Logic programming in a fragment of intuitionistic linear logic
• A linear logical framework
• Formalization of metatheory of the Quipper quantum programming language in a linear logic
• Formal meta-level analysis framework for quantum programming languages
• An Overview of QML With a Concrete Implementation in Haskell
• An Introduction to Quantum Programming in Quipper
• Programming with Higher-Order Logic
• On quantum lambda calculi: a foundational perspective
• The representational adequacy of <scp>Hybrid</scp>
• A Categorical Model for a Quantum Circuit Description Language (Extended Abstract)
• Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
• The Abella Interactive Theorem Prover (System Description)
• On a measurement-free quantum lambda calculus with classical control
• A framework for defining logics
• Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
• Enriching a Linear/Non-linear Lambda Calculus
• A lambda calculus for quantum computation with classical control
• Reasoning with higher-order abstract syntax in a logical framework
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)

This page was built for publication: Formalization of metatheory of the Quipper quantum programming language in a linear logic