From 002e8883709214c96a171d216af3868fe34ceeb9 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Thu, 6 Nov 2025 07:17:25 +0100 Subject: revealjs version of slides --- lambda-calcul/support/custom.css | 15 ++ lambda-calcul/support/newcrafts-2025.html | 307 ++++++++++++++++++++++++++++++ lambda-calcul/support/newcrafts-2025.md | 20 +- 3 files changed, 334 insertions(+), 8 deletions(-) create mode 100644 lambda-calcul/support/custom.css create mode 100644 lambda-calcul/support/newcrafts-2025.html (limited to 'lambda-calcul') diff --git a/lambda-calcul/support/custom.css b/lambda-calcul/support/custom.css new file mode 100644 index 0000000..abdea26 --- /dev/null +++ b/lambda-calcul/support/custom.css @@ -0,0 +1,15 @@ +.reveal h1, +.reveal h2, +.reveal h3, +.reveal h4, +.reveal h5, +.reveal h6 { + text-transform: none; +} + +code { + background-color: #111; + color: #f8f8f2; + padding: 2px 4px; + font-style: normal; +} diff --git a/lambda-calcul/support/newcrafts-2025.html b/lambda-calcul/support/newcrafts-2025.html new file mode 100644 index 0000000..c4e4429 --- /dev/null +++ b/lambda-calcul/support/newcrafts-2025.html @@ -0,0 +1,307 @@ + + + + + + + + + How I learnt to love typed λ-calculus + + + + + + + + + + +
+
+ +
+

How I learnt to love typed λ-calculus

+

A NewCrafts 2025 Hands-On Lab

+

Arnaud Bailly

+

Emmanuel Gaillot

+

2025-11-06

+
+ +
+

Introduction

+
+

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

+
+
+
+ +

+
+
+

λ-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. λ→
    • +
+
+
+

The Code

+

+
+
+

Action

+

+
+
+

Conclusion

+

+
+
+
+ + + + + + + + + + + diff --git a/lambda-calcul/support/newcrafts-2025.md b/lambda-calcul/support/newcrafts-2025.md index 713e3e5..3506d52 100644 --- a/lambda-calcul/support/newcrafts-2025.md +++ b/lambda-calcul/support/newcrafts-2025.md @@ -13,7 +13,7 @@ author: --- -![](biface.jpg) +![](./biface.jpg) ## λ-Calculus Syntax @@ -27,8 +27,12 @@ A term from the λ-Calculus is either: 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]` +* α-renaming: + + > `(lam (x) x)` ⟹ `(lam (y) y)` +* β-reduction: + + > `((lam (x) body) term)` ⟹ `body[x ← term]` ## λ-Calculus Extensions @@ -38,14 +42,14 @@ Terms from the λ-Calculus can be _rewritten_ using various rules the two main o * 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"` -## λ-Calculus Typing +## 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!) @@ -54,12 +58,12 @@ Terms from the λ-Calculus can be _rewritten_ using various rules the two main o ## The Code -![](repo.jpg) +![](./repo.jpg) ## Action -![](eruption.jpg) +![](./eruption.jpg) ## Conclusion -![](gatsby.jpeg) +![](./gatsby.jpeg) -- cgit v1.3.1