View on GitHub

Ahn, Ki Yung

안기영 (安基榮)

Download this project as a .zip file Download this project as a tar.gz file

profie image Facebook Instagram Flickr Google+ Twitter LinkedIn Logdown ResearchGate Google Scholar DBLP ORCID GitHub Hackage

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

Teaching (2019 Fall)

see more, including previous lectures


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:


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.


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 원서 표지.