From b2ee60e31ea7f4b48a84269c41e7db7ffaaa061f Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Wed, 5 Nov 2025 18:37:45 +0100 Subject: add slides for newcrafts --- lambda-calcul/support/newcrafts-2025.md | 61 +++++++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 lambda-calcul/support/newcrafts-2025.md (limited to 'lambda-calcul/support/newcrafts-2025.md') diff --git a/lambda-calcul/support/newcrafts-2025.md b/lambda-calcul/support/newcrafts-2025.md new file mode 100644 index 0000000..c80e453 --- /dev/null +++ b/lambda-calcul/support/newcrafts-2025.md @@ -0,0 +1,61 @@ +--- +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))` + +---- + +* Primitive data: + * booleans: `true`, `false` + * numbers: `12`, `0.27` + * strings: `"λ-calculus rocks"` + +## λ-Calculus Typing + +* 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}$ + +## Action + +![](eruption.jpg) + +## Conclusion + +![](gatsby.jpeg) -- cgit v1.3.1