Erasing irrelevant information while retaining the verification of dependent types.

This obscure class of polymorphism acts as an interesting replacement for subtyping.

What are Algebraic Data Types and what can we do with them?

What is type theory and how is it used?

I've made a lot of toy language projects, here's a list of them!

Description of an algorithm to replace Heap Allocations with Stack Allocations.