Update theme with support for series

config.toml

@@ -6,6 +6,12 @@ summaryLength = 20
 
 defaultContentLanguage = 'en'
 
+
+
+[taxonomies]
+  tag = 'tags'
+  series = "series"
+
 [outputFormats]
   [outputFormats.Toml]
     name = "toml"

content/blog/00_aoc_coq.md

@@ -2,6 +2,7 @@
 title: "Advent of Code in Coq - Day 1"
 date: 2020-12-02T18:44:56-08:00
 tags: ["Advent of Code", "Coq"]
+series: "Advent of Code in Coq"
 favorite: true
 ---
 

content/blog/00_compiler_intro.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 0 - Intro
 date: 2019-08-03T01:02:30-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this first post of a larger series, we embark on a journey of developing a compiler for a lazily evaluated functional language."
 ---
 During my last academic term, I was enrolled in a compilers course.

content/blog/00_cs325_languages_hw1.md

@@ -2,6 +2,7 @@
 title: A Language for an Assignment - Homework 1
 date: 2019-12-27T23:27:09-08:00
 tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
+series: "A Language for an Assignment"
 ---
 
 On a rainy Oregon day, I was walking between classes with a group of friends.

content/blog/00_types_intro.md

@@ -2,6 +2,7 @@
 title: "Everything I Know About Types: Introduction"
 date: 2022-06-26T18:36:01-07:00
 tags: ["Type Systems", "Programming Languages"]
+series: "Everything I Know About Types"
 draft: true
 ---
 

content/blog/01_aoc_coq.md

@@ -2,6 +2,7 @@
 title: "Advent of Code in Coq - Day 8"
 date: 2021-01-10T22:48:39-08:00
 tags: ["Advent of Code", "Coq"]
+series: "Advent of Code in Coq"
 ---
 
 Huh? We're on day 8? What happened to days 2 through 7?

content/blog/01_compiler_tokenizing.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 1 - Tokenizing
 date: 2019-08-03T01:02:30-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this post, we tackle the first component of our compiler: tokenizing."
 ---
 It makes sense to build a compiler bit by bit, following the stages we outlined in

content/blog/01_cs325_languages_hw2.md

@@ -2,6 +2,7 @@
 title: A Language for an Assignment - Homework 2
 date: 2019-12-30T20:05:10-08:00
 tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
+series: "A Language for an Assignment"
 ---
 
 After the madness of the

content/blog/01_types_basics.md

@@ -2,6 +2,7 @@
 title: "Everything I Know About Types: Basics"
 date: 2022-06-30T19:08:50-07:00
 tags: ["Type Systems", "Programming Languages"]
+series: "Everything I Know About Types"
 draft: true
 ---
 

content/blog/02_compiler_parsing.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 2 - Parsing
 date: 2019-08-03T01:02:30-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this post, we combine our compiler's tokenizer with a parser, allowing us to extract structure from input source code."
 ---
 In the previous post, we covered tokenizing. We learned how to convert an input string into logical segments, and even wrote up a tokenizer to do it according to the rules of our language. Now, it's time to make sense of the tokens, and parse our language.

content/blog/02_cs325_languages_hw3.md

@@ -2,6 +2,7 @@
 title: A Language for an Assignment - Homework 3
 date: 2020-01-02T22:17:43-08:00
 tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
+series: "A Language for an Assignment"
 ---
 
 It rained in Sunriver on New Year's Eve, and it continued to rain

content/blog/02_types_variables.md

@@ -2,6 +2,7 @@
 title: "Everything I Know About Types: Variables"
 date: 2022-08-28T19:05:31-07:00
 tags: ["Type Systems", "Programming Languages"]
+series: "Everything I Know About Types"
 draft: true
 ---
 

content/blog/03_compiler_typechecking.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 3 - Type Checking
 date: 2019-08-06T14:26:38-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this post, we allow our compiler to throw away invalid programs, detected using a monomorphic typechecking algorithm."
 ---
 I think tokenizing and parsing are boring. The thing is, looking at syntax

content/blog/04_compiler_improvements.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 4 - Small Improvements
 date: 2019-08-06T14:26:38-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this post, we take a little break from pushing our compiler forward to make some improvements to the code we've written so far."
 ---
 We've done quite a big push in the previous post. We defined

content/blog/05_compiler_execution.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 5 - Execution
 date: 2019-08-06T14:26:38-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this post, we define the rules for a G-machine, the abstract machine that we will target with our compiler."
 ---
 {{< gmachine_css >}}

content/blog/06_compiler_compilation.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 6 - Compilation
 date: 2019-08-06T14:26:38-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this post, we enable our compiler to convert programs written in our functional language to G-machine instructions."
 ---
 In the previous post, we defined a machine for graph reduction,

content/blog/07_compiler_runtime.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 7 - Runtime
 date: 2019-08-06T14:26:38-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this post, we implement the supporting code that will be shared between all executables our compiler will create."
 ---
 Wikipedia has the following definition for a __runtime__:

content/blog/08_compiler_llvm.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 8 - LLVM
 date: 2019-10-30T22:16:22-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this post, we enable our compiler to convert G-machine instructions to LLVM IR, which finally allows us to generate working executables."
 ---
 

content/blog/09_compiler_garbage_collection.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 9 - Garbage Collection
 date: 2020-02-10T19:22:41-08:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this post, we implement a garbage collector that frees memory no longer used by the executables our compiler creates."
 ---
 

content/blog/10_compiler_polymorphism.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 10 - Polymorphism
 date: 2020-03-25T17:14:20-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this post, we extend our compiler's typechecking algorithm to implement the Hindley-Milner type system, allowing for polymorphic functions."
 favorite: true
 ---

