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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x23e.google.com (mail-oi1-x23e.google.com [IPv6:2607:f8b0:4864:20::23e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e6411432 for ; Fri, 21 Dec 2018 04:10:08 +0000 (UTC) Received: by mail-oi1-x23e.google.com with SMTP id j13sf2710671oii.8 for ; Thu, 20 Dec 2018 20:10:08 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1545365406; cv=pass; d=google.com; s=arc-20160816; b=ewkRrPzDRBGgIngESBqWVoQFZY9ugu6KUhNQs1TilspZIZALxmSSIXTwMZzFGFa42z MOa88n7mXOJzkbJ3ICE3N0owSYTOzQUTJmKdNdr26p/Ghbp21yAKybuSvfge7vjAVpAX 0AUUTM31EHBNc3tgPnKNNCkimLen+x3cwgU0Ywkq5wrlm09WTD5CfOWllm5FZsFtGy07 zeyIHHd2+YPI4685JgMD1UrBonVM68c84pl/ZwQo6eDYYRVp10kqt44GLYqi6ErTgrMd JrYwfHiUtp85jSHgDvtdUxt6dCy+Q2/bdKzsM3AJenZmnSAMC2pZGLg33FbMrXHKOVYS F0Aw== 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:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature:dkim-signature; bh=9dBBzt9q2zl7Al57itQ49wPxtiPb/tDUG2pe0ymOWdM=; b=ehP2Nd2Rj5yP64sup+nUpVH9VKJ8T0fET+gBEz51wX6/eLvN341FL03oZEe9Rc0IzL SnUGC+v9WIMPVDs4pyUpwW2BfwFB+cm0E0Y7qPsg6sRuWfnDWA3SKVDqL0MMvY5VkBOr M+4GlembgTV7mPuxNBYagrE5qlXBib6sV7pIlLE2gQjORWWutGGZgVvA65SBBCsDsNmZ NXxOifqec2yuX/Phg7L87StjOrfG2QpjOXu1DtW/trmFPdITOU/zqLgbcsoVQJOciF5k anFgO0+M7tx5Rh1KjZL8bMezWbVlRkCQB3aDZnjP4NDoMHcBS+X2EQx9s8k3jFL7Qp4T Hlrw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=NuwvoRC2; spf=pass (google.com: domain of droberts.65537@gmail.com designates 2607:f8b0:4864:20::c2b as permitted sender) smtp.mailfrom=droberts.65537@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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=9dBBzt9q2zl7Al57itQ49wPxtiPb/tDUG2pe0ymOWdM=; b=J800VBhdAhvkGnB5OnZMpImAGFATDzA4Cvm+6DjVyuWx0JCHft7Y1a6PBf/52cwLxb 2Pm2kV/En28ZObZWT0sBkexOETVXqFeR2CHyRudnpI+rzf1r70cI+DPKNpDtJGWCWmxe 6xm90eIyRkCT5egp90hnWoUw7T41EFeZbGbOkQmm4Jwcq1A/pEcGafcWIlQjqjcetEHX sPC3Lok8XQacG17pgNxcgfEMQg+HGZLs6ghK/DX+LCIz61lYG6rRFY8U/wDGFM3umYFw aIkvDewbN+xTMXw4HgdHBGuswWlOcsONB7weA5aslSHyqdIwPBTDmd29sAAbh9RdpSHK h2Dw== 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=9dBBzt9q2zl7Al57itQ49wPxtiPb/tDUG2pe0ymOWdM=; b=MeKWiRDB3m/n2UzixrlQsnGMj9x3f6XbPtzKSSVfaeeJwe+xamZXQ5w42A2y2tyWnu YJdtSv5a8FYwHBogN/pb0g9wKWTzzUp/papdPDzcACvAk+Hwx8zRA73XDpQlr8YDVMd7 IBSSnHvmo8K0CBH5RJkhrMAKNxkeJmrvycs3dHE1gcgZgdlZ1Er6RH3Hqo2k2gJ2/6au VwdPDQgtzh4WuRGGBZLUFkNNnEt17e6Xi4eUxYWlh8muIz5hFaenonCa34QpPi3g6O1A KiOY+oQnvqWWW6mV17wG8yZTd4clVDFJKD5U8bzjYh1SYqxdjkzSCdK63BIddAYsWr0C APfg== 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:content-transfer-encoding :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=9dBBzt9q2zl7Al57itQ49wPxtiPb/tDUG2pe0ymOWdM=; b=jWYBsVezghpKFuz+kh3XdIpxT+0z8GLdBGBCSUnL7jLobObgNDCrruWOsaD6jJVBMf xfA9updb2fgw+hC5ZsSbSzxEus2uHq3I9MNRFbE4p2y14FLydcCYDIskT77373LA7Lr1 IQeUq8rBREuPBqyhKA0T81z58N7OhfG0keoOpMo6+l6Mu+wzlsQ5MCQSqULO4swGZKEr 3NZmXKfi3J9veFOIlXkqJhCPmeYG2dsAZU1hsIIc/kzJ2YH+wtxhv5u/9Wg6RSu41FSE ADyLki7QfdQydAfkKhV69Wty292xs7AGi8E6iNSwP/UB44Fe56s1GM8otQ9JmYyXStkt YuYA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukei1CPO2KnMzBOed+HHbaSsMYoRD9jRZV05yVhW/BxJdCkmc3uw 7HDfmqSLABzc+XU6gCphDPk= X-Google-Smtp-Source: ALg8bN729wRsQQpsIAiw91ODjUlV28aW7cre8ocOJXqAAfhCnafUccCJZwU9vCLt1OL+D7TI+HrgpQ== X-Received: by 2002:a9d:6f14:: with SMTP id n20mr12761otq.2.1545365406525; Thu, 20 Dec 2018 20:10:06 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:27e9:: with SMTP id c96ls580689otb.10.gmail; Thu, 20 Dec 2018 20:10:06 -0800 (PST) X-Received: by 2002:a9d:4701:: with SMTP id a1mr553371otf.28.1545365406227; Thu, 20 Dec 2018 20:10:06 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1545365406; cv=none; d=google.com; s=arc-20160816; b=dpmIUJU+Kt0/jdzBHCf5VoMnvA17QORbJxbhMEvEuSozHk0RPfyE4v2mD5O+ZZaT7y YhK2nEXvOSvP13ab/zxLoTgIEq3eN1fd5+YlQxGq1WEGVdNkqp9fFRXJEV4JTpAvXesc 54uKALYnwIhNLgBNwFQxxQgZqO7tYOyrkSpSE8t0Rc+9ZVy0FzTNc/cRBKDsQuhDvtqk oOF/0h7B+p9qZplCZML9/YkhNj2MZPZZWPp8+bKGvXdwjl23/UediwYYvv497BxwHa2m FfFwHqqbFj1miAYv3wLbBCs5uqmX6+r8mmu8q4BsFwmerRgL3/SA2dlYG/eJHvBy4j4g bMew== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=a97vKQ4XYtmGzzYWh8s3T2Dy+pIakIexynCxgpq1/XM=; b=cxvGiqirOZJHgtQDGpm5iIPI7y4CW5in8RU7R7UrG8pCZ0XWKU1cpSds68vGdi48ak FioNq8oAslaE0gSauVN0WecGXZBsNnBtt6w4nrWH/70SHMN0SHOdw5kiWhPhW188ZFWz RrkHkvFENoq+oV2ZYjpJ2sgimBPJU6YM7im+3CyDzjBroCbkrIoUXMk1mwVZ9LlYOmYT i1a4qBZMliWK8Hw3MlXsxzoWqyzLsKMIUNuydQQ1pTZ7VnDJ+dISJ2Sf8LiJ6iVsBD3c FGZUg7KkZsA5y9T1R7YgD+iinAPL6P6wkRoBtdPIJ83nBFe1eLFCDfm99kQblzrWLMv3 kMgg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=NuwvoRC2; spf=pass (google.com: domain of droberts.65537@gmail.com designates 2607:f8b0:4864:20::c2b as permitted sender) smtp.mailfrom=droberts.65537@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yw1-xc2b.google.com (mail-yw1-xc2b.google.com. [2607:f8b0:4864:20::c2b]) by gmr-mx.google.com with ESMTPS id n10si737704otf.2.2018.12.20.20.10.06 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 20 Dec 2018 20:10:06 -0800 (PST) Received-SPF: pass (google.com: domain of droberts.65537@gmail.com designates 2607:f8b0:4864:20::c2b as permitted sender) client-ip=2607:f8b0:4864:20::c2b; Received: by mail-yw1-xc2b.google.com with SMTP id b63so310391ywc.11 for ; Thu, 20 Dec 2018 20:10:06 -0800 (PST) X-Received: by 2002:a81:a155:: with SMTP id y82mr878523ywg.400.1545365405862; Thu, 20 Dec 2018 20:10:05 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: David Roberts Date: Fri, 21 Dec 2018 14:39:54 +1030 Message-ID: Subject: Re: [HoTT] Quantum Computations and HoTT To: josephcmac@gmail.com Cc: homotopytypetheory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: droberts.65537@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=NuwvoRC2; spf=pass (google.com: domain of droberts.65537@gmail.com designates 2607:f8b0:4864:20::c2b as permitted sender) smtp.mailfrom=droberts.65537@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: , [resending from correct email address for the list] 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 correctn= ess. 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." Cheers, David David Roberts http://ncatlab.org/nlab/show/David+Roberts 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 Quant= um 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 (C= oq). 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.