Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic

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 quantum programming language u...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2019-12, Vol.63 (4), p.967-1002
Main Authors: Mahmoud, Mohamed Yousri, Felty, Amy P.
Format: Article
Language:English
Subjects:
Artificial Intelligence
Computer Science
Hybrid systems
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Programming languages
Quantum computing
Semantics
Symbolic and Algebraic Manipulation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 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 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.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-019-09527-x