content/blog/11_compiler_polymorphic_data_types.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 11 - Polymorphic Data Types
 date: 2020-04-14T19:05:42-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this post, we enable our compiler to understand polymorphic data types."
 ---
 [In part 10]({{< relref "10_compiler_polymorphism.md" >}}), we managed to get our

content/blog/12_compiler_let_in_lambda/index.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 12 - Let/In and Lambdas
 date: 2020-06-21T00:50:07-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this post, we extend our language with let/in expressions and lambda functions."
 ---
 

content/blog/13_compiler_cleanup/index.md

@@ -2,6 +2,7 @@
 title: Compiling a Functional Language Using C++, Part 13 - Cleanup
 date: 2020-09-19T16:14:13-07:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
+series: "Compiling a Functional Language using C++"
 description: "In this post, we clean up our compiler."
 ---
 

content/blog/haskell_newtype.md

@@ -1,6 +1,7 @@
 ---
 title: "Multiple Typeclass Instances using Newtype in Haskell"
 date: 2022-04-28T23:09:42-07:00
+expirydate: 2022-04-28T23:09:42-07:00
 tags: ["Haskell"]
 draft: true
 ---

content/blog/idris_catamorphisms.md

@@ -1,6 +1,7 @@
 ---
 title: "Induction Principles from Base Functors"
 date: 2022-04-22T12:19:22-07:00
+expirydate: 2022-04-22T12:19:22-07:00
 tags: ["Idris"]
 draft: true
 ---

content/blog/typeclasses_are_logic.md

@@ -1,6 +1,7 @@
 ---
 title: Typeclasses are Basically Logic Programming
 date: 2021-06-28T17:11:38-07:00
+expirydate: 2021-06-28T17:11:38-07:00
 draft: true
 description: "In this post, we explore the connection between typeclasses and logic programming."
 tags: ["Haskell", "Prolog"]

content/blog/typesafe_interpreter.md

@@ -2,6 +2,7 @@
 title: Meaningfully Typechecking a Language in Idris
 date: 2020-02-27T21:58:55-08:00
 tags: ["Haskell", "Idris", "Programming Languages"]
+series: "Meaningfully Typechecking a Language in Idris"
 ---
 
 This term, I'm a TA for Oregon State University's Programming Languages course.

content/blog/typesafe_interpreter_revisited.md

@@ -2,6 +2,7 @@
 title: Meaningfully Typechecking a Language in Idris, Revisited
 date: 2020-07-22T14:37:35-07:00
 tags: ["Idris", "Programming Languages"]
+series: "Meaningfully Typechecking a Language in Idris"
 favorite: true
 ---
 

content/blog/typesafe_interpreter_tuples.md

@@ -2,6 +2,7 @@
 title: Meaningfully Typechecking a Language in Idris, With Tuples
 date: 2020-08-12T15:48:04-07:00
 tags: ["Idris", "Programming Languages"]
+series: "Meaningfully Typechecking a Language in Idris"
 ---
 
 Some time ago, I wrote a post titled

content/series/_index.md

@@ -0,0 +1,6 @@
+---
+title: "Series"
+---
+Sometimes, content about the same topic is best organized into multiple posts.
+The following series span multiple articles, but have a common overarching
+theme.

content/series/a-language-for-an-assignment/_index.md

@@ -0,0 +1,10 @@
++++
+title = "A Language for an Assignment"
+summary = """
+  In this series, I create a brand new programming language for each homework
+  assignment of my algorithms class. I try to make the language whimsical
+  and specialized to only the problem at hand. The languages are implemented
+  using Haskell, and translate to Python.
+  """
+status = "suspended"
++++

content/series/advent-of-code-in-coq/_index.md

@@ -0,0 +1,9 @@
++++
+title = "Advent of Code in Coq"
+summary = """
+  In this series, I apply the Coq proof assistant to formalize solutions to the
+  puzzles to Advent of Code 2020. That is, I try to solve the problem, and
+  formally prove that the solution is correct.
+  """
+status = "suspended"
++++

content/series/compiling-a-functional-language-using-c++/_index.md

@@ -0,0 +1,11 @@
++++
+title = "Compiling a Functional Language using C++"
+summary = """
+  This series covers the implementation of a compiler for a lazily evaluated
+  functional language using C++ and LLVM. The language is initially based on
+  my project for a university course in compilers, but is extended with many
+  additional features, such as polymorphism, let-in expressions, and
+  polymorphism.
+  """
+status = "complete"
++++

content/series/everything-i-know-about-types/_index.md

@@ -0,0 +1,10 @@
++++
+title = "Everything I Know About Types"
+summary = """
+  In this series, I try to write down and organize all I know about type systems.
+  Most of this knowledge was acquired over my time as a researcher in the field
+  of programming languages at Oregon State University.
+  """
+status = "ongoing"
+draft = true
++++

content/series/meaningfully-typechecking-a-language-in-idris/_index.md

@@ -0,0 +1,11 @@
++++
+title = "Meaningfully Typechecking a Language in Idris"
+summary = """
+  In this series, I use the dependently-typed programming language Idris to
+  implement relatively simple typechecking of a simple object language.
+  However, I do so with a twist: the typechecker produces expressions
+  that are guaranteed to be safe to evaluate. The interpreter then
+  doesn't have to worry about checking for type errors.
+  """
+status = "complete"
++++

themes/vanilla

@@ -1 +1 @@
-Subproject commit e7cada3764d9700e9d29134bc07571cc29d1572f
+Subproject commit e431d65659148919ae8c60d1c1873abd039c40be