ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore

This program is tentative and subject to change.

Sun 12 Oct 2025 14:00 - 14:30 at Seminar Room 2 - Session 2

Data engineers increasingly use domain-specific languages (DSLs) to generate the code for data pipelines. Such DSLs are often embedded in Python. Unfortunately, there are challenges in debugging the generation of data pipelines: an error in a Python DSL script is often detected too late, after the execution of the script, and the source code location that triggers the error is hard to pinpoint.

In this paper, we focus on the scenario where a DSL embedded in Python (so it is dynamically-typed) generates data pipeline description code that is statically-typed. We propose gradual metaprogramming to (1) provide a migration path toward statically typed DSLs, (2) immediately provide earlier detection of code generation type errors, and (3) report the source code location responsible for the type error. Gradual metaprogramming accomplishes this by type checking code fragments and incrementally performing runtime checks as they are spliced together. We define MetaGTLC, a metaprogramming calculus in which a gradually-typed metalanguage manipulates a statically-typed object language, and give semantics to it by translation to the cast calculus MetaCC. We prove that successful metaevaluation always generates a well-typed object program and mechanize the proof in Agda.

This program is tentative and subject to change.

Sun 12 Oct

Displayed time zone: Perth change

14:00 - 15:30
Session 2TyDe at Seminar Room 2
14:00
30m
Talk
Gradual Metaprogramming
TyDe
Tianyu Chen Indiana University, Darshal Shetty Indiana University, Jeremy G. Siek Indiana University, USA, Chao-Hong Chen Meta, Weixi Ma Meta, Arnaud Venet Meta, Rocky Liu Meta
Link to publication DOI Pre-print
14:30
30m
Talk
Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search
TyDe
Satoshi Takimoto Institute of Science Tokyo, Sosuke Moriguchi Institute of Science Tokyo, Takuo Watanabe Institute of Science Tokyo
DOI
15:00
30m
Talk
Generating a corpus of Hazel programs from ill-typed OCaml programs (Extended Abstract)
TyDe
Patrick Ferris University of Cambridge, UK, Anil Madhavapeddy University of Cambridge, UK