ICFP 2022
Proceedings of the ACM on Programming Languages, Volume 6, Number ICFP

Title Page

Editorial Message

Sponsors

Beyond Relooper: Recursive Translation of Unstructured Control Flow to Structured Control Flow (Functional Pearl)
Norman Ramsey
(Tweag, France; Tufts University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Searching Entangled Program Spaces
James Koppel, Zheng Guo, Edsko de Vries, Armando Solar-Lezama, and Nadia Polikarpova
(Massachusetts Institute of Technology, USA; University of California at San Diego, USA; Well-Typed LLP, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Generating Circuits with Generators
Marek Materzok
(University of Wrocław, Poland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Monadic Compiler Calculation (Functional Pearl)
Patrick Bahr and Graham Hutton
(IT University of Copenhagen, Denmark; University of Nottingham, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A Simple and Efficient Implementation of Strong Call by Need by an Abstract Machine
Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab
(University of Wrocław, Poland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Linearly Qualified Types: Generic Inference for Capabilities and Uniqueness
Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, and Richard A. Eisenberg
(Tweag, France; Imperial College London, UK; University of Gothenburg, Sweden)

Publisher's Version

Propositional Equality for Gradual Dependently Typed Programming
Joseph Eremondi, Ronald Garcia, and Éric Tanter
(University of British Columbia, Canada; University of Chile, Chile)

Publisher's Version

Verified Symbolic Execution with Kripke Specification Monads (and No Meta-programming)
Steven Keuchel, Sander Huyghebaert, Georgy Lukyanov, and Dominique Devriese
(Vrije Universiteit Brussel, Belgium; Newcastle University, UK; KU Leuven, Belgium)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Datatype-Generic Programming Meets Elaborator Reflection
Hsiang-Shang Ko, Liang-Ting Chen, and Tzu-Chi Lin
(Academia Sinica, Taiwan)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Formal Reasoning about Layered Monadic Interpreters
Irene Yoon, Yannick Zakowski, and Steve Zdancewic
(University of Pennsylvania, USA; Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Later Credits: Resourceful Reasoning for the Later Modality
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer
(MPI-SWS, Germany; New York University, USA; Massachusetts Institute of Technology, USA; Radboud University Nijmegen, Netherlands; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Program Adverbs and Tlön Embeddings
Yao Li and Stephanie Weirich
(Portland State University, USA; University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Structural versus Pipeline Composition of Higher-Order Functions (Experience Report)
Elijah Rivera and Shriram Krishnamurthi
(Brown University, USA)

Publisher's Version

Reference Counting with Frame Limited Reuse
Anton Lorenzen and Daan Leijen
(University of Bonn, Germany; Microsoft Research, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Modular Probabilistic Models via Algebraic Effects
Minh Nguyen, Roly Perera, Meng Wang, and Nicolas Wu
(University of Bristol, UK; Alan Turing Institute, UK; Imperial College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A Completely Unique Account of Enumeration
Cas van der Rest and Wouter Swierstra
(Delft University of Technology, Netherlands; Utrecht University, Netherlands)

Publisher's Version

Introduction and Elimination, Left and Right
Klaus Ostermann, David Binder, Ingo Skupin, Tim Süberkrüb, and Paul Downen
(University of Tübingen, Germany; University of Massachusetts at Lowell, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom
Jules Jacobs, Stephanie Balzer, and Robbert Krebbers
(Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Fusing Industry and Academia at GitHub (Experience Report)
Patrick Thomson, Rob Rix, Nicolas Wu, and Tom Schrijvers
(GitHub, USA; GitHub, Canada; Imperial College London, UK; KU Leuven, Belgium)

Publisher's Version

‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl)
Sebastian Ullrich and Leonardo de Moura
(KIT, Germany; Microsoft Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Staged Compilation with Two-Level Type Theory
András Kovács
(Eötvös Loránd University, Hungary)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Constraint-Based Type Inference for FreezeML
Frank Emrich, Jan Stolarek, James Cheney, and Sam Lindley
(University of Edinburgh, UK)

Publisher's Version

Safe Couplings: Coupled Refinement Types
Elizaveta Vasilenko, Niki Vazou, and Gilles Barthe
(IMDEA Software Institute, Spain; HSE University, Russia; MPI-SP, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Practical Generic Programming over a Universe of Native Datatypes
Lucas Escot and Jesper Cockx
(Delft University of Technology, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Analyzing Binding Extent in 3CPS
Benjamin Quiring, John Reppy, and Olin Shivers
(University of Maryland, USA; University of Chicago, USA; Northeastern University, USA)

Publisher's Version Artifacts Reusable

Entanglement Detection with Near-Zero Cost
Sam Westrick, Jatin Arora, and Umut A. Acar
(Carnegie Mellon University, USA)

Publisher's Version Published Artifact Archive submitted (490 kB) Artifacts Available Artifacts Reusable

Aeneas: Rust Verification by Functional Translation
Son Ho and Jonathan Protzenko
(Inria, France; Microsoft Research, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Automatically Deriving Control-Flow Graph Generators from Operational Semantics
James Koppel, Jackson Kearl, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Normalization for Fitch-Style Modal Calculi
Nachiappan Valliappan, Fabian Ruch, and Carlos Tomé Cortiñas
(Chalmers University of Technology, Sweden)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Multi Types and Reasonable Space
Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni
(Inria, France; École Polytechnique, France; University of Bologna, Italy)

Publisher's Version

On Feller Continuity and Full Abstraction
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, and Francesco Gavazzo
(MPI-SP, Germany; IMDEA Software Institute, Spain; CNRS, France; University of Bologna, Italy; Inria, France)

Publisher's Version

The Theory of Call-by-Value Solvability
Beniamino Accattoli and Giulio Guerrieri
(Inria, France; École Polytechnique, France; Huawei Edinburgh Research Centre, UK)

Publisher's Version

Random Testing of a Higher-Order Blockchain Language (Experience Report)
Tram Hoang, Anton Trunov, Leonidas Lampropoulos, and Ilya Sergey
(National University of Singapore, Singapore; Zilliqa Research, Russia; University of Maryland at College Park, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Flexible Presentations of Graded Monads
Shin-ya Katsumata, Dylan McDermott, Tarmo Uustalu, and Nicolas Wu
(National Institute of Informatics, Japan; Reykjavik University, Iceland; Tallinn University of Technology, Estonia; Imperial College London, UK)

Publisher's Version

A Reasonably Gradual Type Theory
Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, and Éric Tanter
(Inria, France; University of Chile, Chile)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable