This post discusses the interesting typechecker of SaberVM, which uses a stack-based bytecode language with a powerful type system.
This post briefly maps out many different subfields of programming language theory, in an effort to make it more accessible to those outside academia.
Using ideas from Crary et al.'s Calculus of Capabilities, I discuss the coeffectful memory management used in SaberVM.
This post announces SaberVM, an abstract machine for functional programs that guarantees safety, reliability, and portability.
Modal logic is a beautiful field of logic that can be applied to computer science in a few ways, one of which we explore in this post. It can elucidate security concepts and how and why to crash software.
Implicit products are a fascinating approach to universal quantification in dependent type theory, as well as proof irrelevance/erasure in compiler implementation.
This post introduces the basic ideas behind dependent-type-based proof assistants, and expressing logic with types and values.
A test post for the blog.