ICFP 2024
Mon 2 - Sat 7 September 2024 Milan, Italy
You're viewing the program in a time zone which is different from your device's time zone change time zone

Mon 2 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30
Welcome; Robots and SynthesisFARM at Meeting 3
09:00
10m
Day opening
Welcome to FARM!
FARM
Mae Milano Princeton University, Stephen Taylor University of Illinois Urbana-Champaign
09:10
35m
Talk
Using Functional Reactive Programming for Robotic Art
FARM
Eliane I. Schmidli OST – Eastern Switzerland University of Applied Sciences, Farhad Mehta OST – Eastern Switzerland University of Applied Sciences
09:45
23m
Talk
Bridging art and mathematics with Tessella: a Scala functional library for regular polygon finite tessellations of a plane
FARM
10:08
22m
Talk
Functional Curves and Surfaces: Algebraic Geometry Inspired Visuals in Hydra
FARM
Yoni Maltsman Harvey Mudd College
09:00 - 10:30
Welcome & KeynoteErlang at Meeting 4
Chair(s): Kiko Fernandez-Reyes Ericsson, Sweden, Adriana Laura Voinea
09:00
5m
Talk
Welcome to the Erlang Workshop
Erlang
09:05
55m
Keynote
(Keynote) Environmentally sustainable software and data architectures
Erlang
10:00
30m
Talk
Unsafe Impedance: safe languages and safe by design software
Erlang
Lee Barney Brigham Young University-Idaho, Adolfo Neto Federal University of Technology - Paraná
Pre-print
09:00 - 10:30
Icebreaker and Getting the Most Out of ICFPPLMW @ ICFP at Orange 3
Chair(s): Stefan K. Muller Illinois Institute of Technology
09:00
5m
Day opening
Welcome
PLMW @ ICFP
Ningning Xie University of Toronto; Google DeepMind, Stefan K. Muller Illinois Institute of Technology, Thomas Bourgeat EPFL
09:05
40m
Other
PLMW Icebreaker Session
PLMW @ ICFP

09:45
45m
Talk
Getting the Most Out of ICFP
PLMW @ ICFP
Samantha Frohlich University of Bristol
10:30 - 11:00
Coffee breakCatering at Catering Area
11:00 - 12:30
Livecoding and SemanticsFARM at Meeting 3
Chair(s): Mae Milano Princeton University
11:00
22m
Talk
Trane: Musical Janet on the Web
FARM
11:22
22m
Talk
From Konnakol to Live Coding
FARM
Alex McLean Then Try This
11:45
22m
Talk
Demo: Composable Compositions in Tonart
FARM
12:07
22m
Talk
The Maquette Monad
FARM
11:00 - 12:30
Types & CompilersErlang at Meeting 4
11:00
30m
Talk
Same same but different: A Comparative Analysis of Static Type Checkers in Erlang
Erlang
Florian Berger University of Kaiserslautern-Landau, Albert Schimpf University of Kaiserslautern-Landau, Annette Bieniusa University of Kaiserslautern-Landau, Stefan Wehr Offenburg University of Applied Sciences
11:30
30m
Talk
Nominal Types for Erlang
Erlang
Isabell Huang , John Högberg , Tobias Wrigstad Uppsala University, Kiko Fernandez-Reyes Ericsson, Sweden
12:00
30m
Talk
Modeling Erlang Compiler IR as SMT Formulas
Erlang
11:00 - 12:30
Session 1HOPE at Orange 2
11:00
30m
Talk
Amplifying Contextual Distance in Higher-Order Languages, using the Law of Large Numbers
HOPE
Raphaëlle Crubillé CNRS, Houssein Mansour Aix-Marseille Université
11:30
30m
Talk
An Incremental Approach to the Semantics of Borrowing
HOPE
Brianna Marshall Northeastern University, Andrew Wagner Northeastern University, John Li Northeastern University, Olek Gierczak Northeastern University, Amal Ahmed Northeastern University, USA
12:00
30m
Talk
Towards a linear functional translation for borrowing
HOPE
11:00 - 12:30
Panel and Speed MentoringPLMW @ ICFP at Orange 3
Chair(s): Stefan K. Muller Illinois Institute of Technology
11:00
60m
Panel
Research, Grad School, Community - Let's chat!
PLMW @ ICFP
Niki Vazou IMDEA Software Institute, Aymeric Fromherz Inria, Sam Lindley University of Edinburgh, Andreas Rossberg Independent, Samantha Frohlich University of Bristol
12:00
30m
Social Event
Speed mentoring
PLMW @ ICFP

