coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Implementing Coq on quantum computer

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Implementing Coq on quantum computer
Date: Thu, 12 Dec 2019 18:34:16 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:dH24vxK6dZEE8KkaiNmcpTZWNBhigK39O0sv0rFitYgRLv3xwZ3uMQTl6Ol3ixeRBMOHsqkC0ruG+Pm5EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCezbL9oMRm7qQbcusYLjYd/N6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9gr9FrhKvpxJxwIDab4+aO/V8YqzTcsgXRXZDU8tLSyBNHo2xYosJAuEcPehYtY79p14WoBaiGAajHubvwSJWi3/22a060vwhHhvC3AM6AtkDt27bo8jvO6cXTe+417XHzS7ZYPNX3Tfx8o3IchE9of2WQ71/bNfRxFApGgjYjVuQsZToMy6L2ukOqWSW4fZsWfixh2I9tQ19vySjyt8xhoXXnI4Z1E7I+CRjzIsxOdG0UlN3bNC4HJZWqiqULZF5Qtk4TGFtoCs6yqMJuZq8fCUSz5Qn2gLfa/OAc4iJ5BLjW/+dISxkhH1/ZLKwnQy+/lS7yuLmV8m01ExGri9EktnQrHwCyQHc6tWfRvt8+EeuxyqP2hjO5u1aIk04j6TWJ4I7zrIujJYfr1nPEjPulEXzlqCWd0Ek+uay6+TgZ7XrvoWTOJJuhQH7LqsjgdCwAf8iPQgPW2iX4+G81Lz//UHjXrpFk+A2nrHDsJ/GPcQburK5AwhN34k/7Ba/Fi6q38gcnXkaN11IYwmHjojsO1HWOv/0F/a/g1K2kDdq3f/KJLPhAo+eZkTExbzmZPN271NW4As119FWoZxOWZ8bJ/emc0P4sZTzDhs4KwWwyq6zAdl004g2UnmGA6vfNaLO91KE+7R8cKG3eIYJtWOleLAe7Pn0gCphwAJPTeySxZISLUuAMLFmLkGeOiK+hcodHmALuAV7V/DjlFTEWiVaZnL0WqMgoDw3FdD+VNuRdsWWmLWEmRyDMNhOfGkfVwKHCn7pc8OBWutKZS6PcJc4w240EIO5Qopk7imA8Qrzyr5pNO3Ro3BKvonq1dwz4uzP0xw+6G4tAg==

I'm not aware of any known useful connection between these two subjects, so you will probably need to write more about the kind of connection that you expect (and the evidence that it probably exists), to get anyone associated with either topic to offer any useful perspectives.

On 12/12/19 5:21 PM, Alex Meyer wrote:

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?

[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