ICFP 2024

35 papers

1. A Coq Mechanization of JavaScript Regular Expression Semantics · Noé De Santo, Aurèle Barrière, Clément Pit-Claudel
2. A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler · Guillaume Melquiond, Josué Moreau
3. A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer-Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction · Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, Steve Zdancewic
4. Abstract Interpreters: A Monadic Approach to Modular Verification · Sébastien Michelland, Yannick Zakowski, Laure Gonnord
5. Abstracting Effect Systems for Algebraic Effect Handlers · Takuma Yoshioka, Taro Sekiyama, Atsushi Igarashi
6. Almost-Sure Termination by Guarded Refinement · Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
7. Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System · Satoshi Kura, Hiroshi Unno
8. Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl) · Patrick Bahr, Graham Hutton
9. Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts · Bram Vandenbogaerde, Quentin Stiévenart, Coen De Roover
10. CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs · Cole Kurashige, Ruyi Ji, Aditya Giridharan, Mark Barbone, Daniel Noor, Shachar Itzhaky + 2 more
11. Call-by-Unboxed-Value · Paul Downen
12. Closure-Free Functional Programming in a Two-Level Type Theory · András Kovács
13. Compiled, Extensible, Multi-language DSLs (Functional Pearl) · Michael Ballantyne, Mitch Gamburg, Jason Hemann
14. Contextual Typing · Xu Xue, Bruno C. d. S. Oliveira
15. Dependent Ghosts Have a Reflection for Free · Théo Winterhalter
16. Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis · Benjamin Quiring, David Van Horn
17. Double-Ended Bit-Stealing for Algebraic Data Types · Martin Elsman
18. Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs · Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti + 1 more
19. Example-Based Reasoning about the Realizability of Polymorphic Programs · Niek Mulleners, Johan Jeuring, Bastiaan Heeren
20. Functional Programming in Financial Markets (Experience Report) · Atze Dijkstra, José Pedro Magalhães, Pierre Néron
21. Gradual Indexed Inductive Types · Mara Malewski, Kenji Maillard, Nicolas Tabareau, Éric Tanter
22. Grokking the Sequent Calculus (Functional Pearl) · David Binder, Marco Tzschentke, Marius Müller, Klaus Ostermann
23. How to Bake a Quantum Π · Jacques Carette, Chris Heunen, Robin Kaarsgaard, Amr Sabry
24. On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRs · Paulo Henrique Torrens, Dominic Orchard, Cristiano D. Vasconcellos
25. Oxidizing OCaml with Modal Memory Management · Anton Lorenzen, Leo White, Stephen Dolan, Richard A. Eisenberg, Sam Lindley
26. Parallel Algebraic Effect Handlers · Ningning Xie, Daniel D. Johnson, Dougal Maclaurin, Adam Paszke
27. Refinement Composition Logic · Youngju Song, Dongjae Lee
28. Snapshottable Stores · Clément Allain, Basile Clément, Alexandre Moine, Gabriel Scherer
29. Sound Borrow-Checking for Rust via Symbolic Semantics · Son Ho, Aymeric Fromherz, Jonathan Protzenko
30. Specification and Verification for Unrestricted Algebraic Effects and Handling · Yahui Song, Darius Foo, Wei-Ngan Chin
31. Staged Compilation with Module Functors · Tsung-Ju Chiang, Jeremy Yallop, Leo White, Ningning Xie
32. Story of Your Lazy Function's Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs · Li-yao Xia, Laura Israel, Maite Kramarz, Nicholas Coltharp, Koen Claessen, Stephanie Weirich + 1 more
33. Synchronous Programming with Refinement Types · Jiawei Chen, José Luiz Vargas de Mendonça, Bereket Ayele, Bereket Ngussie Bekele, Shayan Jalili, Pranjal Sharma + 3 more
34. The Functional, the Imperative, and the Sudoku: Getting Good, Bad, and Ugly to Get Along (Functional Pearl) · Manuel Serrano, Robert Bruce Findler
35. The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures · Yijia Chen, Lionel Parreaux