add slides for newcrafts

1 files changed, 61 insertions, 0 deletions

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)