POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
Thu 23 Jan 2025 15:00 - 15:20 at Marco Polo - Types 1 Chair(s): Stephanie Weirich

In this paper, we introduce DeLaM, a dependent layered modal type theory which enables meta-programming in Martin-Löf type theory (MLTT) with recursion principles on open code. DeLaM includes three layers: the layer of static syntax objects of MLTT without any computation; the layer of pure MLTT with the computational behaviors; the meta-programming layer extends MLTT with support for quoting an open MLTT code object and composing and analyzing open code using recursion. We can also execute a code object at the meta-programming layer. The expressive power strictly increases as we move up in a given layer. In particular, while code objects only describe static syntax, we allow computation at the MLTT and meta-programming layer. As a result, DeLaM provides a dependently typed foundation for meta-programming that supports both type-safe code generation and code analysis. We prove the weak normalization of DeLaM and the decidability of convertibility using Kripke logical relations.

Thu 23 Jan

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

15:00 - 16:20
Types 1POPL at Marco Polo
Chair(s): Stephanie Weirich University of Pennsylvania
15:00
20m
Talk
A Dependent Type Theory for Meta-programming with Intensional Analysis
POPL
Jason Z.S. Hu Amazon Web Services, USA, Brigitte Pientka McGill University
15:20
20m
Talk
Avoiding signature avoidance in ML modules with zippers
POPL
15:40
20m
Talk
Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
POPL
Shengyi Jiang , Chen Cui University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
16:00
20m
Talk
Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs
POPL
Taro Sekiyama National Institute of Informatics; SOKENDAI, Hiroshi Unno Tohoku University