---
title: How I learnt to love typed λ-calculus
subtitle: "**A NewCrafts 2025 Hands-On Lab**"
date: 2025-11-06
author:
- Arnaud Bailly
- Emmanuel Gaillot
---

## Introduction

> An experimental workshop to explore the computational foundation of the universe, and have fun

---

![](./biface.jpg)

## λ-Calculus Syntax

A term from the λ-Calculus is either:

* A _Symbol_: `x`, `y`, `Foo`, `++`...
* An _Abstraction_: `(lam (x) x)`
* An _Application_: `(foo bar)`

## λ-Calculus Rules

Terms from the λ-Calculus can be _rewritten_ using various rules the two main ones being:

* α-renaming:

  > `(lam (x) x)` ⟹ `(lam (y) y)`
* β-reduction:

  > `((lam (x) body) term)` ⟹ `body[x ← term]`

## λ-Calculus Extensions

* Syntactic sugar:
  * `(lam (x) (lam (y) y))` ⟹ `(lam (x y) y)`
  * `((foo bar) baz)`  ⟹ `(foo bar baz)`
* Local definitions: `(let ((id (lam (x) x))) (id foo))`
* Global definitions: `(def id (lam (x) x))`

## λ-Calculus Extensions

* Primitive data:
  * booleans: `true`, `false`
  * numbers: `12`, `0.27`
  * strings: `"λ-calculus rocks"`

## Typed λ-Calculus

* The λ-Calculus is the favorite playground of type theorists
* There's a whole zoo of type systems we won't dive into (see you next year!)
* Search for _λ Cube_online...
* We'll introduce _Simply Typed λ-Calculus_ aka. $\lambda_{\rightarrow}$

## The Code

![](./repo.jpg)

## Action

![](./eruption.jpg)

## Conclusion

![](./gatsby.jpeg)