Harpoon: Mechanizing Metatheory Interactively - (System Description). - Jacob Errington; Junyoung Jang 001; Brigitte Pientka (CADE, 2021)

Moebius: Metaprogramming using Contextual Types - The stage where System F can pattern match on itself (Long Version). - Junyoung Jang 001; Samuel Gélineau; Stefan Monnier; Brigitte Pientka (CoRR, 2021)

XCheck: a Simple, Effective and Extensible Bug Finder using micro-grammar. - Hanwen Zhu; Junyoung Jang 001; Xujie Si (CoRR, 2021)

Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itself. - Junyoung Jang 001; Samuel Gélineau; Stefan Monnier; Brigitte Pientka (Proc. ACM Program. Lang., 2022)

Normalization by evaluation for modal dependent type theory. - Jason Z. S. Hu; Junyoung Jang 001; Brigitte Pientka (J. Funct. Program., 2023)

Adjoint Natural Deduction. - Junyoung Jang 001; Sophia Roshal; Frank Pfenning; Brigitte Pientka (FSCD, 2024)

Adjoint Natural Deduction (Extended Version). - Junyoung Jang 001; Sophia Roshal; Frank Pfenning; Brigitte Pientka (CoRR, 2024)

Polymorphic Metaprogramming with Memory Management - An Adjoint Analysis of Metaprogramming. - Junyoung Jang 001; Brigitte Pientka (CoRR, 2024)

Formally Verified Cloud-Scale Authorization. - Aleks Chakarov; Jaco Geldenhuys; Matthew Heck; Michael Hicks 001; Sam Huang; Georges-Axel Jaloyan; Anjali Joshi; K. Rustan M. Leino; Mikael Mayer; Sean McLaughlin; Akhilesh Mritunjai; Clément Pit-Claudel; et al. (ICSE, 2025)