Search events for 'all'
A Mechanised Semantics of Erlang's References
Erlang 2026 People: Dániel Lukács, Péter Bereczky, Dániel Horpácsi
… freshly generated references are guaranteed to be distinct from all references …
Set-Theoretic Type Checking of Beginner Erlang Code: A Retrospective Study
Erlang 2026 People: Albert Schimpf, Stefan Wehr, Annette Bieniusa
… eliminates all observed spurious rejections without regressions.
Our findings …
Coercive Subtyping for Implicit Functorial Programming
Haskell 2026 People: Ryan Doenges, Caden Parajuli, Ayden Lamparski, Ke Wu, Aaron Stump
… , meaning that all possible choices of coercions from (A) to (B) end up … by evaluation. All definitions and theorems in the paper are checked in Agda …
The Next 700 Block-Based Editors
Haskell 2026 People: Ravi Chugh
… , text, and structure-editing each have merits. Can’t we all just get along …
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 Papers People: April Tune, Alex Kavvos
… the CK and CEK machines, all as corollaries. All results are mechanized in Agda. …
First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of Termination
ICFP Papers 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 …
A Catenable, Splittable, Transient Sequence Data Structure
ICFP Papers People: Arthur Charguéraud, François Pottier
… for a one-size-fits-all, general-purpose sequence data structure. …
Coverage Types Modulo Equivalences
ICFP SRC People: Aaryan Prakash, Benjamin Delaware
… they enforce all distinct inputs must be generated. We propose an extension …
Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations
ICFP Papers 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 …
QuickChecking Convergence of Rewriting Systems (Functional Pearl)
ICFP Papers People: Koen Claessen
… here: exhaustively computing all normal forms is fundamentally flawed and too slow …
Completeness of Iris-Based Program Logics
ICFP Papers 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 …
A Separation Logic for Parallel Time Complexity with Work and Span Credits
ICFP Papers People: Alexandre Moine, Sam Westrick, Joseph Tassarotti
… concurrency with parallelism. All the presented results are mechanized in the Rocq …