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
Junyoung JangSophia RoshalFrank Pfenningand Brigitte Pientka. (2024). Adjoint Natural Deduction. In Formal Structures for Computation and Deduction (FSCD 24). https://doi.org/10.4230/LIPIcs.FSCD.2024.15
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 Junyoung JangSophia RoshalFrank Pfenningand Brigitte Pientka. (2024). Adjoint Natural Deduction (Extended Version). In arXiv. https://doi.org/10.48550/arXiv.2402.01428
2021
Hanwen ZhuJunyoung Jangand Xujie Si. (2021). XCheck: a Simple, Effective and Extensible Bug Finder using micro-grammar. In arXiv. https://doi.org/10.48550/arXiv.2112.08010Junyoung 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