12:30 - 14:00
14:00 - 15:30
Music GenerationFARM at Meeting 3
14:00
22m
Talk
Demo: A Geometric Approach to Generate Musical Rhythmic Patterns in Haskell
FARM
Xavier Góngora Universidad Nacional Autónoma de México
Link to publication DOI
14:22
22m
Talk
Diffusion-Based Sound Synthesis in Music Production
FARM
Pierre-Louis Suckrow Berlin University of the Arts, Technical University of Berlin, Christoph Johannes Weber University of Television and Film Munich, LMU Munich, Sylvia Rothe University of Television and Film Munich
14:45
10m
Talk
Demo: Functional Sound Design
FARM
Stefano Panelli Conservatorio A. Vivaldi Alessandria
14:55
35m
Talk
A Progressive-Adaptive Music Generator (PAMG): An Approach to Interactive Procedural Music for Videogames
FARM
Alvaro Lopez Duarte University of California Riverside
14:00 - 15:30
Testing & VerificationErlang at Meeting 4
14:00
30m
Talk
Erla+: Translating TLA+ Models into Executable Actor-Based Implementations
Erlang
Marian Hristov University of Kaiserslautern-Landau, Annette Bieniusa University of Kaiserslautern-Landau
DOI
14:30
30m
Talk
Controlled Scheduling of Concurrent Elixir Programs
Erlang
Luis Eduardo Bueso de Barrio Universidad Politécnica de Madrid, Lars-Åke Fredlund Universidad Politécnica de Madrid, Clara Benac Earle Universidad Politécnica de Madrid, Ángel Herranz Universidad Politécnica de Madrid, Julio Mariño Universidad Politécnica de Madrid
15:00
30m
Talk
Is this really a refactoring? Automated equivalence checking for Erlang projects
Erlang
Bendegúz Seres Eötvös Loránd University, Dániel Horpácsi Eötvös Loránd University, Simon Thompson IOHK, University of Kent, and ELTE
14:00 - 15:30
Session 2HOPE at Orange 2
14:00
30m
Talk
Effectful Assembly Programming with AsmFX
HOPE
Brian Campbell University of Edinburgh, Sam Lindley University of Edinburgh, Wilmer Ricciotti University of Edinburgh, UK, Ian Stark The University of Edinburgh
File Attached
14:30
30m
Talk
Logical Relations for Effect Capabilities
HOPE
Patrycja Balik University of Wrocław, Piotr Polesiuk University of Wrocław
15:00
30m
Talk
Paella: algebraic effects with parameters and their handlers
HOPE
Jesse Sigal University of Edinburgh, Ohad Kammar University of Edinburgh, Cristina Matache University of Edinburgh, Conor McBride University of Strathclyde
Media Attached File Attached
14:00 - 15:30
Technical SessionPLMW @ ICFP at Orange 3
Chair(s): Ningning Xie University of Toronto; Google DeepMind
14:00
45m
Talk
How to read a research paper
PLMW @ ICFP
Simon Peyton Jones Epic Games
14:45
45m
Talk
Self-verification for Proof Assistants
PLMW @ ICFP
15:30 - 16:00
Coffee breakCatering at Catering Area
16:00 - 17:30
Software Engineering & ClosingErlang at Meeting 4
16:00
30m
Talk
Elixir-powered Low-income Animal Shelter Support: an Experience Report from Conception to Production
Erlang
Carla Rodríguez Estévez Universidade da Coruña, Spain, Laura M. Castro University of A Coruña
16:30
30m
Talk
The Benefits of Tierless Elixir/Potato for Engineering IoT Systems
Erlang
Solaris Li University of Glasgow, Phil Trinder University of Glasgow, Christophe De Troyer Vrije Universiteit Brussel, Mart Lubbers Radboud University Nijmegen, Adrian Ramsingh Sia Fusion Ltd
17:00
30m
Talk
Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors
Erlang
Jonah Pears , Laura Bocchi University of Kent, Raymond Hu Queen Mary University of London
16:00 - 17:30
Session 3HOPE at Orange 2
16:00
30m
Talk
Arrows as applicatives in a monad
HOPE
Leo White Jane Street
File Attached
16:30
30m
Talk
Mechanized monadic equational reasoning for ML references
HOPE
Reynald Affeldt AIST, Jacques Garrigue Nagoya University, Takafumi Saikawa Nagoya University
File Attached
17:00
30m
Talk
Modularizing Reasoning about AI Capabilities via Abstract Dijkstra Monads
HOPE
Cyrus Omar University of Michigan, Patrick Ferris University of Cambridge, UK, Anil Madhavapeddy University of Cambridge, UK
File Attached
16:00 - 17:30
Sharing ExperiencesPLMW @ ICFP at Orange 3
Chair(s): Ningning Xie University of Toronto; Google DeepMind
16:00
45m
Talk
My PhD Compass: 6 Ways to Guide a PhD Towards Success
PLMW @ ICFP
Harrison Goldstein University of Maryland College Park
16:45
45m
Day closing
Conclusion, survey and unstructured time
PLMW @ ICFP

19:00 - 22:30
Performance EveningFARM at Auditorium San Fedele
Chair(s): Stephen Taylor University of Illinois Urbana-Champaign
19:00
60m
Keynote
Refactoring Musical Thought
FARM
Dmitri Tymoczko Princeton University
20:20
15m
Live Coding Konnakol
FARM
Alex McLean Then Try This
20:35
10m
Self-censorship
FARM
cecilia suhr Miami University
20:45
10m
Hydra FCS: A Performance
FARM
Yoni Maltsman Harvey Mudd College
20:55
15m
WAYA
FARM
Stefano Panelli Conservatorio A. Vivaldi Alessandria, Luca Carillo Conservatorio A. Vivaldi Alessandria
21:10
10m
Gamyeon III
FARM
Tae Hong Park Purdue University

