Sync after adding Huot2019 and updating years for QPL'20

Author: k4rtik

.gitignore

@@ -5,3 +5,4 @@
 /resources/
 public/
 assets/jsconfig.json
+.hugo_build.lock

content/publication/Huot2019/cite.bib

@@ -0,0 +1,15 @@
+@inproceedings{Huot2019,
+ title = {Universal Properties in Quantum Theory},
+ author = {Huot, Mathieu and Staton, Sam},
+ year = {2019},
+ month = {January},
+ booktitle = {Proceedings of the 15th International Conference on Quantum Physics and Logic (QPL), Halifax, Canada, June 3--7, 2018},
+ editor = {Selinger, Peter and Chiribella, Giulio},
+ publisher = {{Open Publishing Association}},
+ series = {Electronic Proceedings in Theoretical Computer Science},
+ volume = {287},
+ pages = {213--223},
+ doi = {10.4204/EPTCS.287.12},
+ abstract = {We argue that notions in quantum theory should have universal properties in the sense of category theory. We consider the completely positive trace preserving (CPTP) maps, the basic notion of quantum channel. Physically, quantum channels are derived from pure quantum theory by allowing discarding. We phrase this in category theoretic terms by showing that the category of CPTP maps is the universal monoidal category with a terminal unit that has a functor from the category of isometries. In other words, the CPTP maps are the affine reflection of the isometries.}
+}
+

content/publication/Huot2019/index.md

@@ -0,0 +1,43 @@
+---
+# Documentation: https://wowchemy.com/docs/managing-content/
+
+title: Universal Properties in Quantum Theory
+subtitle: ''
+summary: ''
+authors:
+- Mathieu Huot
+- Sam Staton
+tags: []
+categories: []
+date: '2019-01-01'
+lastmod: 2021-12-13T08:25:15-06:00
+featured: false
+draft: false
+
+# Featured image
+# To use, add an image named `featured.jpg/png` to your page's folder.
+# Focal points: Smart, Center, TopLeft, Top, TopRight, Left, Right, BottomLeft, Bottom, BottomRight.
+image:
+  caption: ''
+  focal_point: ''
+  preview_only: false
+
+# Projects (optional).
+#   Associate this post with one or more of your projects.
+#   Simply enter your project's folder or file name without extension.
+#   E.g. `projects = ["internal-project"]` references `content/project/deep-learning/index.md`.
+#   Otherwise, set `projects = []`.
+projects: []
+publication_types:
+- '1'
+abstract: We argue that notions in quantum theory should have universal properties
+  in the sense of category theory. We consider the completely positive trace preserving
+  (CPTP) maps, the basic notion of quantum channel. Physically, quantum channels are
+  derived from pure quantum theory by allowing discarding. We phrase this in category
+  theoretic terms by showing that the category of CPTP maps is the universal monoidal
+  category with a terminal unit that has a functor from the category of isometries.
+  In other words, the CPTP maps are the affine reflection of the isometries.
+publication: '*Proceedings of the 15th International Conference on Quantum Physics
+  and Logic (QPL), Halifax, Canada, June 3--7, 2018*'
+doi: 10.4204/EPTCS.287.12
+---

content/publication/Rand2020/cite.bib renamed to content/publication/Rand2021/cite.bib

