A theorem prover for Boolean BI. - Jonghyun Park; Jeongbong Seo; Sungwoo Park (POPL, 2013)

Judgmental subtyping systems with intersection types and modal types. - Jeongbong Seo; Sungwoo Park (Acta Informatica, 2013)

Mechanizing Metatheory Without Typing Contexts. - Jonghyun Park; Jeongbong Seo; Sungwoo Park; Gyesik Lee (J. Autom. Reason., 2014)