Tue 3 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Tuesday keynoteICFP Papers and Events at Green 1-2-3
Chair(s): Brigitte Pientka McGill University
09:00
60m
Keynote
Requirements are All You Need
ICFP Papers and Events
Andrew D. Gordon Cogna and University of Edinburgh
10:00 - 10:30
Coffee breakCatering at Catering Area
10:30 - 12:00
Algebraic and Computational EffectsICFP Papers and Events / JFP First Papers at Green 1-2-3
Chair(s): Patrick Bahr IT University of Copenhagen
10:30
18m
Talk
Abstracting Effect Systems for Algebraic Effect Handlers
ICFP Papers and Events
Takuma Yoshioka Kyoto University, Taro Sekiyama National Institute of Informatics; SOKENDAI, Atsushi Igarashi Kyoto University
DOI
10:48
18m
Talk
Parallel Algebraic Effect Handlers
ICFP Papers and Events
Ningning Xie University of Toronto; Google DeepMind, Daniel D. Johnson University of Toronto; Google DeepMind, Dougal Maclaurin Google DeepMind, Adam Paszke Google DeepMind
DOI
11:06
18m
Talk
Abstract Interpreters: A Monadic Approach to Modular Verification
ICFP Papers and Events
Sébastien Michelland Université Grenoble-Alpes - Grenoble INP - LCIS, Yannick Zakowski Inria - ENS de Lyon - CNRS - UCBL1 - LIP - UMR 5668, Laure Gonnord Université Grenoble-Alpes - Grenoble INP - LCIS
DOI Pre-print
11:24
18m
Talk
Algebraic effects and handlers for arrowsJFP First Paper
JFP First Papers
Takahiro Sanada Fukui Prefectural University
11:42
18m
Talk
How to Bake a Quantum Π
ICFP Papers and Events
Jacques Carette McMaster University, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark, Amr Sabry Indiana University
DOI
12:00 - 13:30
12:00 - 13:30
13:00 - 13:30
ICFP programming contest resultsICFP Programming Contest at Green 1-2-3
13:00
30m
Awards
ICFP Contest Results
ICFP Programming Contest

13:30 - 15:00
Type TheoryICFP Papers and Events / JFP First Papers at Green 1-2-3
Chair(s): Brent Yorgey Hendrix College
13:30
18m
Talk
Normalization by evaluation for modal dependent type theoryJFP First Paper
JFP First Papers
Jason Z.S. Hu McGill University, Junyoung Jang McGill University, Brigitte Pientka McGill University
DOI
13:48
18m
Talk
Closure-Free Functional Programming in a Two-Level Type Theory
ICFP Papers and Events
András Kovács University of Gothenburg
DOI Pre-print
14:06
18m
Talk
Gradual Indexed Inductive Types
ICFP Papers and Events
Mara Malewski Correa University of Chile, Kenji Maillard Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile
DOI
14:24
18m
Talk
Dependent Ghosts Have a Reflection for Free
ICFP Papers and Events
DOI
14:42
18m
Talk
Static Blame for gradual typingJFP First Paper
JFP First Papers
Chenghao Su Nanjing University, Lin Chen Nanjing University, Yanhui Li Nanjing University, Yuming Zhou Nanjing University
DOI
15:00 - 15:30
Coffee breakCatering at Catering Area
15:30 - 17:00
Logical FoundationsICFP Papers and Events / JFP First Papers at Green 1-2-3
Chair(s): Kenji Maillard Inria
15:30
18m
Talk
Grokking the Sequent Calculus (Functional Pearl)
ICFP Papers and Events
David Binder University of Tübingen, Marco Tzschentke Universität Tübingen, Marius Müller University of Tübingen, Klaus Ostermann University of Tübingen
DOI
15:48
18m
Talk
Call-by-Unboxed-Value
ICFP Papers and Events
Paul Downen University of Massachusetts at Lowell
DOI
16:06
18m
Talk
A correct-by-construction conversion from lambda calculus to combinatory logic (JFP Functional Pearls)JFP First Paper
JFP First Papers
Wouter Swierstra Utrecht University, Netherlands
DOI
16:24
18m
Talk
On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRs
ICFP Papers and Events
Paulo Torrens University of Kent, Dominic Orchard University of Kent; University of Cambridge, Cristiano Vasconcellos Santa Catarina State University
DOI Pre-print
16:42
18m
Talk
Example-Based Reasoning about the Realizability of Polymorphic ProgramsDistinguished Paper
ICFP Papers and Events
Niek Mulleners Utrecht University, Johan Jeuring Utrecht University, Bastiaan Heeren Open Universiteit
DOI Pre-print
17:00 - 17:15
Introduction of Industrial SponsorsICFP Papers and Events at Green 1-2-3
17:15 - 18:15
Memorial for D. Turner & ArvindICFP Papers and Events at Green 1-2-3
Chair(s): Marco Gaboardi Boston University
18:30 - 20:00
ICFP ReceptionCatering at Catering Area
18:30 - 20:00
18:30
90m
Poster
SRC Posters
Student Research Competition