@@ -1,8 +1,8 @@
-@inproceedings{Rand2020,
+@inproceedings{Rand2021,
  title = {Gottesman Types for Quantum Programs},
  author = {Rand, Robert and Sundaram, Aarthi and Singhal, Kartik and Lackey, Brad},
- year = {2020},
- month = {June},
+ year = {2021},
+ month = {September},
  booktitle = {Proceedings of the 17th International Conference on Quantum Physics and Logic (QPL), Paris, France, June 2--6, 2020},
  editor = {Valiron, Beno{\^i}t and Mansfield, Shane and Arrighi, Pablo and Panangaden, Prakash},
  publisher = {{Open Publishing Association}},

content/publication/Rand2020/index.md renamed to content/publication/Rand2021/index.md

@@ -14,8 +14,8 @@ tags:
 - type systems
 - gottesman types
 categories: []
-date: '2020-06-01'
-lastmod: 2021-08-16T11:44:20-05:00
+date: '2021-09-01'
+lastmod: 2021-12-13T08:25:18-06:00
 featured: false
 draft: false
 
@@ -33,7 +33,6 @@ image:
 #   E.g. `projects = ["internal-project"]` references `content/project/deep-learning/index.md`.
 #   Otherwise, set `projects = []`.
 projects: []
-publishDate: '2021-08-16T16:44:20.671364Z'
 publication_types:
 - '1'
 abstract: The Heisenberg representation of quantum operators provides a powerful technique
@@ -46,8 +45,8 @@ abstract: The Heisenberg representation of quantum operators provides a powerful
   apply these types to reason about separable states and the superdense coding algorithm.
 publication: '*Proceedings of the 17th International Conference on Quantum Physics
   and Logic (QPL), Paris, France, June 2--6, 2020*'
+doi: 10.4204/EPTCS.340.14
 links:
 - name: URL
   url: https://rand.cs.uchicago.edu/publication/rand-2020-gottesman/
-doi: 10.4204/EPTCS.340.14
 ---

content/publication/Singhal2020a/cite.bib

@@ -1,18 +1,15 @@
-@inproceedings{Singhal2020a,
- title = {Quantum Hoare Type Theory: Extended Abstract},
- author = {Singhal, Kartik and Reppy, John},
+@mastersthesis{Singhal2020a,
+ title = {Quantum Hoare Type Theory},
+ author = {Singhal, Kartik},
  year = {2020},
- month = {June},
- booktitle = {Proceedings of the 17th International Conference on Quantum Physics and Logic (QPL), Paris, France, June 2--6, 2020},
- editor = {Valiron, Beno{\^i}t and Mansfield, Shane and Arrighi, Pablo and Panangaden, Prakash},
- publisher = {{Open Publishing Association}},
- series = {Electronic Proceedings in Theoretical Computer Science},
- volume = {340},
- pages = {291--302},
- doi = {10.4204/EPTCS.340.15},
- url = {https://ks.cs.uchicago.edu/publication/qhtt/},
- abstract = {As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. In classical computing, formal verification and sound static type systems prevent several classes of bugs from being introduced. There is a need for similar techniques in the quantum regime. Inspired by Hoare Type Theory in the classical paradigm, we propose Quantum Hoare Types by extending the Quantum IO Monad by indexing it with pre- and post-conditions that serve as program specifications. In this paper, we introduce Quantum Hoare Type Theory (QHTT), present its syntax and typing rules, and demonstrate its effectiveness with the help of examples. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs. This is a work in progress.},
- keywords = {formal verification, program proof, programming languages, quantum computing, type systems, type theory, pre- and postconditions, program specifications},
- note = {Also see expanded version: \cite{Singhal2020b}}
+ 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},
+ note = {See also: \cite{Singhal2021a}}
 }
 

content/publication/Singhal2020a/index.md

@@ -1,36 +1,57 @@
 ---
-title: 'Quantum Hoare Type Theory: Extended Abstract'
-date: '2020-06-01'
+# Documentation: https://wowchemy.com/docs/managing-content/
+
+title: Quantum Hoare Type Theory
+subtitle: ''
+summary: ''
 authors:
 - Kartik Singhal
-- John Reppy
-publication_types:
-- '1'
-abstract: As quantum computers become real, it is high time we come up with effective
-  techniques that help programmers write correct quantum programs. In classical computing,
-  formal verification and sound static type systems prevent several classes of bugs
-  from being introduced. There is a need for similar techniques in the quantum regime.
-  Inspired by Hoare Type Theory in the classical paradigm, we propose Quantum Hoare
-  Types by extending the Quantum IO Monad by indexing it with pre- and post-conditions
-  that serve as program specifications. In this paper, we introduce Quantum Hoare
-  Type Theory (QHTT), present its syntax and typing rules, and demonstrate its effectiveness
-  with the help of examples. QHTT has the potential to be a unified system for programming,
-  specifying, and reasoning about quantum programs. This is a work in progress.
-featured: false
-publication: '*Proceedings of the 17th International Conference on Quantum Physics
-  and Logic (QPL), Paris, France, June 2--6, 2020*'
 tags:
 - formal verification
 - program proof
 - programming languages
 - quantum computing
+- quantum computation
 - type systems
 - type theory
 - pre- and postconditions
 - program specifications
-doi: 10.4204/EPTCS.340.15
+categories: []
+date: '2020-12-01'
+lastmod: 2021-12-13T08:32:09-06:00
+featured: false
+draft: false
+
+# Featured image
+# To use, add an image named `featured.jpg/png` to your page's folder.
+# Focal points: Smart, Center, TopLeft, Top, TopRight, Left, Right, BottomLeft, Bottom, BottomRight.
+image:
+  caption: ''
+  focal_point: ''
+  preview_only: false
+
+# Projects (optional).
+#   Associate this post with one or more of your projects.
+#   Simply enter your project's folder or file name without extension.
+#   E.g. `projects = ["internal-project"]` references `content/project/deep-learning/index.md`.
+#   Otherwise, set `projects = []`.
+projects: []
+publication_types:
+- '7'
+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.
+publication: ''
 links:
+- name: arXiv
+  url: https://arxiv.org/abs/2012.02154
 - name: URL
-  url: https://ks.cs.uchicago.edu/publication/qhtt/
+  url: https://ks.cs.uchicago.edu/publication/qhtt-masters/
 ---
-Also see expanded version: [[Singhal2020b](../Singhal2020b)]
+See also: [[Singhal2021a](../Singhal2021a)]

content/publication/Singhal2020b/cite.bib

@@ -0,0 +1,18 @@
+@inproceedings{Singhal2021a,
+ title = {Quantum Hoare Type Theory: Extended Abstract},
+ author = {Singhal, Kartik and Reppy, John},
+ year = {2021},
+ month = {September},
+ booktitle = {Proceedings of the 17th International Conference on Quantum Physics and Logic (QPL), Paris, France, June 2--6, 2020},
+ editor = {Valiron, Beno{\^i}t and Mansfield, Shane and Arrighi, Pablo and Panangaden, Prakash},
+ publisher = {{Open Publishing Association}},
+ series = {Electronic Proceedings in Theoretical Computer Science},
+ volume = {340},
+ pages = {291--302},
+ doi = {10.4204/EPTCS.340.15},
+ url = {https://ks.cs.uchicago.edu/publication/qhtt/},
+ abstract = {As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. In classical computing, formal verification and sound static type systems prevent several classes of bugs from being introduced. There is a need for similar techniques in the quantum regime. Inspired by Hoare Type Theory in the classical paradigm, we propose Quantum Hoare Types by extending the Quantum IO Monad by indexing it with pre- and post-conditions that serve as program specifications. In this paper, we introduce Quantum Hoare Type Theory (QHTT), present its syntax and typing rules, and demonstrate its effectiveness with the help of examples. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs. This is a work in progress.},
+ keywords = {formal verification, program proof, programming languages, quantum computing, type systems, type theory, pre- and postconditions, program specifications},
+ note = {Also see expanded version: \cite{Singhal2020a}}
+}
+