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
..........................................................................................................................
Dr David Michael Roberts
School of Mathematical Sciences, University of Adelaide, Australia  5005
Email: david.roberts@adelaide.edu.au

CRICOS Provider Number 00123M
IMPORTANT: This message may contain confidential or legally privileged
information.  If you think it was sent to you by mistake,  please delete all
copies and advise the sender.  For the purposes of the SPAM Act 2003, this
email is authorised by The University of Adelaide.
..........................................................................................................................
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.