revealjs version of slides

3 files changed, 334 insertions, 8 deletions

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 @@
+<!DOCTYPE html>
+<html>
+<head>
+  <meta charset="utf-8">
+  <meta name="generator" content="pandoc">
+  <meta name="author" content="Arnaud Bailly">
+  <meta name="author" content="Emmanuel Gaillot">
+  <meta name="dcterms.date" content="2025-11-06">
+  <title>How I learnt to love typed λ-calculus</title>
+  <meta name="apple-mobile-web-app-capable" content="yes">
+  <meta name="apple-mobile-web-app-status-bar-style" content="black-translucent">
+  <meta name="viewport" content="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no, minimal-ui">
+  <link rel="stylesheet" href="https://unpkg.com/reveal.js@^5/dist/reset.css">
+  <link rel="stylesheet" href="https://unpkg.com/reveal.js@^5/dist/reveal.css">
+  <style>
+    .reveal .sourceCode {  /* see #7635 */
+      overflow: visible;
+    }
+    /* Default styles provided by pandoc.
+    ** See https://pandoc.org/MANUAL.html#variables-for-html for config info.
+    */
+    code{white-space: pre-wrap;}
+    span.smallcaps{font-variant: small-caps;}
+    div.columns{display: flex; gap: min(4vw, 1.5em);}
+    div.column{flex: auto; overflow-x: auto;}
+    div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
+    /* The extra [class] is a hack that increases specificity enough to
+       override a similar rule in reveal.js */
+    ul.task-list[class]{list-style: none;}
+    ul.task-list li input[type="checkbox"] {
+      font-size: inherit;
+      width: 0.8em;
+      margin: 0 0.8em 0.2em -1.6em;
+      vertical-align: middle;
+    }
+    .display.math{display: block; text-align: center; margin: 0.5rem auto;}
+  </style>
+  <link rel="stylesheet" href="https://unpkg.com/reveal.js@^5/dist/theme/moon.css" id="theme">
+  <link rel="stylesheet" href="./custom.css"/>
+</head>
+<body>
+  <div class="reveal">
+    <div class="slides">
+
+<section id="title-slide">
+  <h1 class="title">How I learnt to love typed λ-calculus</h1>
+  <p class="subtitle"><strong>A NewCrafts 2025 Hands-On Lab</strong></p>
+  <p class="author">Arnaud Bailly</p>
+  <p class="author">Emmanuel Gaillot</p>
+  <p class="date">2025-11-06</p>
+</section>
+
+<section id="introduction" class="slide level2">
+<h2>Introduction</h2>
+<blockquote>
+<p>An experimental workshop to explore the computational foundation of
+the universe, and have fun</p>
+</blockquote>
+</section>
+<section class="slide level2">
+
+<p><img data-src="./biface.jpg" /></p>
+</section>
+<section id="λ-calculus-syntax" class="slide level2">
+<h2>λ-Calculus Syntax</h2>
+<p>A term from the λ-Calculus is either:</p>
+<ul>
+<li class="fragment">A <em>Symbol</em>: <code>x</code>, <code>y</code>,
+<code>Foo</code>, <code>++</code>…</li>
+<li class="fragment">An <em>Abstraction</em>:
+<code>(lam (x) x)</code></li>
+<li class="fragment">An <em>Application</em>:
+<code>(foo bar)</code></li>
+</ul>
+</section>
+<section id="λ-calculus-rules" class="slide level2">
+<h2>λ-Calculus Rules</h2>
+<p>Terms from the λ-Calculus can be <em>rewritten</em> using various
+rules the two main ones being:</p>
+<ul>
+<li class="fragment"><p>α-renaming:</p>
+<blockquote>
+<p><code>(lam (x) x)</code> ⟹ <code>(lam (y) y)</code></p>
+</blockquote></li>
+<li class="fragment"><p>β-reduction:</p>
+<blockquote>
+<p><code>((lam (x) body) term)</code> ⟹ <code>body[x ← term]</code></p>
+</blockquote></li>
+</ul>
+</section>
+<section id="λ-calculus-extensions" class="slide level2">
+<h2>λ-Calculus Extensions</h2>
+<ul>
+<li class="fragment">Syntactic sugar:
+<ul>
+<li class="fragment"><code>(lam (x) (lam (y) y))</code> ⟹
+<code>(lam (x y) y)</code></li>
+<li class="fragment"><code>((foo bar) baz)</code> ⟹
+<code>(foo bar baz)</code></li>
+</ul></li>
+<li class="fragment">Local definitions:
+<code>(let ((id (lam (x) x))) (id foo))</code></li>
+<li class="fragment">Global definitions:
+<code>(def id (lam (x) x))</code></li>
+</ul>
+</section>
+<section id="λ-calculus-extensions-1" class="slide level2">
+<h2>λ-Calculus Extensions</h2>
+<ul>
+<li class="fragment">Primitive data:
+<ul>
+<li class="fragment">booleans: <code>true</code>,
+<code>false</code></li>
+<li class="fragment">numbers: <code>12</code>, <code>0.27</code></li>
+<li class="fragment">strings: <code>"λ-calculus rocks"</code></li>
+</ul></li>
+</ul>
+</section>
+<section id="typed-λ-calculus" class="slide level2">
+<h2>Typed λ-Calculus</h2>
+<ul>
+<li class="fragment">The λ-Calculus is the favorite playground of type
+theorists</li>
+<li class="fragment">There’s a whole zoo of type systems we won’t dive
+into (see you next year!)</li>
+<li class="fragment">Search for _λ Cube_online…</li>
+<li class="fragment">We’ll introduce <em>Simply Typed λ-Calculus</em>
+aka. <span class="math inline"><em>λ</em><sub>→</sub></span></li>
+</ul>
+</section>
+<section id="the-code" class="slide level2">
+<h2>The Code</h2>
+<p><img data-src="./repo.jpg" /></p>
+</section>
+<section id="action" class="slide level2">
+<h2>Action</h2>
+<p><img data-src="./eruption.jpg" /></p>
+</section>
+<section id="conclusion" class="slide level2">
+<h2>Conclusion</h2>
+<p><img data-src="./gatsby.jpeg" /></p>
+</section>
+    </div>
+  </div>
+
+  <script src="https://unpkg.com/reveal.js@^5/dist/reveal.js"></script>
+
+  <!-- reveal.js plugins -->
+  <script src="https://unpkg.com/reveal.js@^5/plugin/notes/notes.js"></script>
+  <script src="https://unpkg.com/reveal.js@^5/plugin/search/search.js"></script>
+  <script src="https://unpkg.com/reveal.js@^5/plugin/zoom/zoom.js"></script>
+
+  <script>
+
+      // Full list of configuration options available at:
+      // https://revealjs.com/config/
+      Reveal.initialize({
+        // Display controls in the bottom right corner
+        controls: true,
+
+        // Help the user learn the controls by providing hints, for example by
+        // bouncing the down arrow when they first encounter a vertical slide
+        controlsTutorial: true,
+
+        // Determines where controls appear, "edges" or "bottom-right"
+        controlsLayout: 'bottom-right',
+
+        // Visibility rule for backwards navigation arrows; "faded", "hidden"
+        // or "visible"
+        controlsBackArrows: 'faded',
+
+        // Display a presentation progress bar
+        progress: true,
+
+        // Display the page number of the current slide
+        slideNumber: false,
+
+        // 'all', 'print', or 'speaker'
+        showSlideNumber: 'all',
+
+        // Add the current slide number to the URL hash so that reloading the
+        // page/copying the URL will return you to the same slide
+        hash: true,
+
+        // Start with 1 for the hash rather than 0
+        hashOneBasedIndex: false,
+
+        // Flags if we should monitor the hash and change slides accordingly
+        respondToHashChanges: true,
+
+        // Push each slide change to the browser history
+        history: false,
+
+        // Enable keyboard shortcuts for navigation
+        keyboard: true,
+
+        // Enable the slide overview mode
+        overview: true,
+
+        // Disables the default reveal.js slide layout (scaling and centering)
+        // so that you can use custom CSS layout
+        disableLayout: false,
+
+        // Vertical centering of slides
+        center: true,
+
+        // Enables touch navigation on devices with touch input
+        touch: true,
+
+        // Loop the presentation
+        loop: false,
+
+        // Change the presentation direction to be RTL
+        rtl: false,
+
+        // see https://revealjs.com/vertical-slides/#navigation-mode
+        navigationMode: 'default',
+
+        // Randomizes the order of slides each time the presentation loads
+        shuffle: false,
+
+        // Turns fragments on and off globally
+        fragments: true,
+
+        // Flags whether to include the current fragment in the URL,
+        // so that reloading brings you to the same fragment position
+        fragmentInURL: true,
+
+        // Flags if the presentation is running in an embedded mode,
+        // i.e. contained within a limited portion of the screen
+        embedded: false,
+
+        // Flags if we should show a help overlay when the questionmark
+        // key is pressed
+        help: true,
+
+        // Flags if it should be possible to pause the presentation (blackout)
+        pause: true,
+
+        // Flags if speaker notes should be visible to all viewers
+        showNotes: false,
+
+        // Global override for autoplaying embedded media (null/true/false)
+        autoPlayMedia: null,
+
+        // Global override for preloading lazy-loaded iframes (null/true/false)
+        preloadIframes: null,
+
+        // Number of milliseconds between automatically proceeding to the
+        // next slide, disabled when set to 0, this value can be overwritten
+        // by using a data-autoslide attribute on your slides
+        autoSlide: 0,
+
+        // Stop auto-sliding after user input
+        autoSlideStoppable: true,
+
+        // Use this method for navigation when auto-sliding
+        autoSlideMethod: null,
+
+        // Specify the average time in seconds that you think you will spend
+        // presenting each slide. This is used to show a pacing timer in the
+        // speaker view
+        defaultTiming: null,
+
+        // Enable slide navigation via mouse wheel
+        mouseWheel: false,
+
+        // The display mode that will be used to show slides
+        display: 'block',
+
+        // Hide cursor if inactive
+        hideInactiveCursor: true,
+
+        // Time before the cursor is hidden (in ms)
+        hideCursorTime: 5000,
+
+        // Opens links in an iframe preview overlay
+        previewLinks: false,
+
+        // Transition style (none/fade/slide/convex/concave/zoom)
+        transition: 'slide',
+
+        // Transition speed (default/fast/slow)
+        transitionSpeed: 'default',
+
+        // Transition style for full page slide backgrounds
+        // (none/fade/slide/convex/concave/zoom)
+        backgroundTransition: 'fade',
+
+        // Number of slides away from the current that are visible
+        viewDistance: 3,
+
+        // Number of slides away from the current that are visible on mobile
+        // devices. It is advisable to set this to a lower number than
+        // viewDistance in order to save resources.
+        mobileViewDistance: 2,
+
+        // reveal.js plugins
+        plugins: [
+          RevealNotes,
+          RevealSearch,
+          RevealZoom
+        ]
+      });
+    </script>
+    </body>
+</html>
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)