ICFP 2022
| title | author | length |
|---|---|---|
| Deep Programmability: A New Lens on Networking | Nate Foster | 47m |
Argues that networks are becoming deeply programmable end-to-end and shows concrete tools: a high-level DSL NetKAT with formal semantics and a compiler that… | ||
| Multi Types and Reasonable Space | Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni | 18m |
Claims a concrete machine, Space KAM, is a reasonable space cost model for the lambda calculus (linear overhead vs. Turing/RAM) and handles logarithmic-space… | ||
| Random Testing of a Higher-Order Blockchain Language (Experience Report) | Tram Hoang, Anton Trunov, Leonidas Lampropoulos, Ilya Sergey | 18m |
Integrates QuickChick on Coq with an OCaml implementation of a higher‑order smart‑contract language and builds a semantic harness by turning the monadic… | ||
| Entanglement Detection with Near-Zero Cost | Sam Westrick, Jatin Arora, Umut A. Acar | 16m |
Presents a runtime entanglement detector implemented in the Maple (MPL) compiler that builds a computation graph and uses SP-order maintenance to check only… | ||
| Analyzing Binding Extent in 3CPS | Benjamin Quiring, John Reppy, Olin Shivers | 14m |
3CPS implements a 3CPS factored CPS IR and an abstract‑interpretation analysis that classifies each variable as register/stack/heap extents, mapping extents to… | ||
| Safe Couplings: Coupled Refinement Types | Elizaveta Vasilenko, Niki Vazou, Gilles Barthe | 15m |
Enhances refinement types with a coupling-based connective that captures relational properties like expected sensitivity and proves that output-distance is… | ||
| "do" Unchained: Embracing Local Imperativity in a Purely Functional Langua... | Sebastian Ullrich, Leonardo de Moura | 15m |
Adds local mutation, early return and iteration to do notation and provides formal translation rules that compile them to pure code while preserving semantics… | ||
| Program Adverbs and Tlon Embeddings | Yao Li, Stephanie Weirich | 14m |
Proposes program adverbs as reified functor classes (applicative/selective/monad) that embed effects LiftA2 and Embed constructors to capture static vs dynamic… | ||
| Later Credits: Resourceful Reasoning for the Later Modality | Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer | 15m |
Introduces later credits as an ownable resource in Iris that splits stepping into a credit-generation rule and a credit-spending rule, letting proofs prepay… | ||
| Datatype-Generic Programming Meets Elaborator Reflection | Hsiang-Shang Ko, Liang-Ting Chen, Tzu-Chi Lin | 16m |
Claims a practical framework that uses elaborator reflection in Agda to turn datatype-generic descriptions into real, native datatypes and functions… | ||
| Verified Symbolic Execution with Kripke Specification Monads… | Steven Keuchel, Sander Huyghebaert, Georgy Lukyanov, Dominique Devriese | 20m |
Presents a verified symbolic executor implemented as a Kripke-indexed symbolic specification monad that manipulates deeply embedded assertions, proves… | ||
| Generating Circuits with Generators | Marek Materzok | 17m |
YieldFSM is a generator-based HDL that represents clock-level timing so designers get higher-level code with explicit cycles; the compiler (using… | ||
| Beyond Relooper: Recursive Translation of Unstructured Control Flow to Structu… | Norman Ramsey | 16m |
Translates arbitrary intraprocedural control-flow graphs into structured WebAssembly constructs and reduces the classic three-pass Peterson/Kasami/Tokura… | ||
| Programming Contest Report | 12m | |
ICFP contest runs 40 tasks with three spec stages (first 24h, second, third) and operators limited to point cut, line cuts, colour (RGBA) fills, merges and… | ||
| Fireside Chat with Arvind and Guy Steele | Arvind, Guy Steele | 55m |
Casual, wide‑ranging history that names concrete projects and lessons: early Scheme work and the "rabbit" compiler that rethinks actors vs lambdas; a real… | ||
| A Reasonably Gradual Type Theory | Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter | 16m |
Presents GRIP, an extension of CastCIC that is normalizing and a conservative extension of CIC, and that internalizes precision so graduality can be proven for… | ||
| Flexible Presentations of Graded Monads | Shin-ya Katsumata, Dylan McDermott, Tarmo Uustalu, Nicolas Wu | 15m |
Defines a flexibly graded presentation that permits operations whose arguments carry different grades and proves two concrete claims: every such presentation… | ||
| On Feller Continuity and Full Abstraction | Gilles Barthe, Raphalle Crubill, Ugo Dal Lago, Francesco Gavazzo | 20m |
Shows that in a call-by-value higher-order lambda calculus with sampling and only continuous real-valued primitives, Feller-continuity on the induced labelled… | ||
| Normalization for Fitch-Style Modal Calculi | Nachiappan Valliappan, Fabian Ruch, Carlos Tomé Cortiñas | 17m |
Claims a modular semantic normalization procedure for Fitch-style modal lambda calculi: it builds Normalization by Evaluation models from a single… | ||
| Aeneas: Rust Verification by Functional Translation | Son Ho, Jonathan Protzenko | 15m |
Aeneas translates a large, safe subset of Rust (no interior mutability or unsafe) into a pure lambda calculus so proofs avoid memory/address reasoning… | ||
| Practical Generic Programming over a Universe of Native Datatypes | Lucas Escot, Jesper Cockx | 16m |
Library for Agda implements a universe-of-descriptions approach and exposes regular Agda functions that specialize to native datatypes with a one-liner… | ||
| Staged Compilation with Two-Level Type Theory | András Kovács | 15m |
Shows that two-level type theory (2LTT) can serve as a foundation for staged compilation that supports full dependent types, provides a staging-by-evaluation… | ||
| Fusing Industry and Academia at GitHub (Experience Report) | Patrick Thomson, Rob Rix, Nicolas Wu, Tom Schrijvers | 27m |
GitHub describes building Semantic in Haskell to power code navigation and structural diffing across 9 languages, using tree-sitter grammars compiled to C for… | ||
| Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Fre... | Jules Jacobs, Stephanie Balzer, Robbert Krebbers | 14m |
A functional language MPGV extends GV with multiparty session types, first-class channel endpoints, dynamic spawning and a new redirect construct that enables… | ||
| Introduction and Elimination, Left and Right | Klaus Ostermann, David Binder, Ingo Skupin, Tim Süberkrüb, Paul Downen | 18m |
Claims that four rule choices—right/left introduction and elimination—yield four distinct program structures but are equally expressive through mechanical… | ||
| A Completely Unique Account of Enumeration | Cas van der Rest, Wouter Swierstra | 13m |
A datatype generic enumerator is built that works for all regular types and indexed families and is proven complete and unique: every inhabitant appears… | ||
| Modular Probabilistic Models via Algebraic Effects | Minh Nguyen, Roly Perera, Meng Wang, Nicolas Wu | 15m |
Claims a Haskell-embedded DSL that makes probabilistic models first-class and reusable by using algebraic effects so one model serves for simulation… | ||
| Reference Counting with Frame Limited Reuse | Anton Lorenzen, Daan Leijen | 16m |
Defines Perceus garbage-free refcounting that inserts precise increment/drop ops so objects free exactly when unreachable, adds a new drop-guided reuse… | ||
| Structural versus Pipeline Composition of… (Experience Report) | Elijah Rivera, Shriram Krishnamurthi | 14m |
Claim: students find structural composition easier than pipeline composition for list higher-order functions. Method: restrict to a small set of list HOFs… | ||
| Formal Reasoning about Layered Monadic Interpreters | Irene Yoon, Yannick Zakowski, Steve Zdancewic | 14m |
Extends the Coq interaction trees (ITrees) library to characterize a class of interpretable monads obtained by applying monad transformers to ITrees, gives… | ||
| Propositional Equality for Gradual Dependently Typed Programming | Joseph Eremondi, Ronald Garcia, Éric Tanter | 16m |
A gradual dependently-typed language is implemented that adds a propositional equality whose proofs carry witnesses (each proof pairs an equality with a term… | ||
| Linearly Qualified Types: Generic Inference for Capabilities and Uniqueness | Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, Richard A. Eisenberg | 16m |
Adds implicit linear constraints as qualified types and implements a constraint generation and inference algorithm that extends GHCs solver, desugaring the… | ||
| A Simple and Efficient Implementation of Strong Call by Need by an Abstract Ma… | Malgorzata Biernacka, Witold Charatonik, Tomasz Drab | 18m |
Claims a concrete abstract machine called RKNL that implements strong call-by-need by automatically transforming a higher-order evaluator (with memothunks)… | ||
| Searching Entangled Program Spaces | James Koppel, Zheng Guo, Edsko de Vries, Armando Solar-Lezama, Nadia Polikarpova | 12m |
Introduces equality-constrained tree automata to compactly represent program spaces where subterm choices are entangled, and implements extraction and lazy… | ||
| Conclusions and Awards | 33m | |
Session announces student competition winners (undergrad and grad named), SIGPLAN updates on finances and volunteer roles, and pushes institutions toward ACM… | ||
| Student Research Competition Final Presentations | Bernard Boey, Hilbert Chen, Yanjun Chen, Eric Zhao, Francis Rinaldi, Arthur Correnson, Nathan Corbyn, Denis Carnier | 33m |
Session collects six short student projects with concrete artifacts and techniques: HenBlocks: structured editing for Coq is a client‑side web app (GS‑Coq… | ||
| Automatically Deriving Control-Flow Graph Generators from Operational Semantics | James Koppel, Jackson Kearl, Armando Solar-Lezama | 16m |
An algorithm converts small-step operational semantics into an abstract machine, then uses abstract rewriting to synthesize both interpreted-mode and… | ||
| Retrofitting Concurrency – Lessons from the Engine Room | KC Sivaramakrishnan | 40m |
OCaml 5.0 brings native concurrency and parallelism and ships effect handlers as the language-level mechanism; the Multicore design uses per-domain minor heaps… | ||
| Monadic Compiler Calculation (Functional Pearl) | Patrick Bahr, Graham Hutton | 15m |
Derives a correct compiler from a correctness specification by calculating definitions during the proof, using the partiality monad to make divergence explicit… | ||
| nothing matches | ||