Ki Yung Ahn
Assistant Professor, Computer Engineering at Hannam University, Daejeon, Korea
Links
Biography
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.
Read about executive education
Other experts
Popular Courses
Leading People and Teams
ESMT
Berlin, Germany
Nov 19
The Positive Leader: Deep Change and Organizational Transformation
Stephen M. Ross School of Business
Ann Arbor, Michigan, United States
Dec 1
Private Equity: Investing and Creating Value
The Wharton School
Philadelphia, Pennsylvania, United States
Feb 2, 2025
Looking for an expert?
Contact us and we'll find the best option for you.