- Ph.D. in Computer Science at Portland State University, Dec, 2014 (advisor: Tim Sheard)
- B.S. in Computer Science, at KAIST, Feb, 2002
Security and Process Calculi
Joined Alwen Tui’s research group working on security protocols based on pi-calculi.
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.
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.
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).
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.