The Coq mailing list

[José Manuel Rodriguez Caballero <josephcmac AT gmail.com>]

Robert wrote:
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).

Hi Robert,

  My references to Isabelle/HOL in quantum computing are the following ones (I am a beginner in this subject):

• Unruh's Quantum Relational Hoare Logic https://arxiv.org/pdf/1802.03188.pdf
  
• Anthony Bordg's Isabelle marries Dirac https://github.com/AnthonyBordg/Isabelle_marries_Dirac
  

My main concerns in the choice between dependent type theory and simple type theory for the formalization of a mathematical idea are Lawrence Paulson's arguments for simple type theory as the most natural formal system for the formalization of traditional mathematics: https://arxiv.org/pdf/1804.07860.pdf

For example, I quote from this last paper: "My personal disenchantment with dependent type theories coincides with the decision to shift from extensional to intensional equality. This meant for example that 0+n = n and n+0 = n would henceforth be regarded as fundamentally different assertions". Indeed, Isabelle began with dependent type theory, more precisely, constructive type theory (Isabelle/CTT), and only later it changed to simple type theory (Isabelle/HOL).

I will read the argument according to which matrices should be dependently typed and I will compare it with Paulson's arguments for simple type theory as the most natural formal system for mathematics, in the case of matrices: http://isabelle.in.tum.de/library/HOL/HOL-Matrix_LP/Matrix.html

Thank you for the references.

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

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.