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/2025-10-09.md | 30 +++------------ lambda-calcul/support/2025-10-09.pdf | Bin 54912 -> 12699 bytes lambda-calcul/support/Makefile | 6 +-- lambda-calcul/support/biface.jpg | Bin 0 -> 89013 bytes lambda-calcul/support/eruption.jpg | Bin 0 -> 500131 bytes lambda-calcul/support/gatsby.jpeg | Bin 0 -> 118228 bytes lambda-calcul/support/newcrafts-2025.md | 61 +++++++++++++++++++++++++++++++ lambda-calcul/support/newcrafts-2025.pdf | Bin 0 -> 764907 bytes 8 files changed, 70 insertions(+), 27 deletions(-) create mode 100644 lambda-calcul/support/biface.jpg create mode 100644 lambda-calcul/support/eruption.jpg create mode 100644 lambda-calcul/support/gatsby.jpeg create mode 100644 lambda-calcul/support/newcrafts-2025.md create mode 100644 lambda-calcul/support/newcrafts-2025.pdf diff --git a/lambda-calcul/support/2025-10-09.md b/lambda-calcul/support/2025-10-09.md index 66ec5a8..2f14e67 100644 --- a/lambda-calcul/support/2025-10-09.md +++ b/lambda-calcul/support/2025-10-09.md @@ -1,7 +1,7 @@ --- -title: λ-Nantes Workshop 2bis -subtitle: Apprenons à aimer le λ-calcul simplement typé -date: 2025-10-09 +title: How I learnt to love typed λ-calculus +subtitle: An experimental workshop to explore the computational foundation of the universe, and have fun +date: 2025-11-06 --- ## Agenda @@ -10,26 +10,8 @@ date: 2025-10-09 * Action * Conclusion -# Introduction +## Introduction -## Rappel de l'épisode précédent +## Action -* On a codé un λ-calcul non typé en Rust, Elixir, Clojure et Java -* En jouant contre un serveur nous envoyant des expressions à évaluer -* On s'est bien amusé -* On veut aller plus loin - -## Rappel de l'épisode précédent - -Pour accéder au repository, c'est par là ⇒ - -![Lambda-Nantes code](qrcode.jpg) - -## Aujourd'hui - -* On passe à la vitesse supérieure en ajoutant des types simples au λ-calcul -* Cela donne le _λ-calcul simplement typé_ - -## Aujourd'hui - -![λ-calcul simplement typé](typing-rules.png) +## Conclusion diff --git a/lambda-calcul/support/2025-10-09.pdf b/lambda-calcul/support/2025-10-09.pdf index 452217b..1e61b7c 100644 Binary files a/lambda-calcul/support/2025-10-09.pdf and b/lambda-calcul/support/2025-10-09.pdf differ diff --git a/lambda-calcul/support/Makefile b/lambda-calcul/support/Makefile index 960c5a0..f54b70a 100644 --- a/lambda-calcul/support/Makefile +++ b/lambda-calcul/support/Makefile @@ -1,11 +1,11 @@ -all: 2024-10-10.pdf 2025-10-09.pdf +all: 2024-10-10.pdf 2025-10-09.pdf newcrafts-2025.pdf %.pdf: %.md pandoc -t beamer -f markdown+implicit_figures \ -i -V theme:default -V aspectratio:169 \ --pdf-engine=xelatex \ - -V monofont='mononoki' \ - -V mainfont='mononoki' \ + -V monofont='DejaVu Sans Mono' \ + -V mainfont='DejaVu Sans' \ $(<) -o $(@) clean: diff --git a/lambda-calcul/support/biface.jpg b/lambda-calcul/support/biface.jpg new file mode 100644 index 0000000..0fe28bd Binary files /dev/null and b/lambda-calcul/support/biface.jpg differ diff --git a/lambda-calcul/support/eruption.jpg b/lambda-calcul/support/eruption.jpg new file mode 100644 index 0000000..5783314 Binary files /dev/null and b/lambda-calcul/support/eruption.jpg differ diff --git a/lambda-calcul/support/gatsby.jpeg b/lambda-calcul/support/gatsby.jpeg new file mode 100644 index 0000000..a8c6d30 Binary files /dev/null and b/lambda-calcul/support/gatsby.jpeg differ 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) diff --git a/lambda-calcul/support/newcrafts-2025.pdf b/lambda-calcul/support/newcrafts-2025.pdf new file mode 100644 index 0000000..086dbc9 Binary files /dev/null and b/lambda-calcul/support/newcrafts-2025.pdf differ -- cgit v1.3.1