Re: [HoTT] Quantum Computations and HoTT

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

[-- Attachment #1: Type: text/plain, Size: 3485 bytes --]

Thank you for this thesis: since February 2019 I will be working in a
similar project.

Kind Regards,
José M.

El jue., 20 dic. 2018 a las 23:04, David Roberts (<a1078662@adelaide.edu.au>)
escribió:

> 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.
>

-- 
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.

[-- Attachment #2: Type: text/html, Size: 4460 bytes --]