coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Why Qwire was verified precisely in Coq?

From: José Manuel Rodriguez Caballero <josephcmac AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Why Qwire was verified precisely in Coq?
Date: Thu, 20 Dec 2018 23:53:55 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=josephcmac AT gmail.com; spf=Pass smtp.mailfrom=josephcmac AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f46.google.com
Ironport-phdr: 9a23:BO+jMhFkb1AbJysJe3bPSp1GYnF86YWxBRYc798ds5kLTJ78r86wAkXT6L1XgUPTWs2DsrQY07qQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDmwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAe4GPeZDtY7yv1wAogG4BQmxGuzvzidHiGPx3aInyeQhEA7G3BE+ENMPqHvZss/6O7wIXuCxyKnH0y/Db/RL0jr66ojIdQshru+UXbJwbcXRzFMgGB/eg1WfrIzqJTKV1uAXv2eH6OpgUPuihmg6oA9/pTivw90jiojPho8N11DE8Dh2zJwrKtKlVU52Z8OvHphItyyCKYd6XscvT3trtSs60LEKpJ+2cSkQxJkoxhPSbeGMfZKS7RL5TumRJC91hHJ7d7K7gBa/6U2gxff9VsmwyVpKry1FnsTVunAD2BHe69KLSvR6/kem1jaP0x7c5vtYLkAzkKrXM58hwrgumZoPqUnPADP6lUHsgKKVdkgo4PWk5uXmb7n8qZKRNpd4igTkPaQvnsy/D/44Mg8LX2WD++S806bj8lPhQLVKkvI2l7PWv4zBKMQUo662GQ5V0oI55xmjCDem1cwUnWMbI1JdZBKHk4/pNknSL/D/FPezmkijkDN2x//dJbDhGZXMLn3bkLj7Z7p96khcyBAyzd9F/Z5UBKsBc7rPXRr6s8WdBRskOSS1xfzmAZNzzNAwQ2WKV42eKyLllFaO++8rFNOLaJUUtyvwOc8O7vTniXs0g1hVKauuxpYPaHu9F/9OLECQYH6qidAERzRZ9jEiRfDn3QXRGQVYYGy/Cvplt2MLTbm+BIKGfbiDxbmI3SO1BJpTPzkUBVWFEHOufIKBCa5VNHCiZ/R5mzlBboCPDpc73Ej35gD/wrtjaOHT/39A7M+x5J1O/+TW0CoK23l0AsCaiTzfSmh1miYJQGZz0vwh50N6zViH3O5zhPkKTdE=

Hello,

In Robert Rand's PhD thesis

http://www.cs.umd.edu/~rrand/thesis.pdf

quantum programs were verified using a tool known as Qwire. The semantics of Qwire was verified in Coq. Other authors have previously used Isabelle/HOL in order to verify semantical structures related to Quantum Computing. My question is rather type-theoretical:

Does Calculus of Inductive Constructions have some advantages over Simple Type Theory in order to formally verify quantum programs?

In other words:

Was the verification of Qwire in Coq an arbitrary choice among all the proof assistants available right now or are there deep theoretical reasons for this precise choice?

Kind Regards,

José M.

Re: [Coq-Club] Example of terminating function that are not accepted by Coq, (continued)
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Jean-Francois Monin, 12/19/2018
  - [Coq-Club] Why Qwire was verified precisely in Coq?, José Manuel Rodriguez Caballero, 12/21/2018
    - Re: [Coq-Club] Why Qwire was verified precisely in Coq?, Robert Rand, 12/21/2018
      - Re: [Coq-Club] Why Qwire was verified precisely in Coq?, José Manuel Rodriguez Caballero, 12/21/2018