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.
-
A Language for an Assignment
Series status: Suspended
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.
-
Advent of Code in Coq
Series status: Suspended
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.
-
Compiling a Functional Language using C++
Series status: Complete
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.
-
Meaningfully Typechecking a Language in Idris
Series status: Complete
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.