Formalization of metatheory of the Quipper quantum programming language in a linear logic
From MaRDI portal
Publication:2331074
Abstract: We develop a linear logical framework within the Hybrid system and use it to reason about the type system of a quantum lambda calculus. In particular, we consider a practical version of the calculus called Proto-Quipper, which contains the core of Quipper. Quipper is a new quantum programming language under active development and recently has gained much popularity among the quantum computing communities. Hybrid is a system that is designed to support the use of higher-order abstract syntax (HOAS) for representing and reasoning about formal systems implemented in the Coq Proof Assistant. In this work, we extend the system with a linear specification logic (SL) in order to reason about the linear type system of Quipper. To this end, we formalize the semantics of Proto-Quipper by encoding the typing and evaluation rules in the SL, and prove type soundness.
Recommendations
Cites work
- \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq
- A categorical model for a quantum circuit description language (extended abstract)
- A framework for defining logics
- A lambda calculus for quantum computation with classical control
- A linear logical framework
- An introduction to quantum programming in Quipper
- An overview of QML with a concrete implementation in Haskell
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- Enriching a linear/non-linear lambda calculus: a programming language for string diagrams
- Formal meta-level analysis framework for quantum programming languages
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Forum: A multiple-conclusion specification logic
- scientific article; zbMATH DE number 1692891 (Why is no real title available?)
- scientific article; zbMATH DE number 2185657 (Why is no real title available?)
- scientific article; zbMATH DE number 1927412 (Why is no real title available?)
- scientific article; zbMATH DE number 2134912 (Why is no real title available?)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Logic programming in a fragment of intuitionistic linear logic
- On a measurement-free quantum lambda calculus with classical control
- On quantum lambda calculi: a foundational perspective
- Programming with higher-order logic.
- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
- Quantum implicit computational complexity
- Reasoning with higher-order abstract syntax in a logical framework
- The Abella Interactive Theorem Prover (System Description)
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- The representational adequacy of Hybrid
Cited in
(7)- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Formal meta-level analysis framework for quantum programming languages
- \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq
- scientific article; zbMATH DE number 910433 (Why is no real title available?)
- A focused linear logical framework and its application to metatheory of object logics
- POPLMark reloaded: mechanizing proofs by logical relations
- Towards substructural property-based testing
This page was built for publication: Formalization of metatheory of the Quipper quantum programming language in a linear logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2331074)
