TyDe 2024
Fri 6 - Sat 7 September 2024 Milan, Italy
co-located with ICFP 2024
VenueAllianz MiCo (Milano Convention Centre)
Room nameGreen 1-2-3
Floor-1
Capacity350
Room InformationNo extra information available
Program

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

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
Link to publication Pre-print File Attached
10:30 - 12:00
Algebraic and Computational EffectsICFP Papers and Events / ICFP 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, Laure Gonnord Université Grenoble-Alpes - Grenoble INP - LCIS
DOI Pre-print
11:24
18m
Talk
Algebraic effects and handlers for arrowsJFP First Paper
ICFP 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
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 / ICFP 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
ICFP 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
ICFP JFP First Papers
Chenghao Su Nanjing University, Lin Chen Nanjing University, Yanhui Li Nanjing University, Yuming Zhou Nanjing University
DOI
15:30 - 17:00
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
ICFP 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

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:30 - 12:00
Meta-Programming, Staging, Generic Programming, Partial EvaluationICFP Papers and Events / ICFP 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
ICFP JFP First Papers
Cameron Moy Northeastern University
DOI
13:00 - 13:30
13:00
30m
Talk
SRC Presentations
ICFP 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:30 - 16:42
Verification and Cost AnalysisICFP JFP 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
ICFP 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
ICFP 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

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:30 - 12:00
Refinement Types, Type InferenceICFP Papers and Events / ICFP 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
ICFP JFP First Papers
Cameron Moy Northeastern University, Matthias Felleisen Northeastern University
DOI
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, 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:30 - 17:00
Distributed Systems, ConcurrencyICFP Papers and Events / ICFP 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
ICFP 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

Tue 3 Sep

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Green 1-2-3

Wed 4 Sep

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:00153045
Green 1-2-3

Thu 5 Sep

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Green 1-2-3