Cricket is a lazy gradually-typed functional language with objects. It's very tiny but very expressive; anyone can implement it themselves!
Category theory is a beautiful and powerful field but it can feel impenetrable without the right entry point. This post hopes to serve as a sort of beginner's guide and reference.
Most static type systems wouldn't let you make something like sprintf, whose type is determined by a format string. Dependent types can save the day!
Simple programming languages are wonderful to work in. But what is it about them that actually makes them simple? And why do we like that so much?
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.
© 2024 Ryan Brewer.