Semantics

August, 2023

The art of binding

variables made complicated

Introduction and pedantry §

In programming, we typically think of a variable as a location to store a value. It turns out this is mostly an implementation detail; if we generalize them into their interface, we find a rich space of languages that captures the distinctions between several different types of programming language that seem very different at first glance.

February, 2023

λ-calculus for programmers

programming language fundamentals

Introduction §

If you’ve done much functional programming, you’ve probably heard of the λ-calculus, invented by Alonzo Church in the 1930s. If you haven’t, the term might be quite new to you; but don’t worry, despite the intimidating name the λ-calculus is actually very simple.

January, 2023

Linear types for programmers

reasoning about resources

Introduction §

Linear types are an application to type theory of the discipline of linear logic, first described by Jean-Yves Girard (Girard, 1987). Since its inception it has led to many fruitful discoveries in computer science. In this article I hope to explain why it is so interesting, as well as relate it to concrete tools and practices available to programmers today.