Ki Yung Ahn

Education

• Ph.D. Portland State University (2005 — 2015)
• B.S. Korea Advanced Institute of Science and Technology (1998 — 2002)
• Bachelor's degree Korea Advanced Institute of Science and Technology (1998 — 2002)

Research Interests

• Security protocol verification using process calcului,
• Executable relational specifications of polymorphic type systems using logic programming,
• Language design to support both convenient programming and logically consistent reasoning via the Curry–Howard correspondence,
• Extending the Hindley–Milner (HM) type inference for languages with Mendler-style recursion schemes and GADTs with true term indices, and
• Interfacing with solvers (e.g., SAT, SMT) in automated testing/verification frameworks.

Awards

• Best Paper Award [4] at CONCUR 2017
• Bronze Medal in the ACM Student Research Competition (SRC) at ICFP 2012

Publications

• Ross Horne, Ki Yung Ahn, Shang-Wei Lin, and Alwen Tiu. Quasi-open bisimilarity with mismatch is intuitionistic. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 26–35, 2018.
• Ki Yung Ahn. Mechanized proof for type preservation of gtlc. Journal of KIISE, 46(5):457–468, May 2019. ISSN 2383-630X.
• Ki Yung Ahn. Experience report: using Jupyter notebook for CS theory education. Communications of KIISE, 37(3), March 2019. ISSN 1015-9908. (in Korean).
• Ki Yung Ahn, Ross Horne, and Alwen Tiu. A characterisation of open bisimulation using an intuitionistic modal logic. In CONCUR ’17, volume 85 of LIPIcs, pages 7:1–7:17, September 2017.
• Ki Yung Ahn, Tim Sheard, Marcelo Fiore, and Andrew M. Pitts. System Fi : a higherorder polymorphic λ-calculus with erasable term indices. In Proceedings of the 11th international conference on Typed Lambda Calculi and Applications. TLCA ’13, volume 7941 of LNCS. Springer, 2013.
• Ki Yung Ahn and Ewen Denney. A framework for testing first-order logic axioms in program verification. Software Quality Journal, 21(1):159–200, March 2013. ISSN 0963- 9314.
• Ki Yung Ahn and Ewen Denney. Testing first-order logic axioms in program verification. In Proceedings of the 4th international conference on Tests and Proofs, TAP’10, pages 22–37. Springer-Verlag, 2010. ISBN 3-642-13976-0, 978-3-642-13976-5.
• Ki Yung Ahn and Tim Sheard. A hierarchy of mendler style recursion combinators: taming inductive datatypes with negative occurrences. In Proceedings of the 16th ACM SIGPLAN international conference on Functional programming, ICFP ’11, pages 234–246, New York, NY, USA, 2011. ACM. ISBN 978-1-4503-0865-6.
• Ki Yung Ahn and Tim Sheard. Shared subtypes: subtyping recursive parametrized algebraic data types. In Proceedings of the first ACM SIGPLAN symposium on Haskell, Haskell ’08, pages 75–86, New York, NY, USA, 2008. ACM. ISBN 978-1-60558-064-7.