ICFP 2022

35 papers

1. 'do' unchained: embracing local imperativity in a purely functional language (functional pearl) · Sebastian Ullrich, Leonardo de Moura
2. A completely unique account of enumeration · Cas van der Rest, Wouter Swierstra
3. A reasonably gradual type theory · Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter
4. A simple and efficient implementation of strong call by need by an abstract machine · Malgorzata Biernacka, Witold Charatonik, Tomasz Drab
5. Aeneas: Rust verification by functional translation · Son Ho, Jonathan Protzenko
6. Analyzing binding extent in 3CPS · Benjamin Quiring, John H. Reppy, Olin Shivers
7. Automatically deriving control-flow graph generators from operational semantics · James Koppel, Jackson Kearl, Armando Solar-Lezama
8. Beyond Relooper: recursive translation of unstructured control flow to structured control flow (functional pearl) · Norman Ramsey
9. Constraint-based type inference for FreezeML · Frank Emrich, Jan Stolarek, James Cheney, Sam Lindley
10. Datatype-generic programming meets elaborator reflection · Hsiang-Shang Ko, Liang-Ting Chen, Tzu-Chi Lin
11. Entanglement detection with near-zero cost · Sam Westrick, Jatin Arora, Umut A. Acar
12. Flexible presentations of graded monads · Shin-ya Katsumata, Dylan McDermott, Tarmo Uustalu, Nicolas Wu
13. Formal reasoning about layered monadic interpreters · Irene Yoon, Yannick Zakowski, Steve Zdancewic
14. Fusing industry and academia at GitHub (experience report) · Patrick Thomson, Rob Rix, Nicolas Wu, Tom Schrijvers
15. Generating circuits with generators · Marek Materzok
16. Introduction and elimination, left and right · Klaus Ostermann, David Binder, Ingo Skupin, Tim Süberkrüb, Paul Downen
17. Later credits: resourceful reasoning for the later modality · Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal + 1 more
18. Linearly qualified types: generic inference for capabilities and uniqueness · Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, Richard A. Eisenberg
19. Modular probabilistic models via algebraic effects · Minh Nguyen, Roly Perera, Meng Wang, Nicolas Wu
20. Monadic compiler calculation (functional pearl) · Patrick Bahr, Graham Hutton
21. Multi types and reasonable space · Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
22. Multiparty GV: functional multiparty session types with certified deadlock freedom · Jules Jacobs, Stephanie Balzer, Robbert Krebbers
23. Normalization for fitch-style modal calculi · Nachiappan Valliappan, Fabian Ruch, Carlos Tomé Cortiñas
24. On Feller continuity and full abstraction · Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo
25. Practical generic programming over a universe of native datatypes · Lucas Escot, Jesper Cockx
26. Program adverbs and Tlön embeddings · Yao Li, Stephanie Weirich
27. Propositional equality for gradual dependently typed programming · Joseph Eremondi, Ronald Garcia, Éric Tanter
28. Random testing of a higher-order blockchain language (experience report) · Tram Hoang, Anton Trunov, Leonidas Lampropoulos, Ilya Sergey
29. Reference counting with frame limited reuse · Anton Lorenzen, Daan Leijen
30. Safe couplings: coupled refinement types · Elizaveta Vasilenko, Niki Vazou, Gilles Barthe
31. Searching entangled program spaces · James Koppel, Zheng Guo, Edsko de Vries, Armando Solar-Lezama, Nadia Polikarpova
32. Staged compilation with two-level type theory · András Kovács
33. Structural versus pipeline composition of higher-order functions (experience report) · Elijah Rivera, Shriram Krishnamurthi
34. The theory of call-by-value solvability · Beniamino Accattoli, Giulio Guerrieri
35. Verified symbolic execution with Kripke specification monads (and no meta-programming) · Steven Keuchel, Sander Huyghebaert, Georgy Lukyanov, Dominique Devriese