ICFP 2022
Proceedings of the ACM on Programming Languages, Volume 6, Number ICFP
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 6, Number ICFP, September 11–16, 2022, Ljubljana, Slovenia

ICFP – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message
Sponsors

Papers

Beyond Relooper: Recursive Translation of Unstructured Control Flow to Structured Control Flow (Functional Pearl)
Norman Ramsey
(Tweag, France; Tufts University, USA)
Publisher's Version 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 Artifacts Reusable
Generating Circuits with Generators
Marek Materzok
(University of Wrocław, Poland)
Publisher's Version Artifacts Reusable
Monadic Compiler Calculation (Functional Pearl)
Patrick Bahr and Graham Hutton
(IT University of Copenhagen, Denmark; University of Nottingham, UK)
Publisher's Version 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 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 Artifacts Reusable
Datatype-Generic Programming Meets Elaborator Reflection
Hsiang-Shang Ko, Liang-Ting Chen, and Tzu-Chi Lin
(Academia Sinica, Taiwan)
Publisher's Version Artifacts Reusable
Formal Reasoning about Layered Monadic Interpreters
Irene Yoon, Yannick Zakowski, and Steve Zdancewic
(University of Pennsylvania, USA; Inria, France)
Publisher's Version 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 Artifacts Reusable
Program Adverbs and Tlön Embeddings
Yao Li and Stephanie Weirich
(Portland State University, USA; University of Pennsylvania, USA)
Publisher's Version 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 Info 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 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 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 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 Artifacts Reusable
Staged Compilation with Two-Level Type Theory
András Kovács
(Eötvös Loránd University, Hungary)
Publisher's Version Info 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 Artifacts Reusable
Practical Generic Programming over a Universe of Native Datatypes
Lucas Escot and Jesper Cockx
(Delft University of Technology, Netherlands)
Publisher's Version 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 Archive submitted (490 kB) Artifacts Reusable
Aeneas: Rust Verification by Functional Translation
Son Ho and Jonathan Protzenko
(Inria, France; Microsoft Research, USA)
Publisher's Version Info 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 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 Info 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 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 Artifacts Reusable

proc time: 7.82