Typed Meta-Programming with Splice Variables
- 講者江宗儒 先生 (加拿大多倫多大學)
邀請人：陳亮廷 - 時間2025-03-12 (Wed.) 10:30 ~ 12:30
- 地點資訊所新館101演講廳
摘要
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.