Wed 4 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Wednesday keynoteICFP Papers and Events at Green 1-2-3
Chair(s): Andrew Kennedy Facebook London
09:00
60m
Keynote
Capabilities for Control
ICFP Papers and Events
10:00 - 10:30
Coffee breakCatering at Catering Area
10:30 - 12:00
Meta-Programming, Staging, Generic Programming, Partial EvaluationICFP Papers and Events / JFP First Papers at Green 1-2-3
Chair(s): Richard A. Eisenberg Jane Street
10:30
18m
Talk
Staged Compilation with Module Functors
ICFP Papers and Events
Tsung-Ju Chiang University of Toronto, Jeremy Yallop University of Cambridge, Leo White Jane Street, Ningning Xie University of Toronto; Google DeepMind
DOI Pre-print
10:48
18m
Talk
A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler
ICFP Papers and Events
Guillaume Melquiond Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Josué Moreau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria
DOI
11:06
18m
Talk
Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis
ICFP Papers and Events
Benjamin Quiring University of Maryland at College Park, David Van Horn University of Maryland
DOI
11:24
18m
Talk
Compiled, Extensible, Multi-language DSLs (Functional Pearl)Functional Pearl
ICFP Papers and Events
Michael Ballantyne Northeastern University, Mitch Gamburg Unaffiliated, Jason Hemann Seton Hall University
DOI Pre-print
11:42
18m
Talk
Knuth–Morris–Pratt illustrated (JFP Functional Pearls )JFP First Paper
JFP First Papers
Cameron Moy Northeastern University
DOI
12:00 - 13:30
12:00 - 13:30
13:00 - 13:30
13:00
30m
Talk
SRC Presentations
Student Research Competition

13:30 - 15:00
Separation Logic ICFP Papers and Events at Green 1-2-3
Chair(s): Jacques Garrigue Nagoya University
13:30
18m
Talk
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic ProgramsDistinguished Paper
ICFP Papers and Events
Alejandro Aguirre Aarhus University, Philipp G. Haselwarter Aarhus University, Markus de Medeiros New York University, Kwing Hei Li Aarhus University, Simon Oddershede Gregersen New York University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University
DOI Pre-print
13:48
18m
Talk
Snapshottable StoresDistinguished Paper
ICFP Papers and Events
Clément Allain Inria, Basile Clément OCamlPro, Alexandre Moine Inria, Gabriel Scherer Université Paris Cité - Inria - CNRS
DOI
14:06
18m
Talk
Almost-Sure Termination by Guarded Refinement
ICFP Papers and Events
Simon Oddershede Gregersen New York University, Alejandro Aguirre Aarhus University, Philipp G. Haselwarter Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University
DOI Pre-print
14:24
18m
Talk
Refinement Composition Logic
ICFP Papers and Events
Youngju Song MPI-SWS, Dongjae Lee Seoul National University
DOI
14:42
18m
Talk
Specification and Verification for Unrestricted Algebraic Effects and Handling
ICFP Papers and Events
Yahui Song National University of Singapore, Darius Foo National University of Singapore, Wei-Ngan Chin National University of Singapore
DOI Pre-print
15:00 - 15:30
Coffee breakCatering at Catering Area
15:30 - 16:42
Verification and Cost AnalysisJFP First Papers / ICFP Papers and Events at Green 1-2-3
Chair(s): Clément Pit-Claudel EPFL
15:30
18m
Talk
Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs
ICFP Papers and Events
Li-yao Xia Unaffiliated, Laura Israel Portland State University, Maite Kramarz University of Toronto, Nicholas Coltharp Portland State University, Koen Claessen Chalmers University of Technology, Stephanie Weirich University of Pennsylvania, Yao Li Portland State University
DOI Pre-print
15:48
18m
Talk
Level-p-complexity of Boolean functions using thinning, memoization, and polynomialsJFP First Paper
JFP First Papers
Julia Jansson , Patrik Jansson Chalmers University of Technology and University of Gothenbrug
DOI
16:06
18m
Talk
CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs
ICFP Papers and Events
Cole Kurashige University of California at San Diego, Ruyi Ji Peking University, Aditya Giridharan University of California at San Diego, Mark Barbone University of California at San Diego, Daniel Noor Technion, Shachar Itzhaky Technion, Ranjit Jhala University of California at San Diego, Nadia Polikarpova University of California at San Diego
DOI
16:24
18m
Talk
Contract Lenses: Reasoning about Bidirectional Programs via CalculationJFP First Paper
JFP First Papers
Hanliang Zhang University of Bristol, UK, Wenhao Tang University of Edinburgh, Ruifeng Xie Peking University, Meng Wang University of Bristol, Zhenjiang Hu Peking University
DOI
17:15 - 18:30
Business MeetingICFP Papers and Events at Green 1-2-3
Chair(s): Marco Gaboardi Boston University
17:15
15m
Other
Remembering Alan Jeffrey
ICFP Papers and Events

17:30
5m
Awards
ICFP 2014 Most Influential Paper Award
ICFP Papers and Events
Marco Gaboardi Boston University
17:35
5m
Awards
Recognition of Distinguished Papers
ICFP Papers and Events
Brigitte Pientka McGill University
17:40
5m
Talk
SRC Awards
ICFP Papers and Events
Kuen-Bang Hou (Favonia) University of Minnesota, J. Garrett Morris University of Iowa
17:45
10m
Other
The functioning of ICFP
ICFP Papers and Events
Sam Lindley University of Edinburgh
File Attached
17:55
5m
Talk
Diversity, equality, and inclusion at ICFP
ICFP Papers and Events
Alejandro Russo Chalmers University of Technology, Sweden / University of Gothenburg, Sweden / DPella AB, Sweden
18:00
10m
Other
General Chair report
ICFP Papers and Events
Marco Gaboardi Boston University
18:10
15m
Other
PC Chair's report
ICFP Papers and Events
Brigitte Pientka McGill University
18:25
5m
Other
ICFP 2025 announcement
ICFP Papers and Events
Ilya Sergey National University of Singapore
19:00 - 20:30
W@ICFP dinnerDiversity, Equity, and Inclusion

