ICFP 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

This program is tentative and subject to change.

Mon 13 Oct 2025 10:50 - 11:15 at Orchid Plenary Ballroom - Dependent Types

Initial semantics aims to model inductive structures and their properties, and to provide them with recursion principles respecting these properties. An ubiquitous example is the fold operator for lists.
We are concerned with initial semantics that model languages with variable binding and their substitution structure, and that provide substitution-safe recursion principles.

There are different approaches to implementing languages with variable binding depending on the choice of representation for contexts and free variables, such as unscoped syntax, or well-scoped syntax with finite or infinite contexts. Abstractly, each approach corresponds to choosing a different monoidal category to model contexts and binding, each choice yielding a different notion of "model" for the same abstract specification (or "signature").

In this work, we provide tools to compare and relate the models obtained from a signature for different choices of monoidal category. We do so by showing that initial semantics naturally has a 2-categorical structure when parametrized by the monoidal category modeling contexts. We thus can relate models obtained from different choices of monoidal categories provided the monoidal categories themselves are related.

In particular, we use our results to relate the models of the different implementation - de Bruijn vs locally nameless, finite vs infinite contexts -, and to provide a generalized recursion principle for simply-typed syntax.

This program is tentative and subject to change.

Mon 13 Oct

Displayed time zone: Perth change

10:50 - 12:05
10:50
25m
Talk
2-Functoriality of Initial Semantics, and Applications
ICFP Papers
Benedikt Ahrens Delft University of Technology, Ambroise Lafont Inria, France, Thomas Lamiaux University of Paris-Saclay, Ens Paris-Saclay
DOI
11:15
25m
Talk
Bialgebraic Reasoning on Stateful Languages
ICFP Papers
Sergey Goncharov University of Birmingham, Stefan Milius Friedrich-Alexander University Erlangen-Nürnberg, Lutz Schröder Friedrich-Alexander University Erlangen-Nürnberg, Stelios Tsampas University of Southern Denmark, Henning Urbat Friedrich-Alexander University Erlangen-Nürnberg
DOI
11:40
25m
Talk
Frex: Dependently Typed Algebraic Simplification
ICFP Papers
Guillaume Allais University of Strathclyde, Edwin Brady University of St. Andrews, Nathan Corbyn University of Oxford, Ohad Kammar University of Edinburgh, Jeremy Yallop University of Cambridge
DOI Pre-print