View on GitHub

Ahn, Ki Yung

안기영 (安基榮)

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

Research Fellow (Office: cubicle RF2, Cyber Security Lab (CSL), NF4)
School of Computer Scinece and Engineering (SCSE)
Nanyang Techological University

Teaching

2016 Spring @ Korea University Sejong Campus

Research

TIPER

My primary reserach focus is currently on 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 (or, resume) and the list of my publications are also available on my Google Scholar profile and on my ResearchGate profile.

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