The dinner will be held at the Big School café restaurant (~7min walk from the main venue).

Thu 5 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Thursday keynoteICFP Papers and Events at Green 1-2-3
Chair(s): Neel Krishnaswami University of Cambridge
09:00
60m
Keynote
Refinement Types from Light to Deep Verification
ICFP Papers and Events
Niki Vazou IMDEA Software Institute
10:00 - 10:30
Coffee breakCatering at Catering Area
10:30 - 12:00
Refinement Types, Type InferenceICFP Papers and Events / JFP First Papers at Green 1-2-3
Chair(s): Dominic Orchard University of Kent; University of Cambridge
10:30
18m
Talk
The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data StructuresDistinguished Paper
ICFP Papers and Events
Yijia Chen Hong Kong University of Science and Technology, Lionel Parreaux HKUST (The Hong Kong University of Science and Technology)
DOI
10:48
18m
Talk
Contextual Typing
ICFP Papers and Events
Xu Xue University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI
11:06
18m
Talk
Synchronous Programming with Refinement Types
ICFP Papers and Events
Jiawei Chen University of Michigan at Ann Arbor, José Luiz Vargas de Mendonça University of Michigan at Ann Arbor, Bereket Shimels Ayele Addis Ababa Institute of Technology, Bereket Ngussie Bekele Addis Ababa Institute of Technology, Shayan Jalili University of Michigan at Ann Arbor, Pranjal Sharma University of Michigan at Ann Arbor, Nicholas Wohlfeil University of Michigan at Ann Arbor, Yicheng Zhang University of Michigan at Ann Arbor, Jean-Baptiste Jeannin University of Michigan at Ann Arbor
DOI
11:24
18m
Talk
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
ICFP Papers and Events
Satoshi Kura Waseda University, Hiroshi Unno Tohoku University
DOI File Attached
11:42
18m
Talk
Trace contractsJFP First Paper
JFP First Papers
Cameron Moy Northeastern University, Matthias Felleisen Northeastern University
DOI
12:00 - 13:30
12:00 - 13:30
13:30 - 15:00
Memory Models / Memory Management / Low-Level LanguagesICFP Papers and Events at Green 1-2-3
Chair(s): Stefan Monnier Université de Montréal
13:30
18m
Talk
Oxidizing OCaml with Modal Memory Management
ICFP Papers and Events
Anton Lorenzen University of Edinburgh, Leo White Jane Street, Stephen Dolan Jane Street, Richard A. Eisenberg Jane Street, Sam Lindley University of Edinburgh
DOI Pre-print
13:48
18m
Talk
A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer–Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction
ICFP Papers and Events
Calvin Beck University of Pennsylvania, Irene Yoon Inria, Hanxi Chen University of Pennsylvania, Yannick Zakowski Inria - ENS de Lyon - CNRS - UCBL1 - LIP - UMR 5668, Steve Zdancewic University of Pennsylvania
DOI
14:06
18m
Talk
Double-Ended Bit-Stealing for Algebraic Data Types
ICFP Papers and Events
Martin Elsman University of Copenhagen
Link to publication DOI
14:24
18m
Talk
Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl)Functional Pearl
ICFP Papers and Events
Patrick Bahr IT University of Copenhagen, Graham Hutton University of Nottingham
DOI Pre-print
14:42
18m
Talk
Sound Borrow-Checking for Rust via Symbolic Semantics
ICFP Papers and Events
Son Ho Inria, Aymeric Fromherz Inria, Jonathan Protzenko Microsoft Azure Research
DOI
15:00 - 15:30
Coffee breakCatering at Catering Area
15:30 - 17:00
Distributed Systems, ConcurrencyICFP Papers and Events / JFP First Papers at Green 1-2-3
Chair(s): Michael Sperber Active Group GmbH
15:30
18m
Talk
The Functional, the Imperative, and the Sudoku: Getting Good, Bad, and Ugly to Get Along (Functional Pearl)Functional Pearl
ICFP Papers and Events
Manuel Serrano Inria; Université Côte d’Azur, Robert Bruce Findler Northwestern University
DOI
15:48
18m
Talk
Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts
ICFP Papers and Events
Bram Vandenbogaerde Vrije Universiteit Brussel, Quentin Stiévenart Université du Québec à Montréal, Coen De Roover Vrije Universiteit Brussel
DOI Pre-print
16:06
18m
Talk
A Coq Mechanization of JavaScript Regular Expression Semantics
ICFP Papers and Events
Link to publication DOI Pre-print
16:24
18m
Talk
Alice or Bob?: Process polymorphism in choreographiesJFP First Paper
JFP First Papers
Eva Graversen University of Southern Denmark, Andrew K. Hirsch University at Buffalo, SUNY, Fabrizio Montesi University of Southern Denmark
DOI
16:42
18m
Talk
Functional Programming in Financial Markets (Experience Report)Experience Report
ICFP Papers and Events
Atze Dijkstra Standard Chartered Bank, José Pedro Magalhães Standard Chartered Bank, Pierre Néron Standard Chartered Bank
DOI Pre-print

Fri 6 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30
Welcome and KeynoteFProPer at Meeting 4
09:00
90m
Keynote
From C to Comonads to Climate: A Functional Programmer's Journey in Array Programming for Good
FProPer
Dominic Orchard University of Kent; University of Cambridge
09:00 - 10:30
Tutorial: Aeneas, a framework to verify safe Rust programs (part 1)ICFP Tutorials at Meeting 5
09:00
90m
Tutorial
Aeneas, a framework to verify safe Rust programs
ICFP Tutorials
Son Ho Inria
09:00 - 10:30
TyDe KeynoteTyDe at Orange 1

