Search events for 'all'
Discussion: All for one and none for all
miniKanren 2026 When: Mon 24 Aug 2026 14:30 - 14:45
… …
All for one and none forall: Compiling polymorphic relations without monomorphization
miniKanren 2026 When: Mon 24 Aug 2026 14:00 - 14:30 People: Dmitri Volkov, Chung-chieh Shan, Yafei Yang
… …
Writing Makes the Researcher: The First Audience Is You
PLMW @ ICFP 2026 When: Mon 24 Aug 2026 14:00 - 14:45 People: Benjamin Delaware
… advisor (to learn to ask your own). In all three cases, the writing is targeted …
Reduction Semantics and How to Read Them
PLMW @ ICFP 2026 When: Mon 24 Aug 2026 14:45 - 15:30 People: Robert Bruce Findler
… , exceptions and continuations) are all just a matter of using the basic tools …
An Array-Oriented Language via the Design Recipe
Scheme 2026 When: Sat 29 Aug 2026 14:30 - 15:00 People: Martin Scheele, Stephen Chang
… . Best of all, functions dealing with this kind of data can be incorporated …
A Call-by-push-value Scheme
Scheme 2026 When: Sat 29 Aug 2026 11:00 - 11:30 People: Max S. New
… Scheme is known for its minimalism: what would be core language features in other languages are instead implemented as macros over a small core. In its most Spartan formulation all compound data arises from the humble cons. Inspired …
A Mechanised Semantics of Erlang’s References
Erlang 2026 When: Fri 28 Aug 2026 11:00 - 11:30 People: Dániel Lukács, Péter Bereczky, Dániel Horpácsi
… freshly generated references are guaranteed to be distinct from all references …
Higher-order fork, modally
HOPE 2026 When: Mon 24 Aug 2026 10:00 - 10:30 People: Aghilas Boussaa, Wenhao Tang, Sam Lindley
… is parametric in its effects, without the need for any effect variables at all. …
Set-Theoretic Type Checking of Beginner Erlang Code: A Retrospective Study
Erlang 2026 When: Fri 28 Aug 2026 11:30 - 12:00 People: Albert Schimpf, Stefan Wehr, Annette Bieniusa
… idiomatic catch-all \texttt{true} clause—a shape that community style guides …
Experience Report: Graph Rewriting with Lexical Effect Handlers
HOPE 2026 When: Mon 24 Aug 2026 09:30 - 10:00 People: Marvin Borner
… , animated layout. All of this is implemented as compact, self-contained libraries …
Demo: Drawing Algorithms as Modular Objects: A Framework for Procedurally Generated Visual Arts and Music
FARM 2026 When: Mon 24 Aug 2026 14:00 - 14:22 People: Xingyu Dong, Daniel Průša, Michael Wehar, Chen Xu
… binary matrix, our task is to enumerate all rectangular blocks containing only 1 …
Coercive Subtyping for Implicit Functorial Programming
Haskell 2026 When: Sat 29 Aug 2026 11:30 - 12:00 People: Ryan Doenges, Caden Parajuli, Ayden Lamparski, Ke Wu, Aaron Stump
… that the resulting system of coercions is coherent, meaning that all possible choices … technique of normalization by evaluation. All definitions and theorems …
The Next 700 Block-Based Editors (Keynote)
Haskell 2026 When: Fri 28 Aug 2026 09:05 - 10:15 People: Ravi Chugh
… , text, and structure-editing each have merits. Can’t we all just get along …
Wren: A Fast Logic Programming eDSL With Host Language Garbage Collection
LOPSTR+PPDP 2026 When: Fri 28 Aug 2026 12:00 - 12:30 People: Kyle Dewey, Mehmet Emre
… languages. However, all existing LP eDSLs have often extremely poor performance in comparison to dedicated LP languages. Furthermore, all are heavy on small …
Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations
LOPSTR+PPDP 2026 When: Sat 29 Aug 2026 11:30 - 12:00 People: David Knothe, Oliver Bringmann
… pipeline, thereby fully preserving all top-level semantic preservation theorems …
Arbiter: Distributed Job Queues using Haskell and PostgreSQL
Haskell 2026 When: Fri 28 Aug 2026 16:00 - 16:35 People: Joshua Miller
… Background job queues have moved into the database. Oban in Elixir, River in Go and Solid Queue in Rails all run on PostgreSQL, because a message broker cannot join the transaction that produced the job. Haskell’s options are narrower …
Deterministic Concurrency
ICFP Keynotes When: Tue 25 Aug 2026 09:00 - 10:00 People: Edward Lee
… as exhibiting “observably different behavior given the same inputs.” But nearly all …. For example, the time at which an output is produced is observably different for all … systems. I will then argue that, contrary to almost all current practice …
Bimodels and Biorthogonality for Abstract Machines
ICFP Artifacts People: April Tune, Alex Kavvos
… the CK and CEK machines, all as corollaries. All results are mechanized in Agda. …
Bimodels and Biorthogonality for Abstract Machines
ICFP Papers When: Wed 26 Aug 2026 13:30 - 13:48 People: April Tune, Alex Kavvos
… the CK and CEK machines, all as corollaries. All results are mechanized in Agda. …
An Exploration of First-Class Constrained Types: Semantics, Soundness, Principal Type Inference, and a Characterization of Termination
ICFP Artifacts People: Chun Kit Lam, Florent Ferrari-Dominguez, Lionel Parreaux
… interesting properties. First, all well-typed FCCT terms terminate under call …, all CBN-terminating terms are well-typed in FCCT. Together, these two properties … FCCTI to track abstracted call contexts, ensuring termination on all input terms …
Mode Crossing
ICFP Artifacts People: Benjamin Peters, Jules Jacobs, Diana Kalinichenko, Liam Stevenson, Aspen Smith, Derek Dreyer, Richard A. Eisenberg
… the empirical measurements in the appendix - a virtual machine to with all …
First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of Termination
ICFP Papers When: Tue 25 Aug 2026 10:48 - 11:06 People: Chun Kit Lam, Florent Ferrari-Dominguez, Lionel Parreaux
… exhibits interesting properties. First, all well-typed FCCT terms terminate under …. Second, all CBN-terminating terms are well-typed in FCCT. Together, these two … approximation by sharing polymorphic instantiations, ensuring termination on all input …
Coverage Types Modulo Equivalences
ICFP SRC When: Wed 26 Aug 2026 14:51 - 14:57 People: Aaryan Prakash, Benjamin Delaware
… they enforce all distinct inputs must be generated. We propose an extension …
A Catenable, Splittable, Transient Sequence Data Structure
ICFP Papers When: Tue 25 Aug 2026 11:24 - 11:42 People: Arthur Charguéraud, François Pottier
… for a one-size-fits-all, general-purpose sequence data structure. …
RunbookFX: Type- and Effect-Safe LLM Synthesis for Executable Incident Diagnosis and Mitigation
ICFP Papers People: Yifan Xiao, Shijie Li, Yuhao Ge
… and multi-step layers, 18 now close with \texttt{Qed}—including all Canonical Forms, all effect-operation Inversion lemmas, Value Typing, de~Bruijn weakening …
Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations
ICFP Papers When: Wed 26 Aug 2026 10:48 - 11:06 People: Patrick Bahr
… for all source programs is too strong a requirement for complex source languages … calculation techniques, all while maintaining the same strong correctness guarantees …
Completeness of Iris-Based Program Logics
ICFP Artifacts People: Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, Joseph Tassarotti
… ), and a relational logic for proving refinement. All our results have been mechanized …
Completeness of Iris-Based Program Logics
ICFP Papers When: Thu 27 Aug 2026 14:42 - 15:00 People: Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, Joseph Tassarotti
… ), and a relational logic for proving refinement. All our results have been …
QuickChecking Convergence of Rewriting Systems (Functional Pearl)
ICFP Papers When: Wed 26 Aug 2026 10:30 - 10:48 People: Koen Claessen
… here: exhaustively computing all normal forms is fundamentally flawed and too slow …
A Separation Logic for Parallel Time Complexity with Work and Span Credits
ICFP Papers When: Tue 25 Aug 2026 14:24 - 14:42 People: Alexandre Moine, Sam Westrick, Joseph Tassarotti
… concurrency with parallelism. All the presented results are mechanized in the Rocq …