Simpler Category Theory
Category theory seems to be all the rage in cutting-edge programming language research and in typed functional programming. This post offers a simple entrypoint. Read more here !
Ryan's Blog
Ryan Brewer's personal blog, covering ideas in programming languages, software, logic, abstract math, and analytic philosophy.
Latest posts
Speaking on Type Theory Forall
I had the absolute honor to be invited as a guest on the Type Theory Forall podcast! We talked about how to learn programming language theory when you're outside of academia, as well as some political notes on the practice of science and engineering, and some updates on my personal work around the time of the recording. Read more here !
Par Part 3: Par, Continued
Par is notoriously difficult to understand, but mostly due to a lack of resources. This post hopes to build on the prior posts on sequent calculus and linear logic to show how par is not such an alien concept after all, and make the theory much more accessible. We'll naturally stumble into constructive/computational classical logic along the way! Read more here !
Par Part 2: Linear Logic
Linear logic is a beautiful logical system taking advantage of the mechanisms of the sequent calculus. In this post we explore the various meanings of linear logic, and dig deep into the reasoning behind its peculiar development. Read more here !
Par Part 1: Sequent Calculus
Sequent Calculus is a way of doing logic that's very explicit and mechanical. It's used as an important system and notation for type theory and logic related to programming languages. Read more here !
The Cricket Language
Cricket is a lazy gradually-typed functional language with objects. It's very tiny but very expressive; anyone can implement it themselves! Read more here !
Getting Started with Category Theory
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. Read more here !
The Type of Sprintf
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! Read more here !
Simple Programming Languages
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? Read more here !
Advanced Typechecking for Stack-Based Languages
This post discusses the interesting typechecker of SaberVM, which uses a stack-based bytecode language with a powerful type system. Read more here !
A Beginner's Guide to Programming Language Academia
This post briefly maps out many different subfields of programming language theory, in an effort to make it more accessible to those outside academia. Read more here !
Safe Manual Memory Management with Coeffects
Using ideas from Crary et al.'s Calculus of Capabilities, I discuss the coeffectful memory management used in SaberVM. Read more here !
Announcing the Saber Virtual Machine
This post announces SaberVM, an abstract machine for functional programs that guarantees safety, reliability, and portability. Read more here !
Security and Crashing with Modal Logic
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. Read more here !
Implicit Products: A Better Type-Theoretic "Forall"
Implicit products are a fascinating approach to universal quantification in dependent type theory, as well as proof irrelevance/erasure in compiler implementation. Read more here !
An Introduction to Proofs with Dependent Types
This post introduces the basic ideas behind dependent-type-based proof assistants, and expressing logic with types and values. Read more here !
My First Blog Post
A test post for the blog. Read more here !