@mastersthesis{Singhal2020a,
  title         = {Quantum Hoare Type Theory},
  author        = {Singhal, Kartik},
  year          = {2020},
  month         = dec,
  school        = {University of Chicago},
  address       = {Chicago, IL},
  archiveprefix = {arXiv},
  eprint        = {2012.02154},
  url           = {https://ks.cs.uchicago.edu/publication/qhtt-masters/},
  abstract      = {As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. Inspired by Hoare Type Theory in classical computing, we propose Quantum Hoare Type Theory (QHTT), in which precise specifications about the modification to the quantum state can be provided within the type of computation. These specifications within a Hoare type are given in the form of Hoare-logic style pre- and postconditions following the propositions-as-types principle. The type-checking process verifies that the implementation conforms to the provided specification. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs.},
  keywords      = {formal verification, program proof, programming languages, quantum computing, quantum computation, type systems, type theory, pre- and postconditions, program specifications, hoare logic, separation logic},
  webnote       = {See also: \cite{Singhal2021a}},
  bibsource     = qplbib
}

{"_id":"HCStp9Zd2rkNfA69D","bibbaseid":"singhal-quantumhoaretypetheory-2020","author_short":["Singhal, K."],"bibdata":{"bibtype":"mastersthesis","type":"mastersthesis","title":"Quantum Hoare Type Theory","author":[{"propositions":[],"lastnames":["Singhal"],"firstnames":["Kartik"],"suffixes":[]}],"year":"2020","month":"December","school":"University of Chicago","address":"Chicago, IL","archiveprefix":"arXiv","eprint":"2012.02154","url":"https://ks.cs.uchicago.edu/publication/qhtt-masters/","abstract":"As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. Inspired by Hoare Type Theory in classical computing, we propose Quantum Hoare Type Theory (QHTT), in which precise specifications about the modification to the quantum state can be provided within the type of computation. These specifications within a Hoare type are given in the form of Hoare-logic style pre- and postconditions following the propositions-as-types principle. The type-checking process verifies that the implementation conforms to the provided specification. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs.","keywords":"formal verification, program proof, programming languages, quantum computing, quantum computation, type systems, type theory, pre- and postconditions, program specifications, hoare logic, separation logic","webnote":"See also: i̧teSinghal2021a","bibsource":"Quantum Programming Languages & Verification Bibliography, https://git.io/qpl-bib","bibtex":"@mastersthesis{Singhal2020a,\n title = {Quantum Hoare Type Theory},\n author = {Singhal, Kartik},\n year = {2020},\n month = dec,\n school = {University of Chicago},\n address = {Chicago, IL},\n archiveprefix = {arXiv},\n eprint = {2012.02154},\n url = {https://ks.cs.uchicago.edu/publication/qhtt-masters/},\n abstract = {As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. Inspired by Hoare Type Theory in classical computing, we propose Quantum Hoare Type Theory (QHTT), in which precise specifications about the modification to the quantum state can be provided within the type of computation. These specifications within a Hoare type are given in the form of Hoare-logic style pre- and postconditions following the propositions-as-types principle. The type-checking process verifies that the implementation conforms to the provided specification. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs.},\n keywords = {formal verification, program proof, programming languages, quantum computing, quantum computation, type systems, type theory, pre- and postconditions, program specifications, hoare logic, separation logic},\n webnote = {See also: \\cite{Singhal2021a}},\n bibsource = qplbib\n}\n\n","author_short":["Singhal, K."],"key":"Singhal2020a","id":"Singhal2020a","bibbaseid":"singhal-quantumhoaretypetheory-2020","role":"author","urls":{"Paper":"https://ks.cs.uchicago.edu/publication/qhtt-masters/"},"keyword":["formal verification","program proof","programming languages","quantum computing","quantum computation","type systems","type theory","pre- and postconditions","program specifications","hoare logic","separation logic"],"metadata":{"authorlinks":{}}},"bibtype":"mastersthesis","biburl":"https://raw.githubusercontent.com/QuantumPL/bib/main/bbt.bib","dataSources":["JG9W34HAXfSxsC6ML"],"keywords":["formal verification","program proof","programming languages","quantum computing","quantum computation","type systems","type theory","pre- and postconditions","program specifications","hoare logic","separation logic"],"search_terms":["quantum","hoare","type","theory","singhal"],"title":"Quantum Hoare Type Theory","year":2020}