{"data":{"id":"10.48550/arxiv.1901.05184","type":"dois","attributes":{"doi":"10.48550/arxiv.1901.05184","prefix":"10.48550","suffix":"arxiv.1901.05184","identifiers":[{"identifier":"1901.05184","identifierType":"arXiv"}],"alternateIdentifiers":[{"alternateIdentifierType":"arXiv","alternateIdentifier":"1901.05184"}],"creators":[{"name":"Barthe, Gilles","nameType":"Personal","givenName":"Gilles","familyName":"Barthe","affiliation":[],"nameIdentifiers":[]},{"name":"Hsu, Justin","nameType":"Personal","givenName":"Justin","familyName":"Hsu","affiliation":[],"nameIdentifiers":[]},{"name":"Ying, Mingsheng","nameType":"Personal","givenName":"Mingsheng","familyName":"Ying","affiliation":[],"nameIdentifiers":[]},{"name":"Yu, Nengkun","nameType":"Personal","givenName":"Nengkun","familyName":"Yu","affiliation":[],"nameIdentifiers":[]},{"name":"Zhou, Li","nameType":"Personal","givenName":"Li","familyName":"Zhou","affiliation":[],"nameIdentifiers":[]}],"titles":[{"title":"Relational Proofs for Quantum Programs"}],"publisher":"arXiv","container":{},"publicationYear":2019,"subjects":[{"lang":"en","subject":"Logic in Computer Science (cs.LO)","subjectScheme":"arXiv"},{"lang":"en","subject":"Quantum Physics (quant-ph)","subjectScheme":"arXiv"},{"subject":"FOS: Computer and information sciences","subjectScheme":"Fields of Science and Technology (FOS)"},{"subject":"FOS: Computer and information sciences","schemeUri":"http://www.oecd.org/science/inno/38235147.pdf","subjectScheme":"Fields of Science and Technology (FOS)"},{"subject":"FOS: Physical sciences","subjectScheme":"Fields of Science and Technology (FOS)"},{"subject":"FOS: Physical sciences","schemeUri":"http://www.oecd.org/science/inno/38235147.pdf","subjectScheme":"Fields of Science and Technology (FOS)"}],"contributors":[],"dates":[{"date":"2019-01-16T09:00:28Z","dateType":"Submitted","dateInformation":"v1"},{"date":"2019-01-18T01:09:50Z","dateType":"Updated","dateInformation":"v1"},{"date":"2019-12-11T17:47:21Z","dateType":"Submitted","dateInformation":"v2"},{"date":"2019-12-12T01:18:14Z","dateType":"Updated","dateInformation":"v2"},{"date":"2019-01","dateType":"Available","dateInformation":"v1"},{"date":"2019","dateType":"Issued"}],"language":null,"types":{"ris":"RPRT","bibtex":"article","citeproc":"article-journal","schemaOrg":"ScholarlyArticle","resourceType":"Article","resourceTypeGeneral":"Text"},"relatedIdentifiers":[{"relationType":"IsVersionOf","relatedIdentifier":"10.1145/3371089","relatedIdentifierType":"DOI"}],"relatedItems":[],"sizes":[],"formats":[],"version":"2","rightsList":[{"rights":"arXiv.org perpetual, non-exclusive license","rightsUri":"http://arxiv.org/licenses/nonexclusive-distrib/1.0/"}],"descriptions":[{"description":"Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantum programs. The interpretation of our logic is based on a quantum analogue of probabilistic couplings. We use our logic to verify non-trivial relational properties of quantum programs, including uniformity for samples generated by the quantum Bernoulli factory, reliability of quantum teleportation against noise (bit and phase flip), security of quantum one-time pad and equivalence of quantum walks.","descriptionType":"Abstract"},{"description":"34 pages, LaTeX; v2: extend version of conference paper","descriptionType":"Other"}],"geoLocations":[],"fundingReferences":[],"xml":"PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0idXRmLTgiPz4KPHJlc291cmNlIHhtbG5zPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCIgeG1sbnM6eHNpPSJodHRwOi8vd3d3LnczLm9yZy8yMDAxL1hNTFNjaGVtYS1pbnN0YW5jZSIgeHNpOnNjaGVtYUxvY2F0aW9uPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCBodHRwOi8vc2NoZW1hLmRhdGFjaXRlLm9yZy9tZXRhL2tlcm5lbC00LjMvbWV0YWRhdGEueHNkIj4KICA8aWRlbnRpZmllciBpZGVudGlmaWVyVHlwZT0iRE9JIj4xMC40ODU1MC9BUlhJVi4xOTAxLjA1MTg0PC9pZGVudGlmaWVyPgogIDxhbHRlcm5hdGVJZGVudGlmaWVycz4KICAgIDxhbHRlcm5hdGVJZGVudGlmaWVyIGFsdGVybmF0ZUlkZW50aWZpZXJUeXBlPSJhclhpdiI+MTkwMS4wNTE4NDwvYWx0ZXJuYXRlSWRlbnRpZmllcj4KICA8L2FsdGVybmF0ZUlkZW50aWZpZXJzPgogIDxjcmVhdG9ycz4KICAgIDxjcmVhdG9yPgogICAgICA8Y3JlYXRvck5hbWUgbmFtZVR5cGU9IlBlcnNvbmFsIj5CYXJ0aGUsIEdpbGxlczwvY3JlYXRvck5hbWU+CiAgICAgIDxnaXZlbk5hbWU+R2lsbGVzPC9naXZlbk5hbWU+CiAgICAgIDxmYW1pbHlOYW1lPkJhcnRoZTwvZmFtaWx5TmFtZT4KICAgIDwvY3JlYXRvcj4KICAgIDxjcmVhdG9yPgogICAgICA8Y3JlYXRvck5hbWUgbmFtZVR5cGU9IlBlcnNvbmFsIj5Ic3UsIEp1c3RpbjwvY3JlYXRvck5hbWU+CiAgICAgIDxnaXZlbk5hbWU+SnVzdGluPC9naXZlbk5hbWU+CiAgICAgIDxmYW1pbHlOYW1lPkhzdTwvZmFtaWx5TmFtZT4KICAgIDwvY3JlYXRvcj4KICAgIDxjcmVhdG9yPgogICAgICA8Y3JlYXRvck5hbWUgbmFtZVR5cGU9IlBlcnNvbmFsIj5ZaW5nLCBNaW5nc2hlbmc8L2NyZWF0b3JOYW1lPgogICAgICA8Z2l2ZW5OYW1lPk1pbmdzaGVuZzwvZ2l2ZW5OYW1lPgogICAgICA8ZmFtaWx5TmFtZT5ZaW5nPC9mYW1pbHlOYW1lPgogICAgPC9jcmVhdG9yPgogICAgPGNyZWF0b3I+CiAgICAgIDxjcmVhdG9yTmFtZSBuYW1lVHlwZT0iUGVyc29uYWwiPll1LCBOZW5na3VuPC9jcmVhdG9yTmFtZT4KICAgICAgPGdpdmVuTmFtZT5OZW5na3VuPC9naXZlbk5hbWU+CiAgICAgIDxmYW1pbHlOYW1lPll1PC9mYW1pbHlOYW1lPgogICAgPC9jcmVhdG9yPgogICAgPGNyZWF0b3I+CiAgICAgIDxjcmVhdG9yTmFtZSBuYW1lVHlwZT0iUGVyc29uYWwiPlpob3UsIExpPC9jcmVhdG9yTmFtZT4KICAgICAgPGdpdmVuTmFtZT5MaTwvZ2l2ZW5OYW1lPgogICAgICA8ZmFtaWx5TmFtZT5aaG91PC9mYW1pbHlOYW1lPgogICAgPC9jcmVhdG9yPgogIDwvY3JlYXRvcnM+CiAgPHRpdGxlcz4KICAgIDx0aXRsZT5SZWxhdGlvbmFsIFByb29mcyBmb3IgUXVhbnR1bSBQcm9ncmFtczwvdGl0bGU+CiAgPC90aXRsZXM+CiAgPHB1Ymxpc2hlcj5hclhpdjwvcHVibGlzaGVyPgogIDxwdWJsaWNhdGlvblllYXI+MjAxOTwvcHVibGljYXRpb25ZZWFyPgogIDxzdWJqZWN0cz4KICAgIDxzdWJqZWN0IHhtbDpsYW5nPSJlbiIgc3ViamVjdFNjaGVtZT0iYXJYaXYiPkxvZ2ljIGluIENvbXB1dGVyIFNjaWVuY2UgKGNzLkxPKTwvc3ViamVjdD4KICAgIDxzdWJqZWN0IHhtbDpsYW5nPSJlbiIgc3ViamVjdFNjaGVtZT0iYXJYaXYiPlF1YW50dW0gUGh5c2ljcyAocXVhbnQtcGgpPC9zdWJqZWN0PgogICAgPHN1YmplY3Qgc3ViamVjdFNjaGVtZT0iRmllbGRzIG9mIFNjaWVuY2UgYW5kIFRlY2hub2xvZ3kgKEZPUykiPkZPUzogQ29tcHV0ZXIgYW5kIGluZm9ybWF0aW9uIHNjaWVuY2VzPC9zdWJqZWN0PgogICAgPHN1YmplY3Qgc3ViamVjdFNjaGVtZT0iRmllbGRzIG9mIFNjaWVuY2UgYW5kIFRlY2hub2xvZ3kgKEZPUykiPkZPUzogUGh5c2ljYWwgc2NpZW5jZXM8L3N1YmplY3Q+CiAgPC9zdWJqZWN0cz4KICA8ZGF0ZXM+CiAgICA8ZGF0ZSBkYXRlVHlwZT0iU3VibWl0dGVkIiBkYXRlSW5mb3JtYXRpb249InYxIj4yMDE5LTAxLTE2VDA5OjAwOjI4WjwvZGF0ZT4KICAgIDxkYXRlIGRhdGVUeXBlPSJVcGRhdGVkIiBkYXRlSW5mb3JtYXRpb249InYxIj4yMDE5LTAxLTE4VDAxOjA5OjUwWjwvZGF0ZT4KICAgIDxkYXRlIGRhdGVUeXBlPSJTdWJtaXR0ZWQiIGRhdGVJbmZvcm1hdGlvbj0idjIiPjIwMTktMTItMTFUMTc6NDc6MjFaPC9kYXRlPgogICAgPGRhdGUgZGF0ZVR5cGU9IlVwZGF0ZWQiIGRhdGVJbmZvcm1hdGlvbj0idjIiPjIwMTktMTItMTJUMDE6MTg6MTRaPC9kYXRlPgogICAgPGRhdGUgZGF0ZVR5cGU9IkF2YWlsYWJsZSIgZGF0ZUluZm9ybWF0aW9uPSJ2MSI+MjAxOS0wMTwvZGF0ZT4KICA8L2RhdGVzPgogIDxyZXNvdXJjZVR5cGUgcmVzb3VyY2VUeXBlR2VuZXJhbD0iVGV4dCI+QXJ0aWNsZTwvcmVzb3VyY2VUeXBlPgogIDxyZWxhdGVkSWRlbnRpZmllcnM+CiAgICA8cmVsYXRlZElkZW50aWZpZXIgcmVsYXRlZElkZW50aWZpZXJUeXBlPSJET0kiIHJlbGF0aW9uVHlwZT0iSXNWZXJzaW9uT2YiPjEwLjExNDUvMzM3MTA4OTwvcmVsYXRlZElkZW50aWZpZXI+CiAgPC9yZWxhdGVkSWRlbnRpZmllcnM+CiAgPHZlcnNpb24+MjwvdmVyc2lvbj4KICA8cmlnaHRzTGlzdD4KICAgIDxyaWdodHMgcmlnaHRzVVJJPSJodHRwOi8vYXJ4aXYub3JnL2xpY2Vuc2VzL25vbmV4Y2x1c2l2ZS1kaXN0cmliLzEuMC8iPmFyWGl2Lm9yZyBwZXJwZXR1YWwsIG5vbi1leGNsdXNpdmUgbGljZW5zZTwvcmlnaHRzPgogIDwvcmlnaHRzTGlzdD4KICA8ZGVzY3JpcHRpb25zPgogICAgPGRlc2NyaXB0aW9uIGRlc2NyaXB0aW9uVHlwZT0iQWJzdHJhY3QiPlJlbGF0aW9uYWwgdmVyaWZpY2F0aW9uIG9mIHF1YW50dW0gcHJvZ3JhbXMgaGFzIG1hbnkgcG90ZW50aWFsIGFwcGxpY2F0aW9ucyBpbiBxdWFudHVtIGFuZCBwb3N0LXF1YW50dW0gc2VjdXJpdHkgYW5kIG90aGVyIGRvbWFpbnMuIFdlIHByb3Bvc2UgYSByZWxhdGlvbmFsIHByb2dyYW0gbG9naWMgZm9yIHF1YW50dW0gcHJvZ3JhbXMuIFRoZSBpbnRlcnByZXRhdGlvbiBvZiBvdXIgbG9naWMgaXMgYmFzZWQgb24gYSBxdWFudHVtIGFuYWxvZ3VlIG9mIHByb2JhYmlsaXN0aWMgY291cGxpbmdzLiBXZSB1c2Ugb3VyIGxvZ2ljIHRvIHZlcmlmeSBub24tdHJpdmlhbCByZWxhdGlvbmFsIHByb3BlcnRpZXMgb2YgcXVhbnR1bSBwcm9ncmFtcywgaW5jbHVkaW5nIHVuaWZvcm1pdHkgZm9yIHNhbXBsZXMgZ2VuZXJhdGVkIGJ5IHRoZSBxdWFudHVtIEJlcm5vdWxsaSBmYWN0b3J5LCByZWxpYWJpbGl0eSBvZiBxdWFudHVtIHRlbGVwb3J0YXRpb24gYWdhaW5zdCBub2lzZSAoYml0IGFuZCBwaGFzZSBmbGlwKSwgc2VjdXJpdHkgb2YgcXVhbnR1bSBvbmUtdGltZSBwYWQgYW5kIGVxdWl2YWxlbmNlIG9mIHF1YW50dW0gd2Fsa3MuPC9kZXNjcmlwdGlvbj4KICAgIDxkZXNjcmlwdGlvbiBkZXNjcmlwdGlvblR5cGU9Ik90aGVyIj4zNCBwYWdlcywgTGFUZVg7IHYyOiBleHRlbmQgdmVyc2lvbiBvZiBjb25mZXJlbmNlIHBhcGVyPC9kZXNjcmlwdGlvbj4KICA8L2Rlc2NyaXB0aW9ucz4KPC9yZXNvdXJjZT4=","url":"https://arxiv.org/abs/1901.05184","contentUrl":null,"metadataVersion":0,"schemaVersion":"http://datacite.org/schema/kernel-4","source":"mds","isActive":true,"state":"findable","reason":null,"viewCount":0,"viewsOverTime":[],"downloadCount":0,"downloadsOverTime":[],"referenceCount":0,"citationCount":0,"citationsOverTime":[],"partCount":0,"partOfCount":0,"versionCount":0,"versionOfCount":0,"created":"2022-03-01T14:45:04.000Z","registered":"2022-03-01T14:45:05.000Z","published":"2019","updated":"2022-03-01T14:45:05.000Z"},"relationships":{"client":{"data":{"id":"arxiv.content","type":"clients"}},"provider":{"data":{"id":"arxiv","type":"providers"}},"media":{"data":{"id":"10.48550/arxiv.1901.05184","type":"media"}},"references":{"data":[]},"citations":{"data":[]},"parts":{"data":[]},"partOf":{"data":[]},"versions":{"data":[]},"versionOf":{"data":[]}}}}