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

+++ 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" divider = ", " +++