ICFP 2023
as the organisers put it
The 28th ACM SIGPLAN International Conference on Functional Programming will be in Seattle, WA, USA on 4–9 September 2023. ICFP’s main research paper track will be on September 5-7 (Tuesday-Thursday), with workshops, tutorials, and other events on September 4 and 8-9 (Monday, and Friday-Saturday). Registration is now open! To locate the rooms, you can click here to view the floor plans provided by The Westin Seattle. The ICFP 2023 Discord instance is here.
| title | author | length |
|---|---|---|
| Welcome | Nikhil Swamy | 06m |
ICFP 2023 opens in Seattle with an acknowledgement of the traditional Salish lands and a QR code linking to an article about local Indigenous issues. The… | ||
| Programming for the planet | Anil Madhavapeddy | 01h 11m |
A reproducible pipeline built in OCaml (the urrent DSL) composes satellite inputs, Dockerized science scripts and Python wrappers into traceable dataflows… | ||
| As low-level as possible, but no lower | Andreas Rossberg | 01h 06m |
WebAssembly claims a rigorous, fully formalized spec with multiple mechanizations and a reference interpreter; a new spec-DSL now generates the formal rules… | ||
| Is Sized Typing for Coq Practical? | Jonathan Chan, Yufeng Li, William J. Bowman | 25m |
Implementation of CIC^ sized type theory inside a Coq 8.12 kernel fork produces a full size-inference pipeline that emits difference constraints solved by… | ||
| A General Fine-Grained Reduction Theory for Effect Handlers | Filip Sieczkowski, Mateusz Pyzik, Dariusz Biernacki | 27m |
Presents a fine-grained reduction semantics for deep effect handlers that gives confluence and standardisation proofs (adapting Takahashi/McKinna techniques)… | ||
| Dependently-Typed Programming with Logical Equality Reflection | Yiyun Liu, Stephanie Weirich | 31m |
System DE is an explicitly typed core calculus that separates a terminating logical fragment from a potentially diverging programmatic fragment using modes for… | ||
| Modular Models of Monoids with Operations | Zhixuan Yang, Nicolas Wu | 28m |
A categorical framework presents equational theories of monoids equipped with arbitrary operations and shows an explicit monoid-theory correspondence: the… | ||
| A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized | Andreas Abel, Nils Anders Danielsson, Oskar Eriksson | 30m |
A graded dependent type theory is formalized in Agda (≈39,000 lines) with Π, weak/strong Σ, Nat, Empty, a universe, and a parameterized semiring‑like modality… | ||
| With or Without You: Programming with Effect Exclusion | Matthew Lutze, Magnus Madsen, Philipp Schuster, Jonathan Immanuel Brachthäuser | 27m |
A new Hindley‑Milner style type-and-effect system adds union, intersection and complement to express “any effects except these” and implements effect exclusion… | ||
| Special Delivery: Programming with Mailbox Types | Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, Phil Trinder | 26m |
Pat implements mailbox types that model each mailbox as a commutative regular expression and statically rule out protocol violations (double put, missing… | ||
| Combinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters | Sven Keidel, Sebastian Erdweg, Tobias Hombücher | 28m |
Library of 12 fixpoint combinators composes to control big‑step abstract interpreters: each combinator enforces one of three divergence fixes (cut off… | ||
| HasChor: Functional Choreographic Programming for All | Gan Shen, Shun Kashiwa, Lindsey Kuper | 30m |
HasChor is a Haskell library that encodes choreographies as a monad and compiles them to per-node programs via endpoint projection implemented with freer… | ||
| More Fixpoints! | Joachim Breitner | 30m |
Library implements lazy sets and lazy booleans by wrapping an imperative propagator network behind a pure API using unsafePerformIO, so recursive equations… | ||
| The Cogent and Dargent approach to facilitating verified software development | Christine Rizkallah | 01h 07m |
Cogent is a restricted functional language with a linear type system and a certifying compiler that emits C, getter/setter code and Isabelle/HOL refinement… | ||
| TypeScript: Static types for JavaScript | Anders Hejlsberg | 01h 11m |
Adds a static, erasable type layer to JavaScript that compiles back to plain JS, ships since October 2012, and now ranks in the top five languages on GitHub… | ||
| Student research contest talks | Daniel Hillerström, J. Garrett Morris | 32m |
Six five-minute student reports present concrete artifacts and results: a semantics for higher-order hardware descriptions with a normalization theorem and… | ||
| Programming contest report | Aymeric Fromherz | 17m |
ICFP 2023 programming contest optimizes musician placement on a rectangular stage with blocking by other musicians and pillars, attendees (500–3,000) having… | ||
| Reflecting on Random Generation | Harrison Goldstein, Samantha Frohlich, Meng Wang, Benjamin C. Pierce | 27m |
Presents reflective generators that combine free generators + partial monadic profunctors so a generator can run “backwards” to recover random choices that… | ||
| Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verifica... | Son Ho, Aymeric Fromherz, Jonathan Protzenko | 30m |
Implements a userland F metaprogram that performs whole-call-graph code specialization for Low and compiles to readable C, producing an extra compiler stage… | ||
| Etna: An Evaluation Platform for Property-Based Testing | Jessica Shi | 28m |
Etna is a multilanguage evaluation platform that runs property‑based testing experiments across Coq and Haskell, uses handcrafted mutants and mutation testing… | ||
| Higher-Order Property-Directed Reachability | Hiroyuki Katsura, Naoki Kobayashi, Ryosuke Sato | 28m |
Formalizes a higher-order extension of PDR that extends PDR to nu-HFL(Z) so transition systems can be described by higher-order recursive functions, implements… | ||
| Formal Specification and Testing for Reinforcement Learning | Mahsa Varshosaz, Mohsen Ghaffari, Einar Broch Johnsen, Andrzej Wąsowski | 29m |
Defines a declarative DSL called BDL domain-specific language that encodes TD backup diagrams, gives a denotational semantics, and generates executable specs… | ||
| Verifying Reliable Network Components in a Distributed Separation Logic with Dep... | Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, Lars Birkedal | 30m |
Claims a verified reliable client–server communication stack implemented in an OCaml-like language (about 300–400 lines of code) that runs over UDP and… | ||
| Timely Computation | Conal Elliott | 34m |
Defines a digital circuit as an analog circuit used in a disciplined way and formalizes that notion in Agda formalization, embedding discrete meanings into… | ||
| Embedding by Unembedding | Kazutaka Matsuda, Samantha Frohlich, Meng Wang, Nicolas Wu | 27m |
Presents a concrete recipe that turns a tagless‑final (HOAS) interface into de Bruijn terms via embedding by unembedding, exposing when HOAS fails and how to… | ||
| A well-known representation of monoids and its application to the function ‘vect... | Wouter Swierstra | 25m |
Shows how representing a monoid as endofunctions yields difference Naturals so monoidal laws hold definitionally, letting a tail-recursive accumulator for… | ||
| MacoCaml: Staging Composable and Compilable Macros | Ningning Xie, Leo White, Olivier Nicole, Jeremy Yallop | 32m |
MacoCaml implements compile‑time code generation inside the OCaml compiler, treating macros as compile-time bindings and using quotation/splice staging so… | ||
| Modal FRP for all: Functional reactive programming without space leaks in Haskel... | Patrick Bahr | 29m |
A modal FRP language Ratus is implemented as a Haskell library plus a GHC plugin that enforces stricter typing: a later modality for time-shifted values and a… | ||
| Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Dat... | Alex Hubers, J. Garrett Morris | 30m |
Claims a practical calculus, System Rω, that extends Fω with row types and higher‑order rows to express generic operations over unknown labels; implements… | ||
| Asynchronous Modal FRP | Patrick Bahr, Rasmus Ejlers Møgelberg | 30m |
Async RaTT is a new modal language that compiles complete programs to machines consuming asynchronous input channels and emitting outputs, using an exist-later… | ||
| Typing Records, Maps, and Structs | Giuseppe Castagna | 28m |
Proposes a type theory that unifies struct-style and map-style records with union, intersection, and negation types, models record values as quasi-constant… | ||
| Awards | 18m | |
The ceremony awards the most influential paper of ICFP 2013 — Handlers in Action (Ohad Kamar, Sam Linley, Nicholas Ruri) with a $1,000 prize, citing its first… | ||
| JFP at ICFP | Gabriele Keller | 01m |
Announcement says JFP runs a JFP to ICFP track started in 2020 that lets original JFP articles — explicitly not extended versions of conference papers — be… | ||
| Diversity, equality, and inclusion at ICFP | Daan Leijen | 06m |
ICFP creates a new coordinated diversity effort with a standing committee, a long-term mentoring program that currently matches about 300 mentees and 200… | ||
| PC Chair's report | Sam Lindley | 14m |
ICFP receives 90 submissions this year, splits into 17 PC and 73 non‑PC papers, and accepts 33 papers (37% overall) with 10 unconditional and 23 conditional… | ||
| ICFP 2024 announcement | Marco Gaboardi | 05m |
ICFP 2024 will be in Milan, Italy, with the main venue a conference center (not a hotel) offering a full-floor program space and basement rooms for workshops… | ||
| The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programmi... | Lennart Augustsson, Joachim Breitner, Koen Claessen, Ranjit Jhala, Simon Peyton Jones, Olin Shivers, Guy L. Steele Jr., Tim Sweeney | 30m |
A new core calculus (VC) gives a small-step rewrite semantics for a deterministic functional logic language and implements unification and logical variables as… | ||
| Explicit Refinement Types | Jad Elkhaleq Ghalayini, Neel Krishnaswami | 29m |
System called λert implements refinement types that require explicit, checkable proofs instead of SMT solving, supporting quantifiers and induction; key claim… | ||
| FP²: Fully in-Place Functional Programming | Anton Lorenzen, Daan Leijen, Wouter Swierstra | 30m |
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… | ||
| Flexible Instruction-Set Semantics via Abstract Monads | Thomas Bourgeat, Ian J Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andy Wright, Adam Chlipala | 36m |
Claims a single Haskell-based core semantics, parameterized by a Risk5Machine type class over monads, supports testing, interactive proof, model checking and… | ||
| LURK: Lambda, the Ultimate Recursive Knowledge | Nada Amin, John Burnham, François Garillot, Rosario Gennaro, Chhi’mèd Künzang, Daniel Rogozin, Cameron Wong | 31m |
Lurk is a LISP-based language plus a universal interpreter circuit that lets programs be supplied as data so zk proofs verify runs instead of flattened… | ||
| How to Evaluate Blame for Gradual Types, Part 2 | Lukas Lazarek, Ben Greenman, Matthias Felleisen, Christos Dimoulas | 30m |
Empirical study instruments a rational-programmer procedure, mutates GTB benchmark programs, and runs three TyRet/Racket semantics (eraser, transient, natural)… | ||
| Intrinsically Typed Sessions with Callbacks | Peter Thiemann | 32m |
Claims a practical embedding of session types that avoids host-language linear types by representing protocols as an indexed command data structure of… | ||
| What Happens When Students Switch (Functional) Languages | Kuang-Chen Lu, Shriram Krishnamurthi, Kathi Fisler, Ethel Tshukudu | 29m |
Two course studies compare Racket, Pyret, and Python to measure transfer, using homework and exams rather than lab tasks. 87% of students report no Pyret… | ||
| Dependent Session Protocols in Separation Logic from First Principles | Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers | 28m |
Three-layer design builds session protocols from mutable references: one-shot channels, then functional session channels, then imperative endpoints; specs use… | ||
| Calculating Compilers for Concurrency | Patrick Bahr, Graham Hutton | 30m |
Paper shows a method that turns a high‑level choice trees semantics into a correct-by-construction compiler by adding a codensity construction, yielding… | ||
| Read/write factorizable programs | Siddharth Bhaskar, Jakob Grue Simonsen | 25m |
Claim: read/write factorization yields a clean syntactic class of programs over strings that exactly captures FP when recursion is non‑nested and FL for tail… | ||
| Trustworthy Runtime Verification via Bisimulation | Ryan G. Scott, Mike Dodds, Ivan Perez, Alwyn E. Goodloe, Robert Dockins | 30m |
CopilotVerifier automatically proves that a Copilot Haskell stream monitor and its compiled C (Clang→LLVM) output produce equivalent observable behavior by… | ||
| Bit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebr... | Thaïs Baudon, Gabriel Radanne, Laure Gonnord | 32m |
A compiler and DSL called ribbit accepts a high‑level ADT plus a separate memory type, emits LLVM IR, and proves pattern‑match compilation correct; it… | ||
| Fireside chat | Amal Ahmed, Felix Klock, Greg Morrisett | 01h 08m |
History of Rust traces concrete choices: adoption of explicit lifetimes evolving into non-lexical lifetimes to handle lookup/mutation patterns, planning… | ||
| Ask me anything | Tim Sweeney | 42m |
A new language called Verse implements functional logic with an effect system and a strong type system that scales toward proofs; it uses transactional memory… | ||
| nothing matches | ||