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

Proceedings of the ACM on Programming Languages, Volume 7, Number ICFP, September 4–9, 2023, Seattle, WA, USA

ICFP – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message
Sponsors

Papers

Embedding by Unembedding
Kazutaka Matsuda, Samantha Frohlich, Meng Wang, and Nicolas Wu
(Tohoku University, Japan; University of Bristol, UK; Imperial College London, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Higher-Order Property-Directed Reachability
Hiroyuki Katsura, Naoki Kobayashi, and Ryosuke Sato
(University of Tokyo, Japan)
Publisher's Version
Special Delivery: Programming with Mailbox Types
Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, and Phil Trinder
(University of Glasgow, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)
Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andy Wright, and Adam Chlipala
(Massachusetts Institute of Technology, USA; Georgia Institute of Technology, USA; Carnegie Mellon University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Formal Specification and Testing for Reinforcement Learning
Mahsa Varshosaz, Mohsen Ghaffari, Einar Broch Johnsen, and Andrzej Wąsowski
(IT University of Copenhagen, Denmark; University of Oslo, Norway)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
How to Evaluate Blame for Gradual Types, Part 2
Lukas Lazarek, Ben Greenman, Matthias Felleisen, and Christos Dimoulas
(Northwestern University, USA; Brown University, USA; Northeastern University, USA)
Publisher's Version
Explicit Refinement Types
Jad Elkhaleq Ghalayini and Neel Krishnaswami
(University of Cambridge, UK)
Publisher's Version
Typing Records, Maps, and Structs
Giuseppe Castagna
(CNRS, France; Université Paris Cité, France)
Publisher's Version
LURK: Lambda, the Ultimate Recursive Knowledge (Experience Report)
Nada Amin, John Burnham, François Garillot, Rosario Gennaro, Chhi’mèd Künzang, Daniel Rogozin, and Cameron Wong
(Harvard University, USA; Lurk Lab, USA; Lurk Lab, Canada; City College of New York, USA; University College London, UK)
Publisher's Version Info
FP²: Fully in-Place Functional Programming
Anton Lorenzen, Daan Leijen, and Wouter Swierstra
(University of Edinburgh, UK; Microsoft Research, USA; Utrecht University, Netherlands)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Trustworthy Runtime Verification via Bisimulation (Experience Report)
Ryan G. Scott, Mike Dodds, Ivan Perez, Alwyn E. Goodloe, and Robert Dockins
(Galois, USA; KBR @ NASA Ames Research Center, USA; NASA Ames Research Center, USA; Amazon, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Reflecting on Random Generation
Harrison Goldstein, Samantha Frohlich, Meng Wang, and Benjamin C. Pierce
(University of Pennsylvania, USA; University of Bristol, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc
Alex Hubers and J. Garrett Morris
(University of Iowa, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification
Son Ho, Aymeric Fromherz, and Jonathan Protzenko
(Inria, France; Microsoft Research, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming
Lennart Augustsson, Joachim Breitner, Koen Claessen, Ranjit Jhala, Simon Peyton Jones, Olin Shivers, Guy L. Steele Jr., and Tim Sweeney
(Epic Games, Sweden; Unaffiliated, Germany; Epic Games, USA; Epic Games, UK; Oracle Labs, USA)
Publisher's Version
With or Without You: Programming with Effect Exclusion
Matthew Lutze, Magnus Madsen, Philipp Schuster, and Jonathan Immanuel Brachthäuser
(Aarhus University, Denmark; University of Tübingen, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Asynchronous Modal FRP
Patrick Bahr and Rasmus Ejlers Møgelberg
(IT University of Copenhagen, Denmark)
Publisher's Version
A General Fine-Grained Reduction Theory for Effect Handlers
Filip Sieczkowski, Mateusz Pyzik, and Dariusz Biernacki
(Heriot-Watt University, UK; University of Wrocław, Poland)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
HasChor: Functional Choreographic Programming for All (Functional Pearl)
Gan Shen, Shun Kashiwa, and Lindsey Kuper
(University of California at Santa Cruz, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Modular Models of Monoids with Operations
Zhixuan Yang and Nicolas Wu
(Imperial College London, UK)
Publisher's Version
MacoCaml: Staging Composable and Compilable Macros
Ningning Xie, Leo White, Olivier Nicole, and Jeremy Yallop
(University of Toronto, Canada; Jane Street, UK; Tarides, France; University of Cambridge, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Dependently-Typed Programming with Logical Equality Reflection
Yiyun Liu and Stephanie Weirich
(University of Pennsylvania, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
More Fixpoints! (Functional Pearl)
Joachim Breitner
(Unaffiliated, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Intrinsically Typed Sessions with Callbacks (Functional Pearl)
Peter Thiemann
(University of Freiburg, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Calculating Compilers for Concurrency
Patrick Bahr and Graham Hutton
(IT University of Copenhagen, Denmark; University of Nottingham, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)
Jules Jacobs, Jonas Kastberg Hinrichsen, and Robbert Krebbers
(Radboud University Nijmegen, Netherlands; Aarhus University, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
What Happens When Students Switch (Functional) Languages (Experience Report)
Kuang-Chen Lu, Shriram Krishnamurthi, Kathi Fisler, and Ethel Tshukudu
(Brown University, USA; University of Botswana, Botswana)
Publisher's Version Archive submitted (2.7 MB)
Bit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebraic Data Types
Thaïs Baudon, Gabriel Radanne, and Laure Gonnord
(University of Lyon, France; ENS Lyon, France; UCBL, France; CNRS, France; Inria, France; LIP, France; University Grenoble Alpes, France; Grenoble INP, France; LCIS, France)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols
Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark; NOVA-LINCS, Portugal; NOVA School of Sciences and Tecnhology, Portugal)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Etna: An Evaluation Platform for Property-Based Testing (Experience Report)
Jessica Shi, Alperen Keles, Harrison Goldstein, Benjamin C. Pierce, and Leonidas Lampropoulos
(University of Pennsylvania, USA; University of Maryland, College Park, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Timely Computation
Conal Elliott
(Independent, USA)
Publisher's Version
A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
Andreas Abel, Nils Anders Danielsson, and Oskar Eriksson
(Chalmers University of Technology, Sweden; University of Gothenburg, Sweden)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Combinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters
Sven Keidel, Sebastian Erdweg, and Tobias Hombücher
(TU Darmstadt, Germany; JGU Mainz, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

proc time: 4.72