[isabelle] Quantum Computing. Contents of Cl-isabelle-users digest, Vol 159, Issue 10

[Anthony Bordg]

Hello Sidi,

thank you for pointing this out.

Larry, it's an opportunity for you to contribute to my library ! :)

cheers
Anthony

Hello Anthony,
There is a formalization of quantum mechanics which is part of a HOL Light
library of complex function vector spaces (
https://github.com/jrh13/hol-light/tree/master/Functionspaces). Using
this library, a tool for the verification of optical quantum circuits was
developed (https://github.com/beillahi/FMV-QC-HOL).
Yours Sincerely
Sidi Mohamed
Message: 2
Date: Fri, 7 Sep 2018 00:27:19 -0400
Subject: [isabelle] [Isabelle] Re: Quantum Computing
<CAA8xVUhNUK9rR7F=
Content-Type: text/plain; charset="UTF-8"

I would like to point out a project I started a few weeks ago in case

some

of you might be interested. It is a formalization of quantum computing
<https://github.com/AnthonyBordg/Isabelle_marries_Dirac> in Isabelle.
I should add a README file soon, but in the meantime if you have any
question please ask, you can also drop me an email.
Best regards
Anthony

There is a new paradigm in quantum mechanics, known as ER = EPR, which is
very important in contemporary physics and it is entering in mathematics
and computer science. There are many papers about this subject, some of
them involving quantum computing. So, to write a library in order to
provide mathematical tools in Isabelle/HOL for physicists about ER = EPR
will be very useful. Nevertheless, a library about the unique
infinite-dimensional separable Hilbert spaces is required as preliminary. A
library about non-commutative geometry, although it is not essential, it
will be helpful for such a project.
Paper: https://arxiv.org/pdf/1306.0533.pdf
Video:

Kind Regards,
Jose M.
End of Cl-isabelle-users Digest, Vol 159, Issue 10
*************************************************