diff options
| author | Arnaud Bailly <arnaud@pankzsoft.com> | 2025-11-06 07:17:25 +0100 |
|---|---|---|
| committer | Arnaud Bailly <arnaud@pankzsoft.com> | 2025-11-06 07:17:25 +0100 |
| commit | 002e8883709214c96a171d216af3868fe34ceeb9 (patch) | |
| tree | 7de6649eda8753dfcea2d6e9c6a37c52a9b11c78 /lambda-calcul/support/newcrafts-2025.html | |
| parent | 3cde28ec7c9c30cfb22bee4906944a55f9f9a8ab (diff) | |
| download | lambda-nantes-002e8883709214c96a171d216af3868fe34ceeb9.tar.gz | |
revealjs version of slides
Diffstat (limited to 'lambda-calcul/support/newcrafts-2025.html')
| -rw-r--r-- | lambda-calcul/support/newcrafts-2025.html | 307 |
1 files changed, 307 insertions, 0 deletions
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> |
