The Coq mailing list

[José Manuel Rodríguez Caballero <josephcmac AT gmail.com>]

Hi,

  Beside the argument about the advantages of dependent types for the formalization of matrices, another argument to use Coq in quantum computing may be the fact that Coq does not assume the law of excluded middle. So, I guess that Coq will be more natural in order to formalize the quantum toposophy (roughly speaking, this is a program in order to preserve the distributivity in Birkhoff-von Neumann quantum logic via topos). Here a reference to this theory:

https://link.springer.com/chapter/10.1007/978-3-319-51777-3_12

  I would appreciate some references to repositories of quantum toposophy in Coq (or another proof assistant), if there is any. Thank you in advance.

Kind Regards,

José M.

El vie., 21 dic. 2018 a las 14:08, Robert Rand (<rrand AT seas.upenn.edu>) escribió:

Hi José,

I'd say that the reason for the choice of Coq was its dependent types for programming, rather than the power of its logic.

Dependent types allow us to define precise circuit families. Consider for instance the type signature for the quantum fourier transform from our POPL paper (http://www.cs.umd.edu/~rrand/popl_2017.pdf, section 6.2, which discusses this choice):

fourier : Π(n:Nat). CIRC(n ⨂ qubit, n ⨂ qubit)

The argument n here is both used in the QFT and precisely specifies the arity of the circuit. When taking the denotation, then, we know that the QFT takes a density matrix of size 2^n by 2^n to another matrix of the same size, which helps in verification. 

(In general, there's a pretty strong argument that matrices should be dependently typed, as the Mathematical Components/SSReflect matrices are, though in the context of QWIRE we had to make some trade-offs discussed here: http://www.cs.umd.edu/~rrand/coqpl_2018.pdf.)

We're not the first to argue for dependent types in quantum programs: The idea is present in the Quipper papers and discussed at length in Alexander Green's thesis (which also does some verification in Agda).

I'm curious, though, about prior uses of Isabelle/HOL for quantum computing. I'm only familiar with two works in that category (Liu et al's Theorem Prover for Quantum Hoare Logic and Its Applications and Unruh's Quantum Relational Hoare Logic) and both are in early stages (in terms of verification in Isabelle).

Best,

Robert