Re: [HoTT] Quantum Computations and HoTT

[David Roberts <droberts.65537@gmail.com>]

[resending from correct email address for the list]

Hi José

see for example this thesis on formally-verified quantum programming

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

Here's a sample from the abstract

"We argue that quantum programs demand machine-checkable proofs of correctness.
We justify this on the basis of the complexity of programs manipulating quantum
states, the expense of running quantum programs, and the inapplicability of
traditional debugging techniques to programs whose states cannot be examined. We
further argue that the existing mathematical models of quantum computation make
this an easier task than one could reasonably expect. In light of
these observations
we introduce Qwire, a tool for writing verifiable, large scale quantum programs.

Qwire is not merely a language for writing and verifying quantum
circuits: it is a
verified circuit description language. This means that the semantics of
Qwire circuits are verified in the Coq proof assistant. We also
implement verified abstractions, like
ancilla management and reversible circuit compilation. Finally, we turn
Qwire and Coq’s abilities outwards, towards verifying popular quantum
algorithms like quantum
teleportation. We argue that this tool provides a solid foundation for
research into
quantum programming languages and formal verification going forward."

Cheers,
David



David Roberts
http://ncatlab.org/nlab/show/David+Roberts
On Fri, 14 Dec 2018 at 14:36, José Manuel Rodriguez Caballero
<josephcmac@gmail.com> wrote:
>
> Hello,
>   I am interested in the formal verification of theorems related to Quantum Computations. I have two possibilities in order to do my formalizations: either I can use simple type theory (Isabelle/HOL) or I can use UniMath (Coq). Does the homotopy type theory has some advantage over the simple type theory in this field?
>
> Kind Regards,
> José M.
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.