Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
* [HoTT] Quantum Computations and HoTT
@ 2018-12-14  4:06 José Manuel Rodriguez Caballero
       [not found] ` <20181214071146.GA19128@pachax.iitpkd.ac.in>
                   ` (2 more replies)
  0 siblings, 3 replies; 4+ messages in thread
From: José Manuel Rodriguez Caballero @ 2018-12-14  4:06 UTC (permalink / raw)
  To: HomotopyTypeTheory

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

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.

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

^ permalink raw reply	[flat|nested] 4+ messages in thread

* Re: [HoTT] Quantum Computations and HoTT
       [not found] ` <20181214071146.GA19128@pachax.iitpkd.ac.in>
@ 2018-12-17  3:06   ` José Manuel Rodriguez Caballero
  0 siblings, 0 replies; 4+ messages in thread
From: José Manuel Rodriguez Caballero @ 2018-12-17  3:06 UTC (permalink / raw)
  To: HomotopyTypeTheory

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

Thank you ppk for the reference. My main suspicion that HoTT may be useful
in Quantum Computing is the idea of the topological quantum computer,
although, it is just a suspicion, not a claim:
 https://en.wikipedia.org/wiki/Topological_quantum_computer

Kind Regards,
José M.


El vie., 14 dic. 2018 a las 2:11, Piyush P Kurur (<ppk@iitpkd.ac.in>)
escribió:

> On Thu, Dec 13, 2018 at 11:06:37PM -0500, José Manuel Rodriguez Caballero
> 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?
>
>
> What probably would be interesting is the linear variant of the type
> theory (whether it is Hott or the standard type theory a la Coq).
>
> https://arxiv.org/pdf/1210.0613.pdf
>
> I have not really followed this line of research and hence have
> nothing intelligent to contribute but if you find something
> interesting or you already have some project going on, please do let
> me know.
>
> Regards,
>
> ppk
>
> >
> > 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: 2897 bytes --]

^ permalink raw reply	[flat|nested] 4+ messages in thread

* Re: [HoTT] Quantum Computations and HoTT
  2018-12-14  4:06 [HoTT] Quantum Computations and HoTT José Manuel Rodriguez Caballero
       [not found] ` <20181214071146.GA19128@pachax.iitpkd.ac.in>
@ 2018-12-21  4:09 ` David Roberts
       [not found] ` <CAFL+ZM9aN8ZuPb8TAXjqR1CJ5t2euwaFGBksu=B9FcUc_x1ghg@mail.gmail.com>
  2 siblings, 0 replies; 4+ messages in thread
From: David Roberts @ 2018-12-21  4:09 UTC (permalink / raw)
  To: josephcmac; +Cc: homotopytypetheory

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

^ permalink raw reply	[flat|nested] 4+ messages in thread

* Re: [HoTT] Quantum Computations and HoTT
       [not found] ` <CAFL+ZM9aN8ZuPb8TAXjqR1CJ5t2euwaFGBksu=B9FcUc_x1ghg@mail.gmail.com>
@ 2018-12-21  4:10   ` José Manuel Rodriguez Caballero
  0 siblings, 0 replies; 4+ messages in thread
From: José Manuel Rodriguez Caballero @ 2018-12-21  4:10 UTC (permalink / raw)
  To: david.roberts; +Cc: HomotopyTypeTheory

[-- 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 --]

^ permalink raw reply	[flat|nested] 4+ messages in thread

end of thread, back to index

Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-12-14  4:06 [HoTT] Quantum Computations and HoTT José Manuel Rodriguez Caballero
     [not found] ` <20181214071146.GA19128@pachax.iitpkd.ac.in>
2018-12-17  3:06   ` José Manuel Rodriguez Caballero
2018-12-21  4:09 ` David Roberts
     [not found] ` <CAFL+ZM9aN8ZuPb8TAXjqR1CJ5t2euwaFGBksu=B9FcUc_x1ghg@mail.gmail.com>
2018-12-21  4:10   ` José Manuel Rodriguez Caballero

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox