ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States

ICFP 2023 will feature keynote talks by Anders Hejlsberg, Anil Madhavapeddy, Cristine Rizkallah, and Andreas Rossberg.

Dates
Tracks
Plenary
You're viewing the program in a time zone which is different from your device's time zone change time zone

Tue 5 Sep

Displayed time zone: Pacific Time (US & Canada) change

08:50 - 09:00
08:50
10m
Welcome
ICFP Papers and Events
Nikhil Swamy Microsoft Research
09:00 - 10:00
Morning keynoteICFP Keynotes / ICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Sam Lindley University of Edinburgh
09:00
60m
Keynote
Programming for the planet
ICFP Keynotes
Anil Madhavapeddy University of Cambridge, UK
10:00 - 10:30
10:30 - 12:00
EffectsICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Ningning Xie University of Toronto
10:30
30m
Talk
A General Fine-Grained Reduction Theory for Effect Handlers
ICFP Papers and Events
Filip Sieczkowski Heriot-Watt University, Mateusz Pyzik University of Wrocław, Dariusz Biernacki University of Wrocław
DOI
11:00
30m
Talk
Modular Models of Monoids with Operations
ICFP Papers and Events
Zhixuan Yang Imperial College London, Nicolas Wu Imperial College London
DOI
11:30
30m
Talk
With or Without You: Programming with Effect Exclusion
ICFP Papers and Events
Matthew Lutze Aarhus University, Magnus Madsen Aarhus University, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen
DOI
10:30 - 12:00
Dependent typesICFP Papers and Events at B - Fifth Avenue
Chair(s): James Chapman Input Output
10:30
30m
Talk
Is Sized Typing for Coq Practical?JFP Presentation
ICFP Papers and Events
Jonathan Chan University of Pennsylvania, Yufeng Li University of Waterloo, William J. Bowman University of British Columbia
Link to publication DOI Media Attached
11:00
30m
Talk
Dependently-Typed Programming with Logical Equality Reflection
ICFP Papers and Events
Yiyun Liu University of Pennsylvania, Stephanie Weirich University of Pennsylvania
DOI
11:30
30m
Talk
A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
ICFP Papers and Events
Andreas Abel Gothenburg University, Nils Anders Danielsson Chalmers and Gothenburg University, Oskar Eriksson Chalmers and Gothenburg University
DOI
13:30 - 14:30
Afternoon keynoteICFP Keynotes / ICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Nikhil Swamy Microsoft Research
13:30
60m
Keynote
As low-level as possible, but no lower
ICFP Keynotes
Andreas Rossberg Independent
14:30 - 15:00
15:00 - 16:00
Concurrency and distributionICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Satnam Singh Groq
15:00
30m
Talk
Special Delivery: Programming with Mailbox Types
ICFP Papers and Events
Simon Fowler University of Glasgow, Duncan Paul Attard University of Glasgow, Franciszek Sowul University of Glasgow, Simon J. Gay University of Glasgow, UK, Phil Trinder University of Glasgow
DOI Pre-print
15:30
30m
Talk
HasChor: Functional Choreographic Programming for All (Functional Pearl)Functional PearlDistinguished Paper
ICFP Papers and Events
Gan Shen University of California, Santa Cruz, USA, Shun Kashiwa University of California, Santa Cruz, Lindsey Kuper University of California, Santa Cruz
DOI Pre-print
15:00 - 16:00
FixpointsICFP Papers and Events at B - Fifth Avenue
Chair(s): Sam Tobin-Hochstadt Indiana University
15:00
30m
Talk
Combinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters
ICFP Papers and Events
Sven Keidel TU Darmstadt, Germany, Sebastian Erdweg JGU Mainz, Tobias Hombücher JGU Mainz
DOI
15:30
30m
Talk
More Fixpoints! (Functional Pearl)Functional Pearl
ICFP Papers and Events
Joachim Breitner unaffiliated
DOI Pre-print File Attached
16:30 - 17:30
16:30
35m
Student research contest talks
ICFP Papers and Events
S: Daniel Hillerström Huawei Zurich Research Center, J. Garrett Morris University of Iowa
17:05
25m
Programming contest report
ICFP Papers and Events

Wed 6 Sep

Displayed time zone: Pacific Time (US & Canada) change

09:00 - 10:00
09:00
60m
Keynote
TypeScript: Static types for JavaScript
ICFP Keynotes
10:00 - 10:30
10:30 - 12:00
Verification 1ICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Tahina Ramananandro Microsoft Research
10:30
30m
Talk
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification
ICFP Papers and Events
Son Ho INRIA, Aymeric Fromherz Inria, Jonathan Protzenko Microsoft Research, Redmond
DOI
11:00
30m
Talk
Higher-Order Property-Directed Reachability
ICFP Papers and Events
Hiroyuki Katsura University of Tokyo, Naoki Kobayashi University of Tokyo, Ryosuke Sato University of Tokyo
DOI
11:30
30m
Talk
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation ProtocolsRemote
ICFP Papers and Events
Léon Gondelman Aarhus University, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Mário Pereira NOVA LINCS & DI -- Nova School of Science and Technology, Amin Timany Aarhus University, Lars Birkedal Aarhus University
DOI
10:30 - 12:00
TestingICFP Papers and Events at B - Fifth Avenue
Chair(s): Stephen Dolan Jane Street
10:30
30m
Talk
Reflecting on Random GenerationDistinguished Paper
ICFP Papers and Events
Harrison Goldstein University of Pennsylvania, Samantha Frohlich University of Bristol, Meng Wang University of Bristol, Benjamin C. Pierce University of Pennsylvania
DOI
11:00
30m
Talk
Etna: An Evaluation Platform for Property-Based Testing (Experience Report)Experience Report
ICFP Papers and Events
Jessica Shi University of Pennsylvania, Alperen Keles University of Maryland at College Park, Harrison Goldstein University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Leonidas Lampropoulos University of Maryland, College Park
DOI
11:30
30m
Talk
Formal Specification and Testing for Reinforcement LearningRemote
ICFP Papers and Events
Mahsa Varshosaz IT University of Copenhagen, Denmark, Mohsen Ghaffari IT University of Copenhagen, Einar Broch Johnsen University of Oslo, Andrzej Wąsowski IT University of Copenhagen, Denmark
DOI
13:30 - 14:30
Circuits and monoidsICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Patrik Jansson Chalmers University of Technology
13:30
30m
Talk
Timely Computation
ICFP Papers and Events
Conal Elliott Independenet
DOI Pre-print
14:00
30m
Talk
A well-known representation of monoids and its application to the function ‘vector reverse’Functional PearlJFP PresentationRemote
ICFP Papers and Events
Wouter Swierstra Utrecht University, Netherlands
Link to publication DOI
13:30 - 14:30
Meta programmingICFP Papers and Events at B - Fifth Avenue
Chair(s): Gabriel Radanne Inria
13:30
30m
Talk
Embedding by Unembedding
ICFP Papers and Events
Kazutaka Matsuda Tohoku University, Samantha Frohlich University of Bristol, Meng Wang University of Bristol, Nicolas Wu Imperial College London
DOI
14:00
30m
Talk
MacoCaml: Staging Composable and Compilable Macros
ICFP Papers and Events
Ningning Xie University of Toronto, Leo White Jane Street, Olivier Nicole Tarides, Jeremy Yallop University of Cambridge
DOI Pre-print
15:00 - 16:00
15:00
30m
Talk
Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc
ICFP Papers and Events
Alex Hubers University of Iowa, J. Garrett Morris University of Iowa
DOI Pre-print
15:30
30m
Talk
Typing Records, Maps, and Structs
ICFP Papers and Events
Giuseppe Castagna CNRS; Université Paris Cité
DOI
15:00 - 16:00
Modal FRPICFP Papers and Events at B - Fifth Avenue
Chair(s): Amos Robinson Australian National University, Australia
15:00
30m
Talk
Modal FRP for all: Functional reactive programming without space leaks in HaskellJFP Presentation
ICFP Papers and Events
Patrick Bahr IT University of Copenhagen
Link to publication DOI
15:30
30m
Talk
Asynchronous Modal FRP
ICFP Papers and Events
Patrick Bahr IT University of Copenhagen, Rasmus Ejlers Møgelberg IT University of Copenhagen
DOI Pre-print
16:30 - 17:15
Business meetingICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Nikhil Swamy Microsoft Research
16:30
15m
Awards
Awards
ICFP Papers and Events

File Attached
16:45
5m
JFP at ICFP
ICFP Papers and Events
Gabriele Keller Utrecht University
16:50
5m
Diversity, equality, and inclusion at ICFP
ICFP Papers and Events
Daan Leijen Microsoft Research
16:55
15m
PC Chair's report
ICFP Papers and Events
Sam Lindley University of Edinburgh
File Attached
17:10
5m
ICFP 2024 announcement
ICFP Papers and Events
Marco Gaboardi Boston University
File Attached

Thu 7 Sep

Displayed time zone: Pacific Time (US & Canada) change

