diff --git a/metadata/entries/FOL_Axiomatic.toml b/metadata/entries/FOL_Axiomatic.toml
--- a/metadata/entries/FOL_Axiomatic.toml
+++ b/metadata/entries/FOL_Axiomatic.toml
@@ -1,34 +1,35 @@
 title = "Soundness and Completeness of an Axiomatic System for First-Order Logic"
 date = 2021-09-24
 topics = [
   "Logic/General logic/Classical first-order logic",
   "Logic/Proof theory",
 ]
 abstract = """
 This work is a formalization of the soundness and completeness of an
 axiomatic system for first-order logic. The proof system is based on
 System Q1 by Smullyan and the completeness proof follows his textbook
 \"First-Order Logic\" (Springer-Verlag 1968). The completeness
 proof is in the Henkin style where a consistent set is extended to a
 maximal consistent set using Lindenbaum's construction and Henkin
 witnesses are added during the construction to ensure saturation as
 well. The resulting set is a Hintikka set which, by the model
-existence theorem, is satisfiable in the Herbrand universe."""
+existence theorem, is satisfiable in the Herbrand universe.
+Paper: <a href=\"https://doi.org/10.4230/LIPIcs.TYPES.2021.8\">doi.org/10.4230/LIPIcs.TYPES.2021.8</a>."""
 license = "bsd"
 note = ""
 
 [authors]
 
 [authors.from]
 homepage = "from_homepage"
 
 [contributors]
 
 [notify]
 from = "from_email"
 
 [history]
 
 [extra]
 
 [related]
diff --git a/metadata/entries/FOL_Seq_Calc2.toml b/metadata/entries/FOL_Seq_Calc2.toml
--- a/metadata/entries/FOL_Seq_Calc2.toml
+++ b/metadata/entries/FOL_Seq_Calc2.toml
@@ -1,42 +1,43 @@
 title = "A Sequent Calculus Prover for First-Order Logic with Functions"
 date = 2022-01-31
 topics = [
   "Logic/General logic/Classical first-order logic",
   "Logic/Proof theory",
   "Logic/General logic/Mechanization of proofs",
 ]
 abstract = """
 We formalize an automated theorem prover for first-order logic with
 functions. The proof search procedure is based on sequent calculus and
 we verify its soundness and completeness using the Abstract Soundness
 and Abstract Completeness theories. Our analytic completeness proof
 covers both open and closed formulas. Since our deterministic prover
 considers only the subset of terms relevant to proving a given
 sequent, we do so as well when building a countermodel from a failed
 proof. We formally connect our prover with the proof system and
 semantics of the existing SeCaV system. In particular, the
 prover's output can be post-processed in Haskell to generate
 human-readable SeCaV proofs which are also machine-verifiable proof
-certificates."""
+certificates.
+Paper: <a href=\"https://doi.org/10.4230/LIPIcs.ITP.2022.13\">doi.org/10.4230/LIPIcs.ITP.2022.13</a>."""
 license = "bsd"
 note = ""
 
 [authors]
 
 [authors.from]
 homepage = "from_homepage"
 
 [authors.jacobsen]
 homepage = "jacobsen_homepage"
 
 [contributors]
 
 [notify]
 from = "from_email"
 jacobsen = "jacobsen_email"
 
 [history]
 
 [extra]
 
 [related]
diff --git a/metadata/entries/Hybrid_Logic.toml b/metadata/entries/Hybrid_Logic.toml
--- a/metadata/entries/Hybrid_Logic.toml
+++ b/metadata/entries/Hybrid_Logic.toml
@@ -1,42 +1,43 @@
 title = "Formalizing a Seligman-Style Tableau System for Hybrid Logic"
 date = 2019-12-20
 topics = [
   "Logic/General logic/Modal logic",
 ]
 abstract = """
 This work is a formalization of soundness and completeness proofs
 for a Seligman-style tableau system for hybrid logic. The completeness
 result is obtained via a synthetic approach using maximally
 consistent sets of tableau blocks. The formalization differs from
 previous work in a few ways. First, to avoid the need to backtrack in
 the construction of a tableau, the formalized system has no unnamed
 initial segment, and therefore no Name rule. Second, I show that the
 full Bridge rule is admissible in the system. Third, I start from rules
 restricted to only extend the branch with new formulas, including only
 witnessing diamonds that are not already witnessed, and show that
 the unrestricted rules are admissible. Similarly, I start from simpler
 versions of the @-rules and show that these are sufficient.
 The GoTo rule is restricted using a notion of potential such that each
 application consumes potential and potential is earned through applications of
 the remaining rules. I show that if a branch can be closed then it can
 be closed starting from a single unit. Finally, Nom is restricted by
-a fixed set of allowed nominals. The resulting system should be terminating."""
+a fixed set of allowed nominals. The resulting system should be terminating.
+Paper: <a href=\"https://doi.org/10.4230/LIPIcs.TYPES.2020.5\">doi.org/10.4230/LIPIcs.TYPES.2020.5</a>."""
 license = "bsd"
 note = ""
 
 [authors]
 
 [authors.from]
 homepage = "from_homepage"
 
 [contributors]
 
 [notify]
 from = "from_email"
 
 [history]
 2020-06-03 = "The fully restricted system has been shown complete by updating the synthetic completeness proof."
 
 [extra]
 
 [related]