12 lines
445 B
Markdown
12 lines
445 B
Markdown
|
+++
|
||
|
|
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"
|
||
|
|
+++
|