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 The University of Hong Kong, 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