From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-vs1-xe37.google.com (mail-vs1-xe37.google.com [IPv6:2607:f8b0:4864:20::e37]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2db91b95 for ; Fri, 21 Dec 2018 04:10:51 +0000 (UTC) Received: by mail-vs1-xe37.google.com with SMTP id f203sf1751153vsd.17 for ; Thu, 20 Dec 2018 20:10:50 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1545365450; cv=pass; d=google.com; s=arc-20160816; b=IoWqCiOTAtNLRrs5Hv2N9mnW7u86n9ebZyW+WzLJXurIDF6/qAefGsBAdqtLEoCPAp SxV6oWedFue/7u5HA31FWfJ7lfQANNF4UA+yZodGvW2FggqOWrEn3VFLNSJZRAI/QvTS BaTvnKzGRmKZCyKtSvHX/tSnw8huL2JPjwWGyhX8IwcWZow72hYwgiaOK0nGW3ZSbgBc 02DsdJ7e/UmEBoBA7PKL9dKaH/5l/qPDFSEsg9K1OjWB/iegxcWlRqdcGKCxwqpiux4x 9MtCFxLObqC6iC8bFXTiMPtEMK7AFXkOrRqiHqgCgIk4ZijoODyRpFShWp3tWJGrlOhB zOsA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=bHaYaPmvWAljqizld682uWtrQGX/d+Wv+oGtqH/rT+U=; b=C7ActbSeXQOgWcxtVqbb3i9FO00UZvggLH/rJ6VL173yG61StOU83w+juYLnlYzkec yoyCpfAgLJzJ6ZVmq2faQ+EsQ9Ap+/x5kEscLuZAN2LBwXYdc6tdlxrYzAwiEJ0e/di8 mrYbeq+PvvtkA+MSZNye0xz4DtbUuUEmiVSm4X3jAcwl1Knhnk4yQEWDzEVDjTysG6ka m9UIDOumOuOmn1U+J1ib0lQTL3J66Hga5+yg6kNEeoeIsTJHGU2Q8EUbqKYZrkPIox0R O5g4BbyIADjJznLXieEXk3qYgt4aN2XxuJXCBAAuXovhnj1TjSPfZ1zCq9q5YnKwu3nf QavA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=t3ci5i4d; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::12d as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=bHaYaPmvWAljqizld682uWtrQGX/d+Wv+oGtqH/rT+U=; b=FHJdI8bs51RwAJkBcfnUMnwvo6yfVNIOSdXmL5IJRVt7/SW7nLcmcaVciKIInO+21w 1NMymXSnHwS/E7Mff990u+zBAgJ5Gd2G9/r6U9JN9cxbVi5qSyVe1Zpj7z4Oc4H63U5T X0FQenbq3VFgFn2pkd94UXYNS4eoWK0da6j5w0d94XMQnYgMARQ2h//6UVbUp7gDBSKd QvtHCB8EZB2bLItNxyeP/dbM78BDc8M9zlDrYZmPKGQAyv3pgIHoTHXKWb/K8T9XhGj4 CNRbA/EIRzIIdpoDKd5Ue5N+T57149X6CtYoQzWj0t6ix915p7JcahEOqzGG11u0UTNR DJ1Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=bHaYaPmvWAljqizld682uWtrQGX/d+Wv+oGtqH/rT+U=; b=K6Gq87hq71ZH5SDc6KFSQJdeEgKLP/V+RnISByC6i5n5uhkzOhHf89q5f1zMtQ5aUD XTPygglQCLie3FAWh4zAAbzOKYQbkHTOXXJgCh4xhP2FLVbmG3Lc4lcCE83REc1qklZK Wo2QNiJD2Uo0zmgrLGCSnd7FjhO4jxAn5gsU5GkqfLOM/KeSkmi4xF6I9N45HiVU9+Wf gxWTPo5xexR6QxSY3TDWnbLgTSx54aZOGF+NildO5T7Hoi9k155MyL3slb9KcyMIvB8D PqaurXnMw2SVPN/rE8hqiUc8jjdVP9mFpazRsuMSS4Sku58NPveaYjNR7ieImbs+pof3 6AZQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=bHaYaPmvWAljqizld682uWtrQGX/d+Wv+oGtqH/rT+U=; b=ZZlUBQwFJhDmRW4pNYyGU2cKhcEqDh+3Y/qHOJqWVBGGxg8f4Gy2Jn9i/cO4IJAR1t /dsGF6XJA65kPWDHqSEbO9hHtsx9QMMMvwJJUry0UJF81txqCPSAL3O/JywPumCwr6Aw UMuffvF/RDM6g4nGBcSY7Drcus3dT765uQTJy4MvjCYVK4AF6UMZJjJis7AyU1ytcGC4 ONO7uuVvLAsjfLbgInJnlJyvHUI3VMj9d8uVWbXjOF0/W8Z/PLW88Ohq7DF/kwgY6dUW a/NYkYDCTJv0GgY7IoS9gD4/YXX+DJrzuvJEDurtl2BU/D5cEZZwAk+vwMC2PZIiRTLu 7jlQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukds6w47GZQTvr+C1Rx5wkOD6eCE2DEbe+Fdv59fjkpbtSumOfIC OpSOMcSESzasGmLuBonTw+Y= X-Google-Smtp-Source: ALg8bN7+d+J6kCciFb15Gud49LI87i8M0sE3lTKBf3YZAxG+hQrgQ+AVEBKy7S+35d4dLoelSDZJKA== X-Received: by 2002:ab0:4e0c:: with SMTP id g12mr5169uah.2.1545365449922; Thu, 20 Dec 2018 20:10:49 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ab0:702a:: with SMTP id u10ls251200ual.3.gmail; Thu, 20 Dec 2018 20:10:49 -0800 (PST) X-Received: by 2002:ab0:3097:: with SMTP id h23mr642219ual.4.1545365449583; Thu, 20 Dec 2018 20:10:49 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1545365449; cv=none; d=google.com; s=arc-20160816; b=VmmrUw3nPwLgVCg+ulzKy8UTwscmWKIT67NNPZaS+Gsarxqemvu4T3eHXjm/OShHQv k4NxWOqqBHOiFoLkBdcBXVpcToehVYcmmL+0LsuyKEdnJ+13Zi6B1RcIzTS8sJL+HxRO tAi0EtIFkfQlrFlvUJQ5VdbMqFFrgC1aJgVPuFV0/5UfXMb9H2sSx181UWiEr8GP/8yg 6728Lhplqzh9/32lqOPWnAMDIvZzv1rjm6Ed8wgMd8jrLhhQCmERwXairBIx2FErwRWL hgX94Yq6b3JkfwNlybTfWyZNPJyZVll3YT/yz4U4l82UCuKjwrs39LhDRzbeXoJOF1SV a6pw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=xoE+MPE15+aLmDf7m1I3Q8DXx2kkll5xMUjjKoLy5u8=; b=tCHg9qgfdc2P8hJkHd/rWpQMVOeXjrwC/sMQI2Ju+jmhweh3MvEEvzXBgZBVtLJnNY MRxUywiGYJR/8rOn01UofRLDUZgnr3fZ3eslsEM+Lt3MTlO5Ts/9KXSL0DFX16akAUM3 DbCw5r8FZKR4Nr4n1jEwksAIyg1hZKslC26uGSpsF+JtOUdQjmn1Q4dRHQC5hDvpxbJ+ M6mGdpFp5Gs6MsEBVFv7eYpIBAjDmcK3gzNoEC5pvoxaxNlp39bxmLpCmWjK6hyPmnLC aRtqY0F2eebrLl/k/WeXSnR40ascx2uAtvtkrUbkNuP3trI0rVrbRDBGKdRM8BIeP87u 5e6w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=t3ci5i4d; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::12d as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it1-x12d.google.com (mail-it1-x12d.google.com. [2607:f8b0:4864:20::12d]) by gmr-mx.google.com with ESMTPS id l127si1132692vkh.3.2018.12.20.20.10.49 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 20 Dec 2018 20:10:49 -0800 (PST) Received-SPF: pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::12d as permitted sender) client-ip=2607:f8b0:4864:20::12d; Received: by mail-it1-x12d.google.com with SMTP id p197so4901438itp.0 for ; Thu, 20 Dec 2018 20:10:49 -0800 (PST) X-Received: by 2002:a24:55d4:: with SMTP id e203mr1037104itb.36.1545365449255; Thu, 20 Dec 2018 20:10:49 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: =?UTF-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= Date: Thu, 20 Dec 2018 23:10:37 -0500 Message-ID: Subject: Re: [HoTT] Quantum Computations and HoTT To: david.roberts@adelaide.edu.au Cc: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000a6b2ac057d806e95" X-Original-Sender: josephcmac@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=t3ci5i4d; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::12d as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --000000000000a6b2ac057d806e95 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thank you for this thesis: since February 2019 I will be working in a similar project. Kind Regards, Jos=C3=A9 M. El jue., 20 dic. 2018 a las 23:04, David Roberts () escribi=C3=B3: > Hi Jos=C3=A9 > > 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 computatio= n > 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=E2=80=99s abilities outwards, towards verifying popular qua= ntum > 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, thi= s > email is authorised by The University of Adelaide. > > .........................................................................= ................................................. > On Fri, 14 Dec 2018 at 14:36, Jos=C3=A9 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 c= an > use UniMath (Coq). Does the homotopy type theory has some advantage over > the simple type theory in this field? > > > > Kind Regards, > > Jos=C3=A9 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. > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --000000000000a6b2ac057d806e95 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thank you for this thesis: since February 2019 I will be w= orking in a similar project.

Kind Regards,
Jos= =C3=A9 M.

El jue= ., 20 dic. 2018 a las 23:04, David Roberts (<a1078662@adelaide.edu.au>) escribi=C3=B3:
=
Hi Jos=C3=A9

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 cor= rectness.
We justify this on the basis of the complexity of programs manipulating qua= ntum
states, the expense of running quantum programs, and the inapplicability of=
traditional debugging techniques to programs whose states cannot be examine= d. 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 prog= rams.

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=E2=80=99s abilities outwards, towards verifying popular quant= um
algorithms like quantum
teleportation. We argue that this tool provides a solid foundation for
research into
quantum programming languages and formal verification going forward."<= br>
Cheers,
David
...........................................................................= ...............................................
Dr David Michael Roberts
School of Mathematical Sciences, University of Adelaide, Australia=C2=A0 50= 05
Email: d= avid.roberts@adelaide.edu.au

CRICOS Provider Number 00123M
IMPORTANT: This message may contain confidential or legally privileged
information.=C2=A0 If you think it was sent to you by mistake,=C2=A0 please= delete all
copies and advise the sender.=C2=A0 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=C3=A9 Manuel Rodriguez Caballero
<josephcmac@gm= ail.com> wrote:
>
> Hello,
>=C2=A0 =C2=A0I am interested in the formal verification of theorems rel= ated to Quantum Computations. I have two possibilities in order to do my fo= rmalizations: either I can use simple type theory (Isabelle/HOL) or I can u= se UniMath (Coq). Does the homotopy type theory has some advantage over the= simple type theory in this field?
>
> Kind Regards,
> Jos=C3=A9 M.
>
> --
> You received this message because you are subscribed to the Google Gro= ups "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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
--000000000000a6b2ac057d806e95--