coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Alex Meyer <alex153 AT outlook.lv>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Implementing Coq on quantum computer
- Date: Thu, 12 Dec 2019 22:21:33 +0000
- Accept-language: lv-LV, en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=none; dmarc=none; dkim=none; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=GvduMVHIgWlY12zYp5PptKqfSYuYLW6lkQ9WxP4NDEE=; b=TeK8+5B0ViNLyKHcjTTmQHGcXB8KcmseM4ehCv/BZpzQASVWT4rHZ/NYd3yelTHV/nNxkQC0FFYxB2AyFPMbm5vmpreAbrgChJdEok85hOotuXQncXbaBuVULIHa5g/QaIphusq+lTZG4ngNOrMg2S/qx297v71fiehz2E17EPihjOo8RhIOXiDKJNGEiVa8pD51dgm4jmeLNiiPE6bn4wtIq3dV3uDDYXCG+SRQV8yY1AudlHTOZUn7BjjsKjQa5SnDuFQ7UaJFSGDF0gCeD5ey2tejgJSpy7zX0117bA2WfmGVCw1KQmRX3j4JVG1YP3Kaya0RicJ/S4OOCZxHnA==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=JknWDd8UR7pHFS/W8Un4DF70T9MYhR7Oiyx9lU4tZOOVqWy8JjCkBcdHQVMWwU8oNyVQ7rc0knQeEIW/oGZc8CeURywuBZE5KfYH5tX2y0PGD0DCgKJw8zfmA59/npmGu9VW9C+kmRnZwzpVShSGkqpu1eCjZMAxskL059i5xAOIClKE5NJFeHl1p4CcECdQfEdBxDRCGEhQ8iZvQtjLVfa3Lvofeslbh9LayK8JKm+IZ3lS/NvSzjRPDwUC7qlPXsCWpbQqHNz0BXpSv4Dgpx7xQxQGDJXQIpnpJSmv09BuL+9cKtfg1HrjkMcNFPglq72ANyWJc8A7rqiOIREBRA==
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=alex153 AT outlook.lv; spf=Pass smtp.mailfrom=alex153 AT outlook.lv; spf=Pass smtp.helo=postmaster AT EUR01-VE1-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:Eda07x2cXfqYQ6dYsmDT+DRfVm0co7zxezQtwd8ZseIWKvad9pjvdHbS+e9qxAeQG9mCsLQd2rWd6v2+EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCezbL9oMRm7qQfcusYLjYZiK6s61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9Zwgbpbrhy/uhJ/34DaboKJO/VxZa7SZ88WSXZbU8pNSyBNHIWxZJYPAeobOuZYqpHwqkcKrRSgCginGeThxSFIh3Dox60xzuMsHhvC3AM+ENMCrXTZodvuOacVTOC10K3IzTLEb/NVwzv97JbIfwknrPqRXrxwadLcxEYzGw/filict5bpMjKU2+gXt2WW7fJsVeyxhGMktw18pz2iy8Qjh4THmI0Yz0vL+jh5zYooINC3VU12bNyqEJZVtyyaOZB5Qs0kTmp1oig10KcGtoS+fCUSyJQo2Rrfa/uffoaH7B3tSPqdLSphiH1qd7yzmg++8U+7xeLiTMW010tKrjZendnLq3AN0QHc5tKfSvtn+UehxSiA2BzP6uFFJkA0k7DXK5k8wr4skpoTtkPDHizslErqi6+Wc10o+umu6+v5frXrvpCRO5Nuhgz6LKgigM2yDOUiPgUKXWWX4eG826fi/U39TrVKlPo2kqzBvZ/AIcQUuKG4DxJV34st8Bu/CCqm0MgcnXkAK1JFewiLj4z3O13WOvD3Ee+/g0iwkDds3/3JIrrhAozUInfflLfhYK1y5lVHyAszyNBf/4hbBqsAIPL1QE/xtcbXAgU3MwyukK7bD4A33YQHHGmLH6WxMaXIsFbO6Phla72HY5ZQszLgIdAk4eTvhDk3gwlOU7Ou2M4+bH2oVtFrMkiDKS7lhtoRSDpRlg0jUOjtj17EVSAFNCX6ZL41+jxuUNHuNozEXI342OXQjhf+JYVfYyV9Mn7JFH7pc4ueXPJVMnCVP9NllTsHE7y/GdZ4iUOe8TTiwr8iFdL6vzUCvMu5ht9o++nUkhJ08SImV53AgVHIdHl9myYzfxFz3K17phAimHq+6/AhxsJ1TJlU7f4PVRomP5nByeA8E8r1Rg/KYtaOThChX8miBjYyCNk2xo1Xbg==
Are there some thoughts, efforts and ideas about implementing Coq (or part of it) on quantum computer? I am novice in quantum computing, but I can not find any guidance about quantum algorithms that are designed especially for the type theory of any kind or
first-order/higher-order logic. Does quantum community call those algorithms somehow differently or have different perspective? Or maybe quantum speedup is not available for the type of reasoning that is done by Coq?
Alex
- [Coq-Club] Implementing Coq on quantum computer, Alex Meyer, 12/12/2019
- Re: [Coq-Club] Implementing Coq on quantum computer, Adam Chlipala, 12/13/2019
Archive powered by MHonArc 2.6.18.