From 7f1b9d31ea8996ab5265a26a03bf8a51278cc627 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Tue, 31 Jan 2023 18:53:02 -0800
Subject: [PATCH] Add all the series pages

---
 config.toml                                           |  6 ++++++
 content/series/_index.md                              |  6 ++++++
 content/series/a-language-for-an-assignment/_index.md | 10 ++++++++++
 content/series/advent-of-code-in-coq/_index.md        |  9 +++++++++
 .../_index.md                                         | 11 +++++++++++
 .../series/everything-i-know-about-types/_index.md    | 10 ++++++++++
 .../_index.md                                         | 11 +++++++++++
 7 files changed, 63 insertions(+)
 create mode 100644 content/series/_index.md
 create mode 100644 content/series/a-language-for-an-assignment/_index.md
 create mode 100644 content/series/advent-of-code-in-coq/_index.md
 create mode 100644 content/series/compiling-a-functional-language-using-c++/_index.md
 create mode 100644 content/series/everything-i-know-about-types/_index.md
 create mode 100644 content/series/meaningfully-typechecking-a-language-in-idris/_index.md

diff --git a/config.toml b/config.toml
index e554f76..0e2c26f 100644
--- a/config.toml
+++ b/config.toml
@@ -6,6 +6,12 @@ summaryLength = 20
 
 defaultContentLanguage = 'en'
 
+
+
+[taxonomies]
+  tag = 'tags'
+  series = "series"
+
 [outputFormats]
   [outputFormats.Toml]
     name = "toml"
diff --git a/content/series/_index.md b/content/series/_index.md
new file mode 100644
index 0000000..1e51191
--- /dev/null
+++ b/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.
diff --git a/content/series/a-language-for-an-assignment/_index.md b/content/series/a-language-for-an-assignment/_index.md
new file mode 100644
index 0000000..c85afa2
--- /dev/null
+++ b/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"
++++
diff --git a/content/series/advent-of-code-in-coq/_index.md b/content/series/advent-of-code-in-coq/_index.md
new file mode 100644
index 0000000..bb6b039
--- /dev/null
+++ b/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"
++++
diff --git a/content/series/compiling-a-functional-language-using-c++/_index.md b/content/series/compiling-a-functional-language-using-c++/_index.md
new file mode 100644
index 0000000..3a4f701
--- /dev/null
+++ b/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"
++++
diff --git a/content/series/everything-i-know-about-types/_index.md b/content/series/everything-i-know-about-types/_index.md
new file mode 100644
index 0000000..02349d9
--- /dev/null
+++ b/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
++++
diff --git a/content/series/meaningfully-typechecking-a-language-in-idris/_index.md b/content/series/meaningfully-typechecking-a-language-in-idris/_index.md
new file mode 100644
index 0000000..32a7981
--- /dev/null
+++ b/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"
++++