Publications

Journal Publications

2025

Junyoung JangAntoine GaulinJason Z. S. Huand Brigitte Pientka. (2025). McTT: A Verified Kernel for a Proof Assistant. In Proceedings of the ACM on Programming Languages, Volume 9, Issue ICFP. https://doi.org/10.1145/3747511

2023

Jason Z. S. HuJunyoung Jangand Brigitte Pientka. (2023). Normalization by Evaluation for Modal Dependent Type Theory. In Journal of Functional Programming (JFP) 33, E7. https://doi.org/10.1017/S0956796823000060

2022

Junyoung JangSamuel GélineauStefan Monnierand Brigitte Pientka. (2022). Mœbius: Metaprogramming Using Contextual Types: The Stage where System F can Pattern Match on Itself. In Proceedings of the ACM on Programming Languages, Volume 6, Issue POPL. https://doi.org/10.1145/3498700

Conference Proceedings

2025

Aleks ChakarovJaco GeldenhuysMatthew HeckMichael HicksSam HuangGeorges-Axel JaloyanAnjali JoshiK. Rustan M. LeinoMikael MayerSean McLaughlinAkhilesh MritunjaiClement Pit-ClaudelSorawee PorncharoenwaseFlorian RabeMarianna RapoportGiles RegerCody RouxNeha RungtaRobin SalkeldMatthias SchlaipferDaniel SchoepeJohanna SchwartzentruberSerdar TasiranAaron TombEmina TorlakJean-Baptiste TristanLucas WagnerMichael WhalenRemy WillemsTongtong XiangTaejoon ByunJoshua CohenRuijie FangJunyoung JangJakob RathHira Taqdees SyedaDominik Wagnerand Yongwei Yuan. (2025). Formally Verified Cloud-Scale Authorization. In International Conference on Software Engineering (ICSE 25). https://doi.org/10.1109/ICSE55347.2025.00166. Note: Amazon authors and external authors are separately sorted lexicographically on their last names.

2024

2021

Jacob ErringtonJunyoung Jangand Brigitte Pientka. (2021). Harpoon: Mechanizing Metatheory Interactively (System Description). In André PlatzerGeoff Sutcliffe(Eds.), Automated Deduction - CADE 28. https://doi.org/10.1007/978-3-030-79876-5_38

Other Manuscripts

2024

Junyoung JangBrigitte Pientka. (2024). Polymorphic Metaprogramming with Memory Management - An Adjoint Analysis of Metaprogramming. In arXiv. https://doi.org/10.48550/arXiv.2411.00752

2021

Junyoung JangSamuel GélineauStefan Monnierand Brigitte Pientka. (2021). Moebius: Metaprogramming using Contextual Types - The stage where System F can pattern match on itself (Long Version). In arXiv. https://doi.org/10.48550/arXiv.2111.08099