Wouter Swierstra
where else to find them
no profile links on file
what they talk about
where they keep going back
- ICFP4 editions2020–2025
all 4 in the filters
on a stage with
all 6 in the filters
who talks about the same things
- Anton Lorenzen8 talks
- Daan Leijen16 talks
- Sam Lindley27 talks
- Steve Zdancewic19 talks
- Deepak Garg18 talks
- Michel Steuwer17 talks
| title | conference | date |
|---|---|---|
| Hole Refinements for Polymorphic Type-and-Example Driven Synthesis | PEPM 2026 | 2026-01-11 |
Toolchain combines a parametricity-aware feasibility reasoner and a tactic-driven synthesizer: Taxi computes polymorphic input–output normal forms and… | ||
| First-Order Laziness | ICFP 2025 | 2025-10-12 |
Proposes replacing thunk closures with lazy constructors that are defunctionalized first‑order values, implemented in Koka; evaluation happens on pattern match… | ||
| The Functional Essence of Imperative Binary Search Trees | PLDI 2024 | 2024-06-24 |
Functional algorithms introduce a new first-class constructor context primitive and use Koka’s reuse-aware reference counting to implement tail-call, in-place… | ||
| A well-known representation of monoids and its application to the function ‘vect... | ICFP 2023 | 2023-09-04 |
Shows how representing a monoid as endofunctions yields difference Naturals so monoidal laws hold definitionally, letting a tail-recursive accumulator for… | ||
| FP²: Fully in-Place Functional Programming | ICFP 2023 | 2023-09-04 |
Formal system proves a large class of pure functions can run with no allocation or deallocation and constant stack space when their arguments are unique, and… | ||
| How to trust a verified program? | Unsound 2022 | 2022-12-06 |
Proof assistants like Agda, Coq and Lean still permit real failures: a universe overflow caused by 63-bit integer wrap lets Agda accept falsity; a… | ||
| A Completely Unique Account of Enumeration | ICFP 2022 | 2022-09-11 |
A datatype generic enumerator is built that works for all regular types and indexed families and is proven complete and unique: every inhabitant appears… | ||
| Heterogeneous binary random-access lists | ICFP 2020 | 2020-08-23 |
Implements heterogeneous binary random-access lists in Agda with the same HList API: nil, cons (via a cons-tree primitive) and lookup that are total and… | ||
| nothing matches | ||