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

Title Page

Editorial Message

Sponsors

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