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

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

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

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