Shared subtypes: subtyping recursive parametrized algebraic data types. - Ki Yung Ahn; Tim Sheard (Haskell, 2008)

Testing First-Order Logic Axioms in Program Verification. - Ki Yung Ahn; Ewen Denney (TAP@TOOLS, 2010)

A hierarchy of mendler style recursion combinators: taming inductive datatypes with negative occurrences. - Ki Yung Ahn; Tim Sheard (ICFP, 2011)

Equational reasoning about programs with general recursion and call-by-value semantics. - Garrin Kimmell; Aaron Stump; Harley D. Eades III; Peng Fu 001; Tim Sheard; Stephanie Weirich; Chris Casinghino; Vilhelm Sjöberg; Nathan Collins; Ki Yung Ahn (PLPV, 2012)

Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems - Vilhelm Sjöberg; Chris Casinghino; Ki Yung Ahn; Nathan Collins; Harley D. Eades III; Peng Fu 001; Garrin Kimmell; Tim Sheard; Aaron Stump; Stephanie Weirich (MSFP, 2012)

System F i . - Ki Yung Ahn; Tim Sheard; Marcelo P. Fiore; Andrew M. Pitts (TLCA, 2013)

A framework for testing first-order logic axioms in program verification. - Ki Yung Ahn; Ewen Denney (Softw. Qual. J., 2013)

Executable Relational Specifications of Polymorphic Type Systems Using Prolog. - Ki Yung Ahn; Andrea Vezzosi (FLOPS, 2016)

An Executable Specification of Typing Rules for Extensible Records based on Row Polymorphism. - Ki Yung Ahn (CoRR, 2017)

A Characterisation of Open Bisimulation using an Intuitionistic Modal Logic. - Ki Yung Ahn; Ross Horne; Alwen Tiu (CoRR, 2017)

Generating Witness of Non-Bisimilarity for the pi-Calculus. - Ki Yung Ahn; Ross Horne; Alwen Tiu (CoRR, 2017)

Quasi-Open Bisimilarity with Mismatch is Intuitionistic. - Ross Horne; Ki Yung Ahn; Shang-Wei Lin 001; Alwen Tiu (LICS, 2018)

A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic. - Ki Yung Ahn; Ross Horne; Alwen Tiu (Log. Methods Comput. Sci., 2021)