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.