Syntax

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.