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

TL;DR

This paper formalizes the metatheory of the Proto-Quipper quantum programming language within a linear logical framework, enabling rigorous reasoning about its type system and semantics using the Hybrid system and Coq.

Contribution

It introduces a linear specification logic in Hybrid to formalize and verify the type soundness of Proto-Quipper, a core subset of Quipper, within Coq.

Findings

Formal encoding of Proto-Quipper's semantics and typing rules

Proof of type soundness within the linear logical framework

Extension of Hybrid with linear specification logic for quantum languages

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.