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 ORCID logo, Samantha Frohlich ORCID logo, Meng Wang ORCID logo, and Nicolas WuORCID logo
(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 ORCID logo, Naoki KobayashiORCID logo, and Ryosuke Sato ORCID logo
(University of Tokyo, Japan)
Publisher's Version
Special Delivery: Programming with Mailbox Types
Simon Fowler ORCID logo, Duncan Paul Attard ORCID logo, Franciszek Sowul ORCID logo, Simon J. Gay ORCID logo, and Phil Trinder ORCID logo
(University of Glasgow, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)
Thomas Bourgeat ORCID logo, Ian Clester ORCID logo, Andres ErbsenORCID logo, Samuel Gruetter ORCID logo, Pratap Singh ORCID logo, Andy Wright ORCID logo, and Adam ChlipalaORCID logo
(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 ORCID logo, Mohsen Ghaffari ORCID logo, Einar Broch Johnsen ORCID logo, and Andrzej WąsowskiORCID logo
(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 ORCID logo, Ben Greenman ORCID logo, Matthias Felleisen ORCID logo, and Christos Dimoulas ORCID logo
(Northwestern University, USA; Brown University, USA; Northeastern University, USA)
Publisher's Version
Explicit Refinement Types
Jad Elkhaleq Ghalayini ORCID logo and Neel Krishnaswami ORCID logo
(University of Cambridge, UK)
Publisher's Version
Typing Records, Maps, and Structs
Giuseppe Castagna ORCID logo
(CNRS, France; Université Paris Cité, France)
Publisher's Version
LURK: Lambda, the Ultimate Recursive Knowledge (Experience Report)
Nada Amin ORCID logo, John Burnham ORCID logo, François Garillot ORCID logo, Rosario Gennaro ORCID logo, Chhi’mèd Künzang ORCID logo, Daniel Rogozin ORCID logo, and Cameron Wong ORCID logo
(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 ORCID logo, Daan LeijenORCID logo, and Wouter SwierstraORCID logo
(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 ORCID logo, Mike Dodds ORCID logo, Ivan Perez ORCID logo, Alwyn E. Goodloe ORCID logo, and Robert Dockins ORCID logo
(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 GoldsteinORCID logo, Samantha Frohlich ORCID logo, Meng Wang ORCID logo, and Benjamin C. PierceORCID logo
(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 ORCID logo and J. Garrett Morris ORCID logo
(University of Iowa, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification
Son HoORCID logo, Aymeric Fromherz ORCID logo, and Jonathan ProtzenkoORCID logo
(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 ORCID logo, Joachim BreitnerORCID logo, Koen Claessen ORCID logo, Ranjit Jhala ORCID logo, Simon Peyton Jones ORCID logo, Olin Shivers ORCID logo, Guy L. Steele Jr. ORCID logo, and Tim Sweeney ORCID logo
(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 ORCID logo, Magnus Madsen ORCID logo, Philipp Schuster ORCID logo, and Jonathan Immanuel Brachthäuser ORCID logo
(Aarhus University, Denmark; University of Tübingen, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Asynchronous Modal FRP
Patrick BahrORCID logo and Rasmus Ejlers MøgelbergORCID logo
(IT University of Copenhagen, Denmark)
Publisher's Version
A General Fine-Grained Reduction Theory for Effect Handlers
Filip Sieczkowski ORCID logo, Mateusz Pyzik ORCID logo, and Dariusz Biernacki ORCID logo
(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 ORCID logo, Shun Kashiwa ORCID logo, and Lindsey Kuper ORCID logo
(University of California at Santa Cruz, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Modular Models of Monoids with Operations
Zhixuan YangORCID logo and Nicolas WuORCID logo
(Imperial College London, UK)
Publisher's Version
MacoCaml: Staging Composable and Compilable Macros
Ningning Xie ORCID logo, Leo White ORCID logo, Olivier Nicole ORCID logo, and Jeremy YallopORCID logo
(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 ORCID logo and Stephanie Weirich ORCID logo
(University of Pennsylvania, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
More Fixpoints! (Functional Pearl)
Joachim BreitnerORCID logo
(Unaffiliated, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Intrinsically Typed Sessions with Callbacks (Functional Pearl)
Peter ThiemannORCID logo
(University of Freiburg, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Calculating Compilers for Concurrency
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
Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)
Jules JacobsORCID logo, Jonas Kastberg Hinrichsen ORCID logo, and Robbert KrebbersORCID logo
(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 ORCID logo, Shriram Krishnamurthi ORCID logo, Kathi Fisler ORCID logo, and Ethel Tshukudu ORCID logo
(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 ORCID logo, Gabriel RadanneORCID logo, and Laure Gonnord ORCID logo
(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 ORCID logo, Jonas Kastberg Hinrichsen ORCID logo, Mário Pereira ORCID logo, Amin TimanyORCID logo, and Lars BirkedalORCID logo
(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 ORCID logo, Alperen Keles ORCID logo, Harrison GoldsteinORCID logo, Benjamin C. PierceORCID logo, and Leonidas LampropoulosORCID logo
(University of Pennsylvania, USA; University of Maryland, College Park, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Timely Computation
Conal ElliottORCID logo
(Independent, USA)
Publisher's Version
A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
Andreas Abel ORCID logo, Nils Anders Danielsson ORCID logo, and Oskar Eriksson ORCID logo
(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 ORCID logo, Sebastian ErdwegORCID logo, and Tobias Hombücher ORCID logo
(TU Darmstadt, Germany; JGU Mainz, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

proc time: 6.4