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/newcrafts-2025.html | 307 ++++++++++++++++++++++++++++++ 1 file changed, 307 insertions(+) create mode 100644 lambda-calcul/support/newcrafts-2025.html (limited to 'lambda-calcul/support/newcrafts-2025.html') 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

+

+
+
+
+ + + + + + + + + + + -- cgit v1.3.1