LambdaConf 2019
2019-06-05..2019-06-07
Boulder, United States
[LambdaConf 2015, LambdaConf 2017, LambdaConf 2018, LambdaConf 2019, LambdaConf 2020 Global Edition, LambdaConf 2024, LambdaConf 2025]
as the organisers put it
LambdaConf is the world's premier annual conference on commercial functional programming
| title | author | length |
|---|---|---|
| Isomorphic Reasoning: Counting with Types Part 1 | Emily Pillmore, Alexander Konovalov | 01h 39m |
Claim: parametric polymorphism gives a hidden type arithmetic that lets one compute exact inhabitant counts (e.g. ∀a. a→a is unique, function types count as… | ||
| Category Theory as a Tool for Thought | Daniel Beskin | 38m |
Argues that category theory yields concrete programmatic payoff by defining types and abstractions via relationships and then applying mechanical transforms… | ||
| Isomorphic Reasoning: Counting with Types Part 2 | Emily Pillmore, Alexander Konovalov | 02h 28m |
This is a 3 video talk; Please see:
Part 1: https://youtu.be/ApHFidwNypE
Part 3: https://youtu.be/kKZTd7D33KY
*We are aware of the sound issue for parts 2 and… | ||
| ETA lang a Journey from Haskell via STG and Bytecode to Assembly Part 1 | Jarosław Ratajski | 01h 39m |
ETA-lang compiles GHC-compatible Haskell to JVM bytecode so teams can run almost any GHC project on the JVM, with GHC-based Haskell on JVM as the core claim… | ||
| Isomorphic Reasoning: Counting with Types Part 3 | Emily Pillmore, Alexander Konovalov | 01h 52m |
This is a 3 video talk; Please see:
Part 1: https://youtu.be/ApHFidwNypE
Part 2: https://youtu.be/UScWv37aJhY
*We are aware of the sound issue for parts 2 and… | ||
| ETA lang a Journey from Haskell via STG and Bytecode to Assembly Part 2 | Jarosław Ratajski | 02h 06m |
Part 2 shows concrete results not promises: live Haskell–JVM interop (JavaFX example, stable pointers passing Haskell state to Java), measurements with a JMH… | ||
| ETA lang a Journey from Haskell via STG and Bytecode to Assembly Part 3 | Jarosław Ratajski | 01h 54m |
ETA compiles Haskell to STG then to JVM bytecode, demonstrates tail-call elimination working on the JVM, and measures performance with JMH benchmarks and… | ||
| A Categorical View of Adjunctions, Free Constructions, and Profunctor Optics | Emily Pillmore | 52m |
Adjunctions become the practical tool for deriving universal properties and free constructions (lists, free monoids, free groups) by exhibiting explicit… | ||
| Real World ZIO | Wiem Zine Elabidine | 31m |
Builds a concurrent, lock‑free elevator controller for H&A Hotel using ZIO and shows it actually works in simulation: n elevators, infinite pickup queue, step… | ||
| Why Writing Blockchain Applications is Hard, and How FP Can Help | François René Rideau | 48m |
Claim: a small domain-specific language compiles abstract specs down with cascading proofs so a 20–50 line spec avoids the 2,000 lines of hand‑written code the… | ||
| Building Distributed Applications in OCaml | François René Rideau | 51m |
OCaml code for real blockchain software uses explicit techniques not handwaving: content-addressed storage with digests for persistent DAGs, ppx-derived… | ||
| Calculating Intuitionistic Logic in Scala | Vlad Patryshev | 56m |
A working Scala library takes a finite category, builds the topos of diagrams (presheaves) over it, and computes Ω (subobject classifier) by enumerating… | ||
| Using GADTs to create a “Full Stack”, Runtime Gen. Scaffolding Lib in Scala | Travis Stevens | 41m |
Claims a concrete library called Bones library that uses GADTs + interpreters to generate HTTP routes, DB schema, Swagger docs, React clients and… | ||
| The Reason for ReasonML | Tianyu Pu | 37m |
Claim: Reason is a syntax layer over OCaml that compiles to readable JavaScript and fits into existing JS codebases. Evidence: BuckleScript (bsb) produces a… | ||
| Boolean Blindness Explained for Beginners in Haskell | Stephen Pimentel | 39m |
Argues that Booleans are an information-poor type and shows concrete fixes in Haskell: replace Boolean flags with pattern matching, custom ADTs or Maybe/Either… | ||
| Up to Your Elbows in GHC | Simon Hafner | 37m |
Proposal claims GHC can disable top-level record selectors so duplicate record fields stop polluting the VAR namespace. Implementation touches the renamer: add… | ||
| Records in Haskell Past, Present, and Future | Simon Hafner | 45m |
History of Haskell records, current hacks and concrete proposals: shows which GHC extensions solve what, demonstrates duplicate record fields quirks… | ||
| ReasonML Predictable Frontend Programming | Seif Ghezala | 57m |
Compares ReasonML, JavaScript and TypeScript by showing concrete behaviors: type inference that deduces int usage from +, option/pattern matching that forces… | ||
| Using Dependent Types in Mathematical Optimization Algorithms | Ryan Orendorff | 50m |
Uses dependent types in Haskell to encode matrix and vector shapes so linear-algebra calls are type-checked, implements convex optimization (proximal /… | ||
| Pretty Parsing | Ryan Delucchi, Sergei Shabanau | 44m |
Claims a single, purely functional implementation that parses and pretty-prints via invertible parsers and ships as scalaz-parsers, using partial isomorphisms… | ||
| Write You Some Proofs for Great Good | Robert Peszek | 56m |
Claim: writing machine-checkable proofs gets the compiler to accept precise types. Uses Haskell extensions GADTs and DataKinds, implements examples like Vect… | ||
| Refactoring a Net Database Connection into a Monadic Interface | Oren Rozen | 41m |
Refactors a legacy imperative .NET DB layer into a composable monadic interface, publishing the code at DBMonad and targeting both SQL and SAP HANA… | ||
| Automate More Code With Scalameta | Devon Stewart | 51m |
Live coding shows scalameta as a concrete AST tool: quasiquotes unpacking and repacking of defs, params and modifiers, structural pattern matches on case… | ||
| GADTs and You; Writing Safer Code Using GADTs | Nathan Holland | 35m |
Concrete claims and runnable patterns: using OCaml with GADTs to encode Peano numbers and length-indexed vectors, build typed heterogeneous lists, and make… | ||
| The CDelta Cryptocurrency Platform | Michael Stay | 42m |
The system claims a new Casanova consensus that runs as a bonded proof-of-stake-and-bandwidth network with one‑megabyte blocks every minute, ~83 tps per… | ||
| Free vs Tagless Final: What, Why, When? | Markus Hauck | 49m |
Compares concrete encodings by building a small Scala DSL with integer and string literals, addition, concatenation and string→int conversion, then implements… | ||
| Whirlwind Tour of the Scala Functional Programming Ecosystem | Mark Moore | 47m |
Builds a Twilio-backed SMS service that mirrors iOFFICE production and shows the actual decisions: abstracting effects as an F, implementing business logic… | ||
| An Independent History of Implicit Language Application | Marco Borst | 26m |
The talk shows how recursion and recursive data structures can be encoded at the type level in Scala by using a type-level fixed point and an ifix/list-like… | ||
| Total Smart Contracts in Pact: Model-Verified Interfaces and Governance | Linda Ortega | 42m |
Pact is a deliberately total, Turing‑incomplete contract language that puts source code on chain, adds an interactive REPL for local pact simulations, and… | ||
| What FP Can Learn From Formal Languages: Towards a Leaner Syntax | Lander Lopez | 01h 04m |
Argues that much syntactic overhead is accidental and shows concrete experiments: code in Haskell and Scala, property-based testing and example generation… | ||
| A Practical Introduction to Eff in Haskell | Keagan McClelland | 49m |
Builds a small Yesod/Persistent app and wires two Eff effects with two interpreters each so business logic stays pure while implementations vary. Uses… | ||
| The Tricks of Game Programming in a Pure Functional Language | Jordy Moos | 43m |
A recreation of Boulder Dash in Elm is used as a tiny game engine to run cellular automata and to solve Advent of Code 2018 day 15. The implementation uses a… | ||
| Back to Front and Beyond | Jim Duey | 45m |
A new Lisp-like language compiles to C/LLVM, implements reference counting GC with tail-call optimization, immutable collections with transient-style in-place… | ||
| Functional Electromagnetism | James Earl Douglas | 49m |
Uses GNU Radio, a HackRF transmitter and an RTL‑SDR receiver to show functional patterns in DSP by actually building a Morse‑code flowgraph that transmits on… | ||
| MiniLaTeX: Parse LaTeX to HTML | James Carlson | 50m |
MiniLaTeX parses a substantial subset of LaTeX to HTML in real time by splitting math to MathJax and text to an AST (a 12-line algebraic type) then rendering… | ||
| Expressing Types as Values with Scalaz-Schema | Dominic Egger | 37m |
Scalaz-Schema presents a concrete Schema datatype that expresses ADTs as values and derives encoders like a JSON serializer without relying on compiler-driven… | ||
| Using Semantic Types to Squash Bugs | Dillon Kearns | 48m |
Elm code converts a bug about masked social security numbers into a compiler-guided refactor: primitives become a wrapper type SSNInput, JSON decoders and… | ||
| Level Up! Game Development With PureScript Native | David Lettier | 45m |
Claim: PureScript Native compiles PureScript to C++ so real 3D games can be written with PureScript logic and a C++ engine. Implementation details: use the… | ||
| Compositional, Expressive, Performant Database Queries: Choose 3 | Dave Nicponski | 48m |
Claims use Slick as a typesafe embedded DSL and a new library called Sloppy to build query transformers that compose into a single SQL query so you avoid N+1… | ||
| Haskell in Production: Adventures in Blockchain Building | Colin Woodbury | 01h 11m |
Haskell runs as the production language at Kadena powering Chainweb (public testnet v1) and Pact tooling; the stack uses Cabal 2.2 with default.nix, NixOS… | ||
| Genetics in PureScript Without Knowing Genetics | Christian Fischer | 42m |
Built a genetics browser in PureScript that maps mouse genome (19 autosomes, 60–200M base pairs each) onto an HTML5 canvas, links points to external resources… | ||
| Pinafore: Strongly Typed Information Representation | Ashley Yakeley | 50m |
A strongly typed functional language for personal data, implemented in Haskell, claims decidable subtyping by using Algebraic Subtyping (Stephen Dolan) and… | ||
| Type Providers: Making Data First Class | André M van Meulebrouck | 50m |
F# type providers connect to a live CSV/XML/DB, run IDE-time schema generation to produce typed APIs and Intellisense, and surface errors as squiggles before… | ||
| Rust's Borrow Checker Proven Correct! | Adam McCullough | 50m |
Claim: borrow checker proven correct for a formal subset of Rust — lifetimes, ownership and aliasing get modeled and the properties are machine-checked… | ||
| Enter the L∞p | Valentin Kasas | 42m |
Conference data: a 500‑respondent Twitter poll shows the top fears, a CFP returns 200+ proposals but only seven targeting beginners and just five proposals… | ||
| A Helicopter Tour of Purely Functional Data Structures | Tyler Prete | 48m |
Walks through concrete implementations and tradeoffs: Scala & Haskell implementations of lists, lazy streams, two‑stack queues, 2‑3 trees and finger trees… | ||
| Go Fully Functional and Take Your Legacy Code with You! | Tuan Nhi Le | 52m |
Promised outcome: a mechanical four‑step migration: plan test build refactor applied to a concrete example (a qualification pipeline that reads CSVs, computes… | ||
| Zippers; The Theory and the Application | Tony Morris | 50m |
Claims that every zipper is a comonad and that a zipper is the derivative of a data structure (McBride et al) get demonstrated with concrete encodings: a list… | ||
| Trees that Grow | Tony Morris | 52m |
Claims that Trees That Grow (Najd, Shayan and Peyton‑Jones, Simon, 2016) let syntax trees extend without breaking callers, implemented with type families… | ||
| Sane System Management with NixOS - I Do Declare! | Tim Steinbach | 55m |
Nix and NixOS promise a single declarative file that reproduces a whole system: kernel options, services, user packages and dotfiles, so a new machine boots to… | ||
| Types as Program Specifications: A Intro to Type-Level Programming in Haskell | Thomas Dietert | 01h 57m |
Argues that types serve as executable specifications and shows how to embed invariants in GHC using language extensions: GADTs, DataKinds, TypeFamilies (plus… | ||
| Running Highly Scalable Tracing, Logging, Monitoring & Metric System in Production | Tapasweni Pathak | 30m |
Claims a production setup that actually serves 252 million subscribers and handled 37 million new users in nine months while running its own data centers. It… | ||
| Building Your Perfect World With Concurrent Combinators in F#! | Riccardo Terrell | 53m |
Concrete F# code wins: a library of reusable concurrent combinators is implemented (async and Task variants), including async/applicative combinators, an… | ||
| You got FP in my Enterprise! | Phillip Carter | 01h 01m |
F# is used to implement F# and the tools are packaged as a compiler binary for .NET Core, source builds, .NET Framework, and Mono — compiler packaged four… | ||
| Constructing a DSL for Composable Reports in Haskell | Nikolai Kudasov | 35m |
Claims a practical solution: an type-safe DSL in Haskell that generates Excel via the xlsx library, arrived at in a few days and used in production. It models… | ||
| Augmenting Reality in Haskell | Nikolai Kudasov | 01h 33m |
Claims a type-safe AR app in Haskell built in ~two hours, implemented with GHCJS + A-Frame, a Docker dev image, WebSocket server for multiplayer sync, and… | ||
| Environmental Dependencies as Coeffects | Nihil Shah | 40m |
Claim: environmental dependencies become coeffects modeled as indexed comonads and encoded with type-level monoids. Implementation: a Haskell prototype uses… | ||
| Why You Should Use Software Transactional Memory | Michael Snoyman | 01h 33m |
Argues that Haskell’s STM actually reduces concurrency footguns by giving concrete semantics: use atomically with TVars and newTVarIO to avoid nested… | ||
| Outer Product as an Introduction to APL and a Pretty Cool Thing in General | Marshall Lochbaum | 02h 25m |
Shows the actual claim: the outer product (APL’s dot-dot operator) applies any function to every pair of elements and doesn’t just mean multiplication… | ||
| An Introduction to Natural Deduction | Lyle Kopnicky | 01h 44m |
Natural deduction gets taught by walking through exact rules, writing and collapsing concrete proofs, then encoding them as programs so you can check they… | ||
| Fun with Lattices | Jose Cardona | 01h 57m |
Explains that some lattice problems have average-case hardness equal to worst-case hardness, focuses on the shortest vector problem and the closest-vector… | ||
| A Server is Just a Function An Introduction to http4s | Jakub Kozłowski | 45m |
http4s presents concrete choices: a functional HTTP library for Scala http4s built on cats-effect and fs2 that makes requests, responses and bodies the same… | ||
| Overlapping and Undecidable and Incoherent, Oh My! | Jake Keuhlen | 50m |
GHC’s typeclass extensions are listed and demonstrated with real code: 16 extensions (six class, ten instance) with concrete examples like the String vs [Char]… | ||
| UI as Warm as a Baked Potato | Isaac Shapira | 59m |
Small Haskell UI core plus plugins that compiles to multiple back ends via jsaddle and ghcjs and can run server‑side over WebSocket or as client JS. HTML is a… | ||
| Pluggable Stackable API Implementations | Harold Carr | 52m |
Builds a composable API that stacks a cache + bloom + base map behind the same Data.Map-like interface, shows concrete Haskell code using type families, Except… | ||
| Elm GraphQL Workshop | Dillon Kearns | 57m |
Workshop demonstrates that elm-graphql introspects a GraphQL schema, generates Elm code for the entire API, and produces compiler errors for invalid queries… | ||
| Principled HTTP Server Generation with Guardrail | Devon Stewart | 54m |
Generates server and client code from OpenAPI/Swagger specs (v2 and v3), with SBT, Maven and CLI runners that run during compile so a changed spec fails to… | ||
| Bring FP to Work | Charles Rumley | 53m |
Slides claim that technical demos alone fail: after 3 group meetings, 5 blackboard sessions and a proof of concept app adoption remains slow, so persuasion… | ||
| Batching Monadic Requests with Free Interpreters | Cary Robbins | 50m |
Builds a runtime that inspects running monadic programs, extracts their next free applicative requests, and batches them against the Google Calendar batch API… | ||
| Maintaining Data Integrity When Blockchains Fork | Basil Ahmad | 44m |
Conseil stores chain data in Postgres and Lorre crawls nodes (currently Tezos) to populate it; the algorithm never deletes blocks but marks them in an… | ||
| Monoids on Steroids: A Brief History of FP | André M van Meulebrouck | 28m |
A hobby project called plotting and scheming implements a fractal-and-plotter suite (complex plane, L‑system, vector, polar, cartesian) written in F# with an… | ||
| Recursion Schemes, Algebras, Finally Tagless, Data Types | Alexander Konovalov | 01h 35m |
Claims a single unifying fact: many FP encodings are isomorphic and mechanically transformable. Demonstrates the isomorphism between fold and data… | ||
| Practical Observable Sharing | Alexander Konovalov | 01h 44m |
Solves two concrete problems: generate an EBNF and decide nullability from finally‑tagless applicative parsers, and simplify a logical‑circuit DSL and emit a… | ||
| Program Obesity: A Code Health Epidemic | Aaron W Hsu | 01h 01m |
Claim: pervasive pointer-based ASTs cause huge bloat and cache-miss performance. Implements the same compiler twice — a nanapass-style Racket version that… | ||
| Specifying Distributed Systems with TLA+ Workshop | Pawel Szulc | 01h 54m |
Workshop teaches TLA+ from the ground up, uses TLA+ Toolbox and the TLC model checker to write formal specs of distributed algorithms (examples: Paxos and Two… | ||
| Asynchronous and Concurrent Programming in Scala Part 1 | John DeGoes | 01h 28m |
Three-part, hands-on workshop that teaches ZIO by building and running real code: concrete exercises implement a toy console effect with map/flatMap, write… | ||
| Asynchronous and Concurrent Programming in Scala Part 3 | John DeGoes | 01h 12m |
Workshop shows using ZIO to build concrete asynchronous, concurrent code: modules with ZIO environment that get provide/provideSome wiring, helper APIs that… | ||
| Asynchronous and Concurrent Programming in Scala Part 2 | John DeGoes | 01h 53m |
Workshop-length, hands-on deep dive into ZIO: how to lift callback APIs (example: Java scheduled executor wrapped with effectAsync and cancel via… | ||
| nothing matches | ||