diff --git a/content/blog/00_spa_agda_intro.md b/content/blog/00_spa_agda_intro.md
index e8e38a0..2539ecd 100644
--- a/content/blog/00_spa_agda_intro.md
+++ b/content/blog/00_spa_agda_intro.md
@@ -4,6 +4,7 @@ series: "Static Program Analysis in Agda"
 description: "In this post, I give a top-level overview of my work on formally verified static analyses"
 date: 2024-04-12T14:23:03-07:00
 draft: true
+tags: ["Agda", "Programming Languages"]
 ---
 
 Some years ago, when the Programming Languages research group at Oregon State
diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md
index 580a0fe..c747e48 100644
--- a/content/blog/01_spa_agda_lattices.md
+++ b/content/blog/01_spa_agda_lattices.md
@@ -3,6 +3,7 @@ title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 1:
 series: "Static Program Analysis in Agda"
 date: 2024-04-13T14:23:03-07:00
 draft: true
+tags: ["Agda", "Programming Languages"]
 ---
 
 This is the first post in a series on
diff --git a/content/blog/02_spa_agda_combining_lattices.md b/content/blog/02_spa_agda_combining_lattices.md
index 44292ea..54a1214 100644
--- a/content/blog/02_spa_agda_combining_lattices.md
+++ b/content/blog/02_spa_agda_combining_lattices.md
@@ -3,6 +3,7 @@ title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 2:
 series: "Static Program Analysis in Agda"
 date: 2024-04-13T14:23:03-07:01
 draft: true
+tags: ["Agda", "Programming Languages"]
 ---
 
 In the previous post, I wrote about how lattices arise when tracking, comparing