Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic
In: Journal of Automated Reasoning, Jg. 63 (2019-06-22), S. 967-1002
Online
unknown
Zugriff:
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.
40 pages, 5 figures
Titel: |
Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic
|
---|---|
Autor/in / Beteiligte Person: | Mohamed Yousri Mahmoud ; Felty, Amy P. |
Link: | |
Zeitschrift: | Journal of Automated Reasoning, Jg. 63 (2019-06-22), S. 967-1002 |
Veröffentlichung: | Springer Science and Business Media LLC, 2019 |
Medientyp: | unknown |
ISSN: | 1573-0670 (print) ; 0168-7433 (print) |
DOI: | 10.1007/s10817-019-09527-x |
Schlagwort: |
|
Sonstiges: |
|