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 RamseyORCID logo
(Tweag, France; Tufts University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Searching Entangled Program Spaces
James Koppel ORCID logo, Zheng Guo ORCID logo, Edsko de Vries ORCID logo, Armando Solar-Lezama ORCID logo, and Nadia PolikarpovaORCID logo
(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 ORCID logo
(University of Wrocław, Poland)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Monadic Compiler Calculation (Functional Pearl)
Patrick BahrORCID logo and Graham Hutton ORCID logo
(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 BiernackaORCID logo, Witold CharatonikORCID logo, and Tomasz DrabORCID logo
(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 ORCID logo, Csongor Kiss ORCID logo, Jean-Philippe Bernardy ORCID logo, Nicolas WuORCID logo, and Richard A. EisenbergORCID logo
(Tweag, France; Imperial College London, UK; University of Gothenburg, Sweden)
Publisher's Version
Propositional Equality for Gradual Dependently Typed Programming
Joseph Eremondi ORCID logo, Ronald GarciaORCID logo, and Éric TanterORCID logo
(University of British Columbia, Canada; University of Chile, Chile)
Publisher's Version
Verified Symbolic Execution with Kripke Specification Monads (and No Meta-programming)
Steven KeuchelORCID logo, Sander Huyghebaert ORCID logo, Georgy Lukyanov ORCID logo, and Dominique DevrieseORCID logo
(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 KoORCID logo, Liang-Ting ChenORCID logo, and Tzu-Chi Lin ORCID logo
(Academia Sinica, Taiwan)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Formal Reasoning about Layered Monadic Interpreters
Irene YoonORCID logo, Yannick ZakowskiORCID logo, and Steve ZdancewicORCID logo
(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 ORCID logo, Lennard Gäher ORCID logo, Joseph Tassarotti ORCID logo, Ralf Jung ORCID logo, Robbert KrebbersORCID logo, Lars BirkedalORCID logo, and Derek DreyerORCID logo
(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 LiORCID logo and Stephanie Weirich ORCID logo
(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 ORCID logo and Shriram Krishnamurthi ORCID logo
(Brown University, USA)
Publisher's Version
Reference Counting with Frame Limited Reuse
Anton LorenzenORCID logo and Daan LeijenORCID logo
(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 ORCID logo, Roly Perera ORCID logo, Meng Wang ORCID logo, and Nicolas WuORCID logo
(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 RestORCID logo and Wouter SwierstraORCID logo
(Delft University of Technology, Netherlands; Utrecht University, Netherlands)
Publisher's Version
Introduction and Elimination, Left and Right
Klaus Ostermann ORCID logo, David Binder ORCID logo, Ingo Skupin ORCID logo, Tim Süberkrüb ORCID logo, and Paul Downen ORCID logo
(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 JacobsORCID logo, Stephanie BalzerORCID logo, and Robbert KrebbersORCID logo
(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 ORCID logo, Rob Rix ORCID logo, Nicolas WuORCID logo, and Tom SchrijversORCID logo
(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 ORCID logo and Leonardo de Moura ORCID logo
(KIT, Germany; Microsoft Research, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Staged Compilation with Two-Level Type Theory
András KovácsORCID logo
(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 ORCID logo, Jan Stolarek ORCID logo, James Cheney ORCID logo, and Sam Lindley ORCID logo
(University of Edinburgh, UK)
Publisher's Version
Safe Couplings: Coupled Refinement Types
Elizaveta Vasilenko ORCID logo, Niki VazouORCID logo, and Gilles Barthe ORCID logo
(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 ORCID logo and Jesper Cockx ORCID logo
(Delft University of Technology, Netherlands)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Analyzing Binding Extent in 3CPS
Benjamin Quiring ORCID logo, John Reppy ORCID logo, and Olin Shivers ORCID logo
(University of Maryland, USA; University of Chicago, USA; Northeastern University, USA)
Publisher's Version Artifacts Reusable
Entanglement Detection with Near-Zero Cost
Sam WestrickORCID logo, Jatin Arora ORCID logo, and Umut A. Acar ORCID logo
(Carnegie Mellon University, USA)
Publisher's Version Published Artifact Archive submitted (490 kB) Artifacts Available Artifacts Reusable
Aeneas: Rust Verification by Functional Translation
Son HoORCID logo and Jonathan ProtzenkoORCID logo
(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 ORCID logo, Jackson Kearl ORCID logo, and Armando Solar-Lezama ORCID logo
(Massachusetts Institute of Technology, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Normalization for Fitch-Style Modal Calculi
Nachiappan Valliappan ORCID logo, Fabian Ruch ORCID logo, and Carlos Tomé Cortiñas ORCID logo
(Chalmers University of Technology, Sweden)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
Multi Types and Reasonable Space
Beniamino AccattoliORCID logo, Ugo Dal LagoORCID logo, and Gabriele VanoniORCID logo
(Inria, France; École Polytechnique, France; University of Bologna, Italy)
Publisher's Version
On Feller Continuity and Full Abstraction
Gilles Barthe ORCID logo, Raphaëlle Crubillé ORCID logo, Ugo Dal LagoORCID logo, and Francesco Gavazzo ORCID logo
(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 AccattoliORCID logo and Giulio Guerrieri ORCID logo
(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 ORCID logo, Anton Trunov ORCID logo, Leonidas LampropoulosORCID logo, and Ilya SergeyORCID logo
(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 ORCID logo, Dylan McDermott ORCID logo, Tarmo Uustalu ORCID logo, and Nicolas WuORCID logo
(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 ORCID logo, Meven Lennon-BertrandORCID logo, Nicolas TabareauORCID logo, and Éric TanterORCID logo
(Inria, France; University of Chile, Chile)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

proc time: 7.73