Session chair: Jesper Cockx

09:00
5m
Day opening
Welcome to TyDe
TyDe

09:05
80m
Keynote
Types for correctness, convenience, and performance
TyDe
Gabriele Keller Utrecht University
09:00 - 10:30
Haskell: Keynote 1Haskell at Orange 3
Chair(s): J. Garrett Morris University of Iowa
09:00
5m
Talk
Welcome
Haskell
J. Garrett Morris University of Iowa
09:05
70m
Keynote
Fabricating Functional Formalisms for Fun
Haskell
Brent Yorgey Hendrix College
09:30 - 10:30
FUNARCH KeynoteFUNARCH at Meeting 6
Chair(s): Michael Sperber Active Group GmbH
09:30
60m
Keynote
Architecting Functional Programs
FUNARCH
09:30 - 10:30
Session 1ML at Orange 2
Chair(s): David Allsopp Tarides
09:30
30m
Talk
Designing interrupts for ML and OCaml
ML
Guillaume Munch-Maccagnoni INRIA, Leo White Jane Street, Stephen Dolan Jane Street
10:00
30m
Talk
Fram: Named Parameters Pushed to the Limit
ML
Patrycja Balik University of Wrocław, Piotr Polesiuk University of Wrocław
Media Attached
10:30 - 11:00
Coffee breakCatering at Catering Area
11:00 - 12:30
Session 2miniKanren at Meeting 3
11:00
30m
Talk
Relational Reactive Programming: miniKanren for the Webremote
miniKanren
S: Evan Donahue University of Tokyo
11:30
30m
Talk
To Be or Not To Be: Adding Integrity Constraints to stableKanren to Make a Decisionin-person
miniKanren
S: Xiangyu Guo Arizona State University, Ajay Bansal Arizona State University
12:00
30m
Talk
Six Ways to Implement Divisibility by Three in miniKanrenin-person
miniKanren
Brett Schreiber None, S: Brysen Pfingsten Seton Hall University, Jason Hemann Seton Hall University
Pre-print
11:00 - 12:30
Algebraic Data Types and PerformanceFProPer at Meeting 4
11:00
45m
Talk
Tail Modulo Async/Await
FProPer
Vivien GACHET LIP, Lyon, France, Gabriel Radanne Inria, Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP
File Attached
11:45
45m
Talk
Ribbit with Memory Morphisms
FProPer
Thaïs Baudon ENS de Lyon & LIP, Gabriel Radanne Inria, Laure Gonnord Université Grenoble-Alpes - Grenoble INP - LCIS
Pre-print Media Attached File Attached
11:00 - 12:30
Tutorial: Aeneas, a framework to verify safe Rust programs (part 2)ICFP Tutorials at Meeting 5
11:00
90m
Tutorial
Aeneas, a framework to verify safe Rust programs
ICFP Tutorials
Son Ho Inria
11:00 - 12:30
FUNARCH Talks #1FUNARCH at Meeting 6
Chair(s): Perdita Stevens University of Edinburgh
11:00
45m
Research paper
F3: A Compiler For Feature Engineering
FUNARCH
Weixi Ma Meta, Arnaud Venet Facebook, Junhua Gu Meta, Subbu Subramanian Meta, Siyu Wang Meta, Rocky Liu Meta, Daniel Friedman Indiana University, Yafei Yang
11:45
45m
Experience report
Design and implementation of a verified interpreter for additive manufacturing programs
FUNARCH
Matthew Sottle Lawrence Livermore National Laboratory, Mohit Tekriwal Lawrence Livermore National Laboratory
11:00 - 12:30
Usability, testing and static analysisTyDe at Orange 1

Session chair: Patrik Jansson

11:00
22m
Talk
A Type- And Control- Flow Analysis for System FC (Extended Abstract)
TyDe
Skye Soss University of Chicago, John Reppy University of Chicago, USA
File Attached
11:22
22m
Talk
Dependent Types to Push Corners of the Property-based Testing (Extended Abstract)
TyDe
Denis Buzdalov Institute for System Programming of RAS
File Attached
11:45
22m
Talk
How Novices Perceive Interactive Theorem Provers (Extended Abstract)
TyDe
Sára Juhošová Delft University of Technology
File Attached
12:07
22m
Talk
Type-level Property Based Testing
TyDe
Thomas Ekström Hansen University of St Andrews, Edwin Brady University of St Andrews, UK
11:00 - 12:30
Haskell 1Haskell at Orange 3
Chair(s): Niki Vazou IMDEA Software Institute
11:00
30m
Talk
Haskelite: A Tracing Interpreter Based on a Pattern-Matching Calculus
Haskell
Pedro Vasconcelos University of Porto, Rodrigo Marques Universidade do Porto
11:30
30m
Talk
Liquid Amortization - Proving amortized complexity with LiquidHaskell (Functional Pearl)
Haskell
Jan van Brügge Heriot-Watt University
12:00
30m
Talk
Making a Curry Interpreter using Effects and Handlers
Haskell
Niels Bunkenburg University of Kiel, Germany, Nicolas Wu Imperial College London
12:30 - 14:00
14:00 - 15:30
Performance and OptimisationFProPer at Meeting 4
14:00
45m
Talk
A comparison of OpenCL, CUDA, and HIP as compilation targets for a functional array language
FProPer
Troels Henriksen University of Copenhagen
14:45
45m
Talk
Fusing Gathers with Integer Linear Programming
FProPer
David van Balen , Gabriele Keller Utrecht University, Trevor L. McDonell Utrecht University, Ivo Gabe de Wolff Utrecht University
14:00 - 15:30
Tutorial: Aeneas, a framework to verify safe Rust programs (repetition of part 1)ICFP Tutorials at Meeting 5
14:00
90m
Tutorial
Aeneas, a framework to verify safe Rust programs
ICFP Tutorials
Son Ho Inria
14:00 - 15:30
FUNARCH Talks #2FUNARCH at Meeting 6
Chair(s): Michael Sperber Active Group GmbH
14:00
45m
Experience report
Applying Continuous Formal Methods to Cardano
FUNARCH
14:45
45m
Experience report
Continuations: what have they ever done for us?
FUNARCH
Marc Kaufman Central European University, Bogdan Popa
14:00 - 15:30
Dependent typesTyDe at Orange 1

