# A HoTT Quantum Equational Theory (Extended Version)

@article{Paykin2019AHQ, title={A HoTT Quantum Equational Theory (Extended Version)}, author={Jennifer Paykin and Steve Zdancewic}, journal={ArXiv}, year={2019}, volume={abs/1904.04371} }

This paper presents an equational theory for the QRAM model of quantum computation, formulated as an embedded language inside of homotopy type theory. The embedded language approach is highly expressive, and reflects the style of state-of-the art quantum languages like Quipper and QWIRE. The embedding takes advantage of features of homotopy type theory to encode unitary transformations as higher inductive paths, simplifying the presentation of an equational theory. We prove that this equational… Expand

#### One Citation

Quantum Temporal Logic: from Birkhoff and von Neumann to Pnueli

- Mathematics, Computer Science
- 2019

A model of quantum concurrent program is introduced, which can be used to model the behaviour of reactive quantum systems and to design quantum compilers, and a quantum Bohm-Jacopini theorem is proved which states that any such program is equivalent to a Q-While program. Expand

#### References

SHOWING 1-10 OF 40 REFERENCES

Algebraic Effects, Linearity, and Quantum Programming Languages

- Computer Science
- POPL 2015
- 2015

A new elementary algebraic theory of quantum computation, built from unitary gates and measurement is presented, and an equational theory for a quantum programming language is extracted from thegebraic theory. Expand

An Algebra of Pure Quantum Programming

- Physics, Computer Science
- Electron. Notes Theor. Comput. Sci.
- 2007

A sound and complete equational theory for the functional quantum programming language QML, omitting measurements is developed and the completeness proof gives rise to a normalisation algorithm following the normalisation-by-evaluation approach. Expand

On a Fully Abstract Model for a Quantum Linear Functional Language: (Extended Abstract)

- Computer Science
- Electron. Notes Theor. Comput. Sci.
- 2008

This paper studies the linear fragment of the programing language for quantum computation with classical control described in, and sketches the language, and describes a fully abstract denotational semantics based on completely positive maps. Expand

Semantics of Higher-Order Quantum Computation via Geometry of Interaction

- Computer Science, Mathematics
- 2011 IEEE 26th Annual Symposium on Logic in Computer Science
- 2011

The proposed denotational model is the first one that supports the full features of a quantum functional programming language, and it is proved adequacy of the semantics is achieved. Expand

Quantum computation and quantum information

- Mathematics, Computer Science
- Mathematical Structures in Computer Science
- 2007

This special issue of Mathematical Structures in Computer Science contains several contributions related to the modern field of Quantum Information and Quantum Computing. The first two papers deal… Expand

The Arrow Calculus as a Quantum Programming Language

- Computer Science, Mathematics
- WoLLIC
- 2009

This framework expresses quantum programming using well-understood and familiar classical patterns for programming in the presence of computational effects using the arrow calculus extended with monadic constructions. Expand

A Double Effect λ-calculus for Quantum Computation

- Mathematics, Computer Science
- SBLP
- 2013

This paper presents a double effect version of the simply typed λ-calculus where it allows to express quantum algorithms including reversible operations over pure states and measurements in the middle of the computation using a traditional style of functional programming and reasoning. Expand

Quipper: a scalable quantum programming language

- Computer Science
- PLDI 2013
- 2013

Quipper, a scalable, expressive, functional, higher-order quantum programming language, which is geared towards a model of computation that uses a classical computer to control a quantum device, but is not dependent on any particular model of quantum hardware. Expand

Applying quantitative semantics to higher-order quantum computing

- Computer Science, Physics
- POPL 2014
- 2013

This paper proposes a denotational semantics for a quantum lambda calculus with recursion and an infinite data type, using constructions from quantitative semantics of linear logic. Expand

The HoTT library: a formalization of homotopy type theory in Coq

- Computer Science, Mathematics
- CPP
- 2017

We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher… Expand