Lambda World 2025
2025-10-23..2025-10-24
Cádiz, Spain
[Lambda World 2015, Lambda World 2016, Lambda World 2017, Lambda World 2024, Lambda World 2025]
who it's for
functional programmers, programming language designers, compiler engineers, Rust developers, Scala developers, verification engineers, tooling and IDE engineers
topics
Verse functional-logic language (UEFN); LLM plus SMT code synthesis; liquid and refinement types; terminating provers in Agda; OCaml multicore domains and effect handlers; Kotlin error handling with Arrow Raise; Warp UI DSL for F# code generation; Rust ADTs to advanced concurrency; comparison of Scala direct-style vs effect systems; SMT-backed refinement with Z3; FS2 aquascape stream visualization; Codeless Tools Rust clinical-data library
| title | author | length |
|---|---|---|
| Complexity is a Sin | Volodymyr Yaroslavskyi | 47m |
Defines three specific failure modes — structural complexity, cognitive complexity, and algorithmic complexity — and shows measurable impact: bubble sort… | ||
| Verse - A New Functional Logic Language | Lennart Augustsson | 42m |
Verse is a new functional‑logic language used inside Unreal Engine for Fortnite (UEFN) and driven by Tim Sweeney’s design. It combines logical variables and… | ||
| Evolving AI-Assisted Web UI Development in F#.. | Adam Granicz | 32m |
A practical pipeline converts natural-language UI intent into a refined external DSL called Warp UI DSL that generates and incrementally updates WebSharper F#… | ||
| Functional Rust: From ADTs to Advanced Concurrency | Stefano, Adrian | 36m |
Refactors a brittle payment pipeline into a state-typed system where amount becomes an integer, payment states are encoded as enums and type parameters, and… | ||
| From Clojure to Elixir: Leveraging Functional Programming for Scalable... | Wendy R | 28m |
Built a fabric inventory called Fabric Stash with a Clojure CRUD live version and an Elixir Phoenix (in development) remake, showing concrete tradeoffs… | ||
| Aeon — An AI-native programming language | Alcides Fonseca | 37m |
Aeon is an experimental language that synthesizes code using LLMs, genetic programming and SMT solvers and then verifies results with Liquid Types; an… | ||
| Total Functions for Automated Reasoning:Building Terminating Theorem Provers | Alex Gryzlov | 41m |
Builds terminating automated-reasoning cores in Agda and proves they halt by design, using Agda combinators and a boxed well‑founded fixed point to enforce… | ||
| Accidental Functional Programming in Rust | Dr. Caroline Morton | 38m |
An open-source Rust library called Codeless Tools validates and standardizes clinical code lists at load time, returning a typed Result as value or a specific… | ||
| When magic meets multicore - OCaml and its elegant era of parallelism | Carine M., Sonja H. | 40m |
Merlin's type-checker is offloaded to a background domain using OCaml 5 domains and effect handlers, implementing early typing return, cancellation, and… | ||
| From Exception Hell to Typed Bliss: Real-World Error Handling with Kotlin and Arrow | Jordi Pradel | 32m |
Team migrates exception-heavy Kotlin code to Arrow using Arrow's Raise DSL and Either for months, keeping direct-style control flow while gaining compile-time… | ||
| The Mastermind behind Refinement Types | Jorge Mayoral, Juanjo Madrigal | 35m |
Example: a sublist function needs index constraints like 0 <= i < j <= length and the compiler should prove those at compile time. SMT solvers follow a CDCL(T)… | ||
| Sketching streams with aquascape | Zainab Ali | 38m |
Explains a concrete stage model for FS2 streams that turns operator execution into a sequence of pull/output/done instructions, shows how those instructions… | ||
| Declarative UIs in a functional language | Damian Soriano | 35m |
An in-house functional language runtime evolves from a 2010 widget API to profunctor view nodes and custom handlers, cutting a text-change render from 6.0s to… | ||
| Pick a (Effect) Lane: A comparison of direct-style Scala vs effect systems | Jayanth Manklu | 31m |
Compares SoftwareMill Ox (direct-style on Project Loom virtual threads) with Cats-Effect IO by showing a 12-hour tonkatsu-broth and 3-hour chashu… | ||
| Prompting Safely: Building Secure LLM Prompts with a Scala DSL | Ignacio Gallego, Isaias B. | 36m |
Scala DSL that composes prompts via a typelevel interpolator and contravariant templates, implemented in about 300 lines, built over three months and flagged… | ||
| Starship Enterprise: Functional Programming at Huge Companies | Jack Higgs | 31m |
JPMorganChase runs a production Scala codebase that converts diverse ASTs (Smithy, GraphQL, UML, proprietary tools) into a single metamodel so a metadata… | ||
| Does FP still matter in the era of AI? | Raúl Raja Martínez, Jack Higgs, Isaias Bartelborth, Anurag Mendhekar | 32m |
Panel argues functional programming stays relevant because it yields proofs of correctness and language designs that eliminate the null problem, which AI… | ||
| Aeon — An AI-native programming language | Alcides Fonseca | 37m |
Aeon is an AI-native language that synthesizes code by combining LLMs + SMT + genetic programming and then verifies results with liquid types (SMT-backed… | ||
| From Functions to Inlinable Effects in Kotlin | Michail Zarečenskij | 27m |
Kotlin uses the inline modifier to make higher-order functions accept suspend and other effectful lambdas by inlining their bodies at call sites so… | ||
| The Margareth Hamilton Project | Jorge Galindo | 15m |
Nonprofit coding school in Cádiz runs classes for 6–12 year olds inside public schools, funded privately so it avoids local bureaucracy and covers costs for… | ||
| From Lambda to LLMs: AI Coding and the Future of Programming | Anurag Mendhekar | 43m |
Adoption jumps from 72% to 82% in weeks and 25% of new code is written by AI today; tools improve weekly and already cut equivalent engineering cost from… | ||
| nothing matches | ||