10:00 - 10:30
10:30 - 12:00
Language designICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Peter Thiemann University of Freiburg, Germany
10:30
30m
Talk
The Verse Calculus: A Core Calculus for Deterministic Functional Logic ProgrammingDistinguished Paper
ICFP Papers and Events
Lennart Augustsson Epic Games , Joachim Breitner unaffiliated, Koen Claessen Epic Games, Ranjit Jhala Epic Games, Simon Peyton Jones Epic Games , Olin Shivers Epic Games, Guy L. Steele Jr. Oracle Labs, Tim Sweeney Epic Games
DOI
11:00
30m
Talk
FP²: Fully in-Place Functional Programming
ICFP Papers and Events
Anton Lorenzen University of Edinburgh, Daan Leijen Microsoft Research, Wouter Swierstra Utrecht University, Netherlands
DOI Pre-print
11:30
30m
Talk
LURK: Lambda, the Ultimate Recursive Knowledge (Experience Report)Experience Report
ICFP Papers and Events
Nada Amin Harvard University, John Burnham Lurk Lab, François Garillot Lurk Lab, Rosario Gennaro Protocol Labs, Chhi’mèd Künzang Lurk Lab, Daniel Rogozin University College London, Cameron Wong
DOI
10:30 - 12:00
Verification 2ICFP Papers and Events at B - Fifth Avenue
Chair(s): Niki Vazou IMDEA Software Institute
10:30
30m
Talk
Explicit Refinement Types
ICFP Papers and Events
Jad Elkhaleq Ghalayini University of Cambridge, Neel Krishnaswami University of Cambridge
DOI
11:00
30m
Talk
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)Experience Report
ICFP Papers and Events
Thomas Bourgeat , Ian Clester Georgia Institute of Technology, Andres Erbsen MIT, Samuel Gruetter Massachusetts Institute of Technology, Pratap Singh CMU, Andy Wright MIT, Adam Chlipala Massachusetts Institute of Technology
DOI
13:30 - 14:30
Session typing functional pearlsICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Andrew K. Hirsch University at Buffalo, SUNY
13:30
30m
Talk
Intrinsically Typed Sessions with Callbacks (Functional Pearl)Functional Pearl
ICFP Papers and Events
Peter Thiemann University of Freiburg, Germany
DOI
14:00
30m
Talk
Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)Functional PearlRemote
ICFP Papers and Events
Jules Jacobs Radboud University Nijmegen, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Robbert Krebbers Radboud University Nijmegen
DOI
13:30 - 14:30
Blame and educationICFP Papers and Events at B - Fifth Avenue
Chair(s): Benjamin C. Pierce University of Pennsylvania
13:30
30m
Talk
How to Evaluate Blame for Gradual Types, Part 2
ICFP Papers and Events
Lukas Lazarek Northwestern University, Ben Greenman Brown University, Matthias Felleisen PLT @ Northeastern University, Christos Dimoulas PLT @ Northwestern University
DOI
14:00
30m
Talk
What Happens When Students Switch (Functional) Languages (Experience Report)RemoteExperience Report
ICFP Papers and Events
Kuang-Chen Lu Brown University, USA, Shriram Krishnamurthi Brown University, United States, Kathi Fisler Brown University, Ethel Tshukudu University of Botswana
DOI
15:00 - 16:00
15:00
30m
Talk
Calculating Compilers for Concurrency
ICFP Papers and Events
Patrick Bahr IT University of Copenhagen, Graham Hutton University of Nottingham, UK
DOI Pre-print
15:30
30m
Talk
Trustworthy Runtime Verification via Bisimulation (Experience Report)Experience Report
ICFP Papers and Events
Ryan Scott Galois, Inc., Mike Dodds Galois, Inc., Robert Dockins Amazon, Ivan Perez NASA Ames Research Center, Alwyn Goodloe NASA Langley Research Center
DOI Pre-print
15:00 - 16:00
Data representationICFP Papers and Events at B - Fifth Avenue
Chair(s): Lennart Augustsson Epic Games
15:00
30m
Talk
Read/write factorizable programsJFP Presentation
ICFP Papers and Events
Siddharth Bhaskar University of Copenhagen, Jakob Grue Simonsen University of Copenhagen
Link to publication DOI
15:30
30m
Talk
Bit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebraic Data Types
ICFP Papers and Events
Thaïs Baudon ENS de Lyon & LIP, Gabriel Radanne Inria, Laure Gonnord Univ. Grenoble Alpes, Grenoble INP, LCIS, Valence, France
DOI Pre-print Media Attached File Attached
16:30 - 17:30
Fireside chatICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Amal Ahmed Northeastern University, USA
16:30
60m
Other
Fireside chat: Amal Ahmed hosts Felix Klock and Greg Morrisett
ICFP Papers and Events
C: Amal Ahmed Northeastern University, USA, P: Felix Klock Amazon Web Services, P: Greg Morrisett Cornell University
17:45 - 18:15
Ask me anything with Tim SweeneyICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Simon Peyton Jones Epic Games
17:45
30m
Live Q&A
Ask me anything with Tim Sweeney
ICFP Papers and Events
Tim Sweeney Epic Games