Typed Meta-Programming with Splice Variables
- LecturerMr. Tsung-Ju Chiang (University of Toronto, Canada)
Host: Liang-Ting Chen - Time2025-03-12 (Wed.) 10:30 ~ 12:30
- LocationAuditorium 101 at IIS new Building
Abstract
Typed meta-programming catches meta-programming errors early by checking them at definition time. This paper introduces 𝜆○▷, a typed meta-programming language that uses nested context design and temporal-style staging to track binding times and variable dependencies. The system supports a range of meta-programming idioms, including explicit splice definitions, unhygienic macros and analytic macros. We formalize the language in Agda, prove its safety propertes, define a denotational semantics to clarify the meaning of its types, and show its soundness and completeness with respect to constructive linear-time temporal logic through type- preserving translations. We compare our approach to contextual modal type theory-based systems, providing insights into their similarities and differences.