The Coq mailing list

[Robert Rand <rrand AT seas.upenn.edu>]

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

On Thu, Dec 20, 2018 at 11:54 PM José Manuel Rodriguez Caballero <josephcmac AT gmail.com> wrote:

Hello,

  In Robert Rand's PhD thesis

http://www.cs.umd.edu/~rrand/thesis.pdf

quantum programs were verified using a tool known as Qwire. The semantics of Qwire was verified in Coq. Other authors have previously used Isabelle/HOL in order to verify semantical structures related to Quantum Computing. My question is rather type-theoretical: 

Does Calculus of Inductive Constructions have some advantages over Simple Type Theory in order to formally verify quantum programs? 

In other words: 

Was the verification of Qwire in Coq an arbitrary choice among all the proof assistants available right now or are there deep theoretical reasons for this precise choice?

Kind Regards,

José M.