Session chair: Jesper Cockx

14:00
22m
Talk
Modal Mu-Calculus for Free in Agda
TyDe
Ivan Todorov Delft University of Technology, Casper Bach Poulsen Delft University of Technology
14:22
22m
Talk
First-class Algebraic Presentations with Elaborator Reflection (Extended Abstract)
TyDe
Robert Wright University of Edinburgh, Ohad Kammar University of Edinburgh
File Attached
14:45
22m
Talk
Normalizable types
TyDe
Stefan Monnier Université de Montréal
15:07
22m
Talk
Intrinsically Typed Syntax, a Logical Relation, and the Scourge of the Transfer Lemma
TyDe
Hannes Saffrich University of Freiburg, Peter Thiemann University of Freiburg, Germany, Marius Weidner University of Freiburg
14:00 - 15:30
Haskell: Keynote 2Haskell at Orange 3
Chair(s): J. Garrett Morris University of Iowa
14:00
70m
Keynote
State of GHC
Haskell
Simon Peyton Jones Epic Games
File Attached
15:30 - 16:00
Coffee breakCatering at Catering Area
16:00 - 17:30
Session 4miniKanren at Meeting 3
16:00
30m
Talk
Improving stableKanren’s Backward Compatibilityin-person
miniKanren
S: Xiangyu Guo Arizona State University, Ajay Bansal Arizona State University
16:30
30m
Talk
A Relational Solver for Constraint-based Type Inferenceremote
miniKanren
Dmitri Boulytchev Saint Petersburg State University, S: Eridan Domoratskiy ITMO University
16:00 - 17:30
Compilation TechniquesFProPer at Meeting 4
16:00
45m
Talk
Functional Sparse Tensor Compilation
FProPer
Shideh Hashemian University of Edinburgh, Amir Shaikhha University of Edinburgh
16:45
45m
Talk
HVM2: Iteraction Combinator Evaluator
FProPer
Victor Taelin Higher Order Company, Francisco Javier Grecco Carman , Nicolas Abril Higher Order Company, Enrico Zandomeni Borba Higher Order Company
16:00 - 17:30
Tutorial: Aeneas, a framework to verify safe Rust programs (repetition of part 2)ICFP Tutorials at Meeting 5
16:00
90m
Tutorial
Aeneas, a framework to verify safe Rust programs
ICFP Tutorials
Son Ho Inria
16:00 - 17:30
FUNARCH Talks #3FUNARCH at Meeting 6
Chair(s): Perdita Stevens University of Edinburgh
16:00
45m
Experience report
Bidirectional Data Transformations
FUNARCH
Marcus Crestani Active Group GmbH, Markus Schlegel Active Group GmbH, Marco Schneider Active Group GmbH
16:45
45m
Panel
Future of FUNARCH
FUNARCH
Michael Sperber Active Group GmbH
16:00 - 17:30
Compilers and toolingTyDe at Orange 1

Session chair: Sandra Alves

16:00
22m
Talk
Typed, Concise, Nanopass (pick 3) (Extended Abstract)
TyDe
Lawrence Chonavel Utrecht University
File Attached
16:22
22m
Talk
Term Search in Rust
TyDe
Philipp Joram Tallinn University of Technology, Tavo Annus Tallinn University of Technology
16:45
22m
Talk
Towards Type-Directed API Search for Mainstream Languages
TyDe
Marc Etter OST Eastern Switzerland University of Applied Sciences, Farhad Mehta OST Eastern Switzerland University of Applied Sciences
17:07
22m
Meeting
TyDe closing
TyDe

16:00 - 17:30
Session 4ML at Orange 2
Chair(s): Jesse Tov Jane Street Europe
16:00
30m
Talk
Labeled Tuples (Informed Position)
ML
Chris Casinghino Jane Street, Ryan Tjoa University of Washington
16:30
30m
Talk
Wasm_of_ocaml
ML
16:00 - 17:30
Haskell 2Haskell at Orange 3
Chair(s): J. Garrett Morris University of Iowa
16:00
30m
Talk
Controlling Computation Granularity through Fusion in Improving Floating-Point Numbers
Haskell
Momoka Saito The University of Electro-Communications, Hideya Iwasaki Meiji University, Hideyuki Kawabata Hiroshima City University, Tsuneyasu Komiya The University of Electro-Communications
16:30
20m
Talk
[HIW] Thrive with HEAD - How to adopt innovation from GHC HEAD timely in industrial scale
Haskell
Ian-Woo Kim Mercury Technologies, Inc
16:50
40m
Talk
Lightning talks I
Haskell

Sat 7 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30
Tutorial part 1ICFP Tutorials at Meeting 5
09:00
90m
Tutorial
Teaching functional programming
ICFP Tutorials
Michael Sperber Active Group GmbH
09:00 - 10:30
OCaml compiler features and optimizationsOCaml at Orange 2
Chair(s): Stephen Dolan Jane Street

Live stream: https://www.youtube.com/watch?v=OuQqblCxJ2Y

09:00
22m
Talk
On the design and implementation of Modular Explicitsin-person
OCaml
Samuel Vivien INRIA & École Normale Supérieure | Université PSL, Didier Rémy Inria
File Attached
09:22
22m
Talk
Flambda2 Validatorin-person
OCaml
Irene Yoon Inria, Chris Casinghino Jane Street
File Attached
09:45
22m
Talk
A Non-allocating Optionin-person
OCaml
File Attached
10:07
22m
Talk
Mixed Blocks: Storing More Fields Flatin-person
OCaml
Nicholas Roberts Jane Street
File Attached
09:00 - 10:30
Haskell 3Haskell at Orange 3
Chair(s): Paul Downen University of Massachusetts at Lowell
09:00
30m
Talk
MicroHs - A Small Compiler for Haskell
Haskell
Lennart Augustsson Epic Games
09:30
30m
Talk
Higher Order Patterns for Rewrite Rules
Haskell
Jaro Reinders Delft University of Technology
DOI File Attached
10:00
30m
Talk
Welcome to the Parti(tioning) (Functional Pearl)
Haskell
Robert Krook Chalmers University of Technology, Sweden, Samuel Hammersberg Gothenburg University
10:30 - 11:00
Coffee breakCatering at Catering Area
11:00 - 12:30
Session 2Scheme at Meeting 4
11:00
30m
Talk
A Teaching Language for Specification
Scheme
Cameron Moy Northeastern University
11:30
30m
Talk
Beyond SICP - Design and Implementation of a Notional Machine for Scheme
Scheme
Kyriel Abad National University of Singapore, Martin Henz National University of Singapore
File Attached
12:00
30m
Talk
Nocksche and Nocko
Scheme
11:00 - 12:30
Tutorial part 2ICFP Tutorials at Meeting 5
11:00
90m
Tutorial
Teaching functional programming
ICFP Tutorials
Michael Sperber Active Group GmbH
11:00 - 12:30
Haskell 4Haskell at Orange 3
Chair(s): Michael D. Adams National University of Singapore
11:00
22m
Talk
[HIW] Analysing the heap of uninstrumented Haskell programs using ghc-debug
Haskell
Zubin Duggal Well-Typed LLP
11:22
22m
Talk
[HIW] A zero-copy interface to compact regions powered by destinations
Haskell
Thomas BAGREL Tweag, LORIA/INRIA
11:45
22m
Talk
[HIW] Building Haskell with Buck2
Haskell
Andreas Herrmann Tweag by Modus Create
12:07
22m
Talk
[HIW] The JavaScript FFI feature in GHC Wasm backend
Haskell
Cheng Shao Modus Create
12:30 - 14:00
14:00 - 15:30
Session 3Scheme at Meeting 4
Chair(s): Robert Bruce Findler Northwestern University
14:00
90m
Tutorial
Tutorial on Program Transformations
Scheme
Jason Hemann Seton Hall University
14:00 - 15:30
Tutorial part 3ICFP Tutorials at Meeting 5
14:00
90m
Tutorial
Teaching functional programming
ICFP Tutorials
Michael Sperber Active Group GmbH
14:00 - 15:30
Haskell 5Haskell at Orange 3
Chair(s): Simon Marlow Meta
14:00
30m
Talk
Calculating Compilers Effectively
Haskell
Zac Garby University of Nottingham, Graham Hutton University of Nottingham, Patrick Bahr IT University of Copenhagen
14:30
30m
Talk
Cloaca: A Concurrent Hardware Garbage Collector for Non-Strict Functional Languages
Haskell
Craig Ramsay Heriot-Watt University, Rob Stewart Heriot-Watt University
15:00
30m
Talk
Functional Reactive Programming, Rearranged
Haskell
Finnbar Keating University of Warwick, Michael Gale GitHub
15:30 - 16:00
Coffee breakCatering at Catering Area
16:00 - 17:30
Session 4Scheme at Meeting 4
Chair(s): Kristopher Micinski Syracuse University
16:00
60m
Talk
Challenges in the Design and Implementation of Teaching Languages for EDSLs
Scheme
Jason Hemann Seton Hall University
16:00 - 17:30
Tutorial part 4ICFP Tutorials at Meeting 5
16:00
90m
Tutorial
Teaching functional programming
ICFP Tutorials
Michael Sperber Active Group GmbH
16:00 - 17:30
Lightning talks / Chairs' reportHaskell at Orange 3
Chair(s): J. Garrett Morris University of Iowa
16:00
90m
Talk
Lightning talks II / Chairs' report / Future of HS discussion
Haskell
J. Garrett Morris University of Iowa, Niki Vazou IMDEA Software Institute