Update welcome and sync

closes #11

Author: k4rtik

content/home/welcome.md

@@ -21,7 +21,7 @@ Welcome to _Quantum Programming Languages & Verification Bibliography_.
 
 Our goal is to provide [canonical bibentries](/bib/about) in [BibTeX](https://raw.githubusercontent.com/QuantumPL/bib/main/bbt.bib) and [BibLaTeX](https://raw.githubusercontent.com/QuantumPL/bib/main/biblatex.bib) formats.
 
-Please [use this form](https://forms.gle/watgbhcDa5jkf85T7) if you find any mistakes or missing entries.
+Please see the [Contributing Guide](https://github.com/QuantumPL/bib/blob/main/CONTRIBUTING.md) or [use this form](https://forms.gle/watgbhcDa5jkf85T7) if you would like to add/correct any entries.
 
 {{% cta cta_link="./publication/" cta_text="See all publications →" %}}
 </center>

content/publication/Liu2019/cite.bib

@@ -12,7 +12,7 @@ @inproceedings{Liu2019
  pages = {187--207},
  doi = {10.1007/978-3-030-25543-5_12},
  abstract = {We formalize the theory of quantum Hoare logic (QHL) [TOPLAS 33(6),19], an extension of Hoare logic for reasoning about quantum programs. In particular, we formalize the syntax and semantics of quantum programs in Isabelle/HOL, write down the rules of quantum Hoare logic, and verify the soundness and completeness of the deduction system for partial correctness of quantum programs. As preliminary work, we formalize some necessary mathematical background in linear algebra, and define tensor products of vectors and matrices on quantum variables. As an application, we verify the correctness of Grover's search algorithm. To our best knowledge, this is the first time a Hoare logic for quantum programs is formalized in an interactive theorem prover, and used to verify the correctness of a nontrivial quantum algorithm.},
- keywords = {hoare logic},
+ keywords = {hoare logic, qhlprover},
  webnote = {See also: Isabelle AFP entry \cite{Liu2019a}},
  bibsource = {Quantum Programming Languages \& Verification Bibliography, https://git.io/qpl-bib}
 }

content/publication/Liu2019/index.md

@@ -15,6 +15,7 @@ authors:
 - Naijun Zhan
 tags:
 - hoare logic
+- qhlprover
 categories: []
 date: '2019-07-01'
 lastmod: 2021-08-16T11:44:18-05:00

content/publication/Liu2019a/cite.bib

@@ -7,7 +7,7 @@ @article{Liu2019a
  volume = {2019},
  url = {https://isa-afp.org/entries/QHLProver.html},
  abstract = {We formalize quantum Hoare logic [TOPLAS 33(6),19]. In particular, we specify the syntax and denotational semantics of a simple model of quantum programs. Then, we write down the rules of quantum Hoare logic for partial correctness, and show the soundness and completeness of the resulting proof system. As an application, we verify the correctness of Grover's algorithm.},
- keywords = {hoare logic},
+ keywords = {hoare logic, qhlprover},
  webnote = {Formal proof development in Isabelle, supplement to \cite{Liu2019}},
  bibsource = {Quantum Programming Languages \& Verification Bibliography, https://git.io/qpl-bib}
 }

static/retro/bbt_abstracts.html

@@ -1843,7 +1843,7 @@ <h1>Quantum PL & Verification Bibliography</h1>
 We formalize the theory of quantum Hoare logic (QHL) [TOPLAS 33(6),19], an extension of Hoare logic for reasoning about quantum programs. In particular, we formalize the syntax and semantics of quantum programs in Isabelle/HOL, write down the rules of quantum Hoare logic, and verify the soundness and completeness of the deduction system for partial correctness of quantum programs. As preliminary work, we formalize some necessary mathematical background in linear algebra, and define tensor products of vectors and matrices on quantum variables. As an application, we verify the correctness of Grover's search algorithm. To our best knowledge, this is the first time a Hoare logic for quantum programs is formalized in an interactive theorem prover, and used to verify the correctness of a nontrivial quantum algorithm.
 </blockquote>
 <blockquote>
-Keywords: hoare logic
+Keywords: hoare logic, qhlprover
 </blockquote>
 
 </td>
@@ -1865,7 +1865,7 @@ <h1>Quantum PL & Verification Bibliography</h1>
 We formalize quantum Hoare logic [TOPLAS 33(6),19]. In particular, we specify the syntax and denotational semantics of a simple model of quantum programs. Then, we write down the rules of quantum Hoare logic for partial correctness, and show the soundness and completeness of the resulting proof system. As an application, we verify the correctness of Grover's algorithm.
 </blockquote>
 <blockquote>
-Keywords: hoare logic
+Keywords: hoare logic, qhlprover
 </blockquote>
 
 </td>

static/retro/bbt_bib.html

@@ -1561,7 +1561,7 @@ <h1>bbt.bib</h1><a name="Abramsky2004"></a><pre>
   pages = {187--207},
   doi = {10.1007/978-3-030-25543-5_12},
   abstract = {We formalize the theory of quantum Hoare logic (QHL) [TOPLAS 33(6),19], an extension of Hoare logic for reasoning about quantum programs. In particular, we formalize the syntax and semantics of quantum programs in Isabelle/HOL, write down the rules of quantum Hoare logic, and verify the soundness and completeness of the deduction system for partial correctness of quantum programs. As preliminary work, we formalize some necessary mathematical background in linear algebra, and define tensor products of vectors and matrices on quantum variables. As an application, we verify the correctness of Grover's search algorithm. To our best knowledge, this is the first time a Hoare logic for quantum programs is formalized in an interactive theorem prover, and used to verify the correctness of a nontrivial quantum algorithm.},
-  keywords = {hoare logic},
+  keywords = {hoare logic, qhlprover},
   webnote = {See also: Isabelle AFP entry \cite{Liu2019a}},
   bibsource = {Quantum Programming Languages \& Verification Bibliography, https://git.io/qpl-bib}
 }
@@ -1577,7 +1577,7 @@ <h1>bbt.bib</h1><a name="Abramsky2004"></a><pre>
   volume = {2019},
   url = {<a href="https://isa-afp.org/entries/QHLProver.html">https://isa-afp.org/entries/QHLProver.html</a>},
   abstract = {We formalize quantum Hoare logic [TOPLAS 33(6),19]. In particular, we specify the syntax and denotational semantics of a simple model of quantum programs. Then, we write down the rules of quantum Hoare logic for partial correctness, and show the soundness and completeness of the resulting proof system. As an application, we verify the correctness of Grover's algorithm.},
-  keywords = {hoare logic},
+  keywords = {hoare logic, qhlprover},
   webnote = {Formal proof development in Isabelle, supplement to \cite{Liu2019}},
   bibsource = {Quantum Programming Languages \& Verification Bibliography, https://git.io/qpl-bib}
 }