일시: 2025. 12. 23. (화요일), 오후 2시~ 오후 3시

장소: 제1공학관 A685호

Speaker: Junyoung Jang (Ph.D. Student at McGill University)

Title: Metaprogramming and Polymorphism - Towards a Foundation of Practical Metaprogramming

Abstract:

Metaprogramming—the practice of generating and manipulating programs—is ubiquitous in modern software development, appearing in preprocessors, compilers, boilerplate-reduction libraries, and domain-specific languages. However, metaprogramming suffers from a critical issue: it is difficult to ensure the safety of metaprograms through testing. As an alternative solution for safety checking, type systems for metaprogramming have been developed. Lambda Box, MetaML, MetaOCaml, and Typed Template Haskell are a few examples of such systems. Can these type systems capture practical metaprogramming? For practical metaprogramming, three features are essential: polymorphism, open code generation (i.e., generating code that refers to variables not yet bound), and pattern matching or case analysis on code structures. These features enable modular generation and optimization of code fragments in real-world applications. However, existing type systems do not support all of these features, creating challenges in real-world use. In this talk, I will introduce Moebius, a system that supports type-safe metaprogramming with all these features, illustrated with simple examples of code generation.

Bio:

Junyoung Jang is a Ph.D. candidate in Computer Science at McGill University. His research focuses on programming languages, type theory, and formal verification, with an emphasis on proof assistants, contextual and dependent type systems, and mechanically verified foundations. He has published in top-tier venues including POPL, ICFP, and FSCD, and has served on the Artifact Evaluation Committees of POPL and OOPSLA, as well as an external reviewer for FSCD. He was formerly an administrator of the Haskell Language Server.