Assistant Professor (kya AT hnu DOT kr +82 42 629 7492)
Office: 9-07-03 (engineering bldg. 7th floor room #03)
Department of Computer Engineering
College of Engineering, Hannam University, Daejeon, Korea 34430

• Ph.D. in Computer Science at Portland State University, Dec, 2014 (advisor: Tim Sheard)
• B.S. in Computer Science, at KAIST, Feb, 2002

Teaching (2019 Fall)

• 프로그래밍언어 Programming Languages
• 컴파일러 Compilers - Service Learning course
• 프로그래밍언어론 (Grad) Programming Lanuages

see more, including previous lectures

Research

Security and Process Calculi

Joined Alwen Tiu’s research group in 2016 summer, have been working on security protocol verification based on pi-calculi. Our result in year 2017 on the modal logic for open bismulation has been presented in CONCUR 2017 and awarded as the best paper:

• Ki Yung Ahn, Ross Horne and Alwen Tiu. A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic. 28th International Conference on Concurrency Theory (CONCUR 2017). September 5-8, 2017. Berlin, Germany. Editors: Roland Meyer and Uwe Nestmann; ISBN 978-3-95977-048-4; LIPICS Volume 85; Article No. 7; pp. 7:1-7:15. Leibniz International Proceedings in Informatics. ISSN 1868-8969. DOI: 10.4230/LIPIcs.CONCUR.2017.7
  • Slides presented by Ross at CONCUR 2017.
  • An Extended Version including Abella formalization of proofs and Bedwyr test of examples.
  • A certificate of the Best Paper Award
    
  • A News Article about the award from the homepage of School of Computer Science & Engineering @ NTU.

TIPER

Another research interest of mine is developing relational specifications of polymorphic type systems that can be automatically executed as working implementations. I am planning to initiate a project called TIPER, which aims to designe and develope a tool that automatically generates Type Inference Prototyping Engines from Executable Relational specifcations. By combining the theriteical and techincal advances in the Functional Programming and the Logic Programming communities, I believe we could realize a missing peice of the language frontend construction toolset. We already have lexer/parser geneartors (e.g. Lex/Yacc) but missing static type system generators. What we lack is a tool that could automate static type system implemetations supports both type checking and type inference over polymorphic types. See the TIPER hompage for further details on this prospective project.

Nax

My thesis research was about theories and language design for a logically consistent system that is convenient for both functional programming and logical reasoning, based on the Curry–Howard correspondence. In my thesis I designed a language called Nax, proved theoretic properteis about the language by studing its underlying calclulus (which is also my conribution). I’ve also implemted a subset of Nax, which motivated the TIPER proejct mentioned previously because the added complexity makes it difficult to keep track of whether the implementation is faithful to the design written on paper.

Additional information

In addtion, I am generally intereseted on programming languages related subjects: type systems, automated testing (using solvers), formal verification, subtyping for algebraic datatypes, and other aspects of functional languages.

Further details about me are summarized in my CV (resume); most recent change of position at Hannam University not yet updated in the CV.

Korean ver. of “Programming in Haskell”

One of my favorate programming language is Haskell. So, I’ve translated Graham Hutton’s “Programming in Haskell” into Korean, first Korean print published in 2009. You can click on the book cover image to go to their homepages.

is a Korean translation of .