ICFP 2023
Proceedings of the ACM on Programming Languages, Volume 7, Number ICFP

Title Page

Article: icfp23foreword-fm000-p doi:

Editorial Message

Article: icfp23foreword-fm001-p doi:

Sponsors

Article: icfp23foreword-fm003-p doi:

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 Article: icfp23main-p6-p doi:10.1145/3607830

Higher-Order Property-Directed Reachability
Hiroyuki Katsura, Naoki Kobayashi, and Ryosuke Sato
(University of Tokyo, Japan)

Publisher's Version Article: icfp23main-p8-p doi:10.1145/3607831

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 Article: icfp23main-p11-p doi:10.1145/3607832

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 Article: icfp23main-p14-p doi:10.1145/3607833

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 Article: icfp23main-p17-p doi:10.1145/3607835

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 Article: icfp23main-p18-p doi:10.1145/3607836

Explicit Refinement Types
Jad Elkhaleq Ghalayini and Neel Krishnaswami
(University of Cambridge, UK)

Publisher's Version Article: icfp23main-p19-p doi:10.1145/3607837

Typing Records, Maps, and Structs
Giuseppe Castagna
(CNRS, France; Université Paris Cité, France)

Publisher's Version Article: icfp23main-p23-p doi:10.1145/3607838

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 Article: icfp23main-p25-p doi:10.1145/3607839

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 Article: icfp23main-p27-p doi:10.1145/3607840

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 Article: icfp23main-p29-p doi:10.1145/3607841

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 Article: icfp23main-p38-p doi:10.1145/3607842

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 Article: icfp23main-p40-p doi:10.1145/3607843

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 Article: icfp23main-p44-p doi:10.1145/3607844

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 Article: icfp23main-p46-p doi:10.1145/3607845

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 Article: icfp23main-p48-p doi:10.1145/3607846

Asynchronous Modal FRP
Patrick Bahr and Rasmus Ejlers Møgelberg
(IT University of Copenhagen, Denmark)

Publisher's Version Article: icfp23main-p51-p doi:10.1145/3607847

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 Article: icfp23main-p53-p doi:10.1145/3607848

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 Article: icfp23main-p55-p doi:10.1145/3607849

Modular Models of Monoids with Operations
Zhixuan Yang and Nicolas Wu
(Imperial College London, UK)

Publisher's Version Article: icfp23main-p69-p doi:10.1145/3607850

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 Article: icfp23main-p72-p doi:10.1145/3607851

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 Article: icfp23main-p74-p doi:10.1145/3607852

More Fixpoints! (Functional Pearl)
Joachim Breitner
(Unaffiliated, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: icfp23main-p80-p doi:10.1145/3607853

Intrinsically Typed Sessions with Callbacks (Functional Pearl)
Peter Thiemann
(University of Freiburg, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: icfp23main-p93-p doi:10.1145/3607854

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 Article: icfp23main-p104-p doi:10.1145/3607855

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 Article: icfp23main-p122-p doi:10.1145/3607856

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) Article: icfp23main-p129-p doi:10.1145/3607857

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 Artifacts Available Artifacts Reusable Article: icfp23main-p134-p doi:10.1145/3607858

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 Article: icfp23main-p142-p doi:10.1145/3607859

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 Article: icfp23main-p161-p doi:10.1145/3607860

Timely Computation
Conal Elliott
(Independent, USA)

Publisher's Version Article: icfp23main-p186-p doi:10.1145/3607861

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 Article: icfp23main-p215-p doi:10.1145/3607862

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 Article: icfp23main-p279-p doi:10.1145/3607863