2025

Taejoon ByunAleks ChakarovJoshua CohenRuijie FangJaco GeldenhuysMatthew HeckMichael HicksSamuel HuangGeorges-Axel JaloyanJunyoung JangAnjali JoshiK. Rustan M. LeinoMikael MayerSean McLaughlinAkhilesh MritunjaiSorawee PorncharoenwaseFlorian RabeMarianna RapoportJakob RathGiles RegerCody RouxNeha RungtaMatthias SchlaipferDaniel SchoepeHira Taqdees SyedaSerdar TasiranAaron TombEmina TorlakDominik WagnerLucas WagnerMichael WhalenRemy WillemsTongtong XiangYongwei YuanClement Pit-ClaudelRobin SalkeldJean-Baptiste TristanJohanna Schwartzentruber. (2025). Formally Verified Cloud-Scale Authorization. In International Conference on Software Engineering (ICSE 25).

2024

Junyoung JangSophia RoshalFrank PfenningBrigitte Pientka. (2024). Adjoint Natural Deduction. In Formal Structures for Computation and Deduction (FSCD 24). https://doi.org/10.4230/LIPIcs.FSCD.2024.15

2023

Jason Z. S. HuJunyoung JangBrigitte 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 MonnierBrigitte 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

2021

Hanwen ZhuJunyoung JangXujie Si. (2021). XCheck: a Simple, Effective and Extensible Bug Finder using micro-grammar. In arXiv. https://doi.org/10.48550/arXiv.2112.08010

Junyoung JangSamuel GélineauStefan MonnierBrigitte 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

Jacob ErringtonJunyoung JangBrigitte 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