I'm a postdoctoral associate (since Aug. 2012) at MIT (CSAIL) working with Adam Chlipala. I've been experimenting with Adam's Bedrock verified programming library for the Coq theorem prover. (Here's some Bedrock examples.) I received PhD in Computer Science at the University of Iowa (July, 2012), under the advisory of Aaron Stump. I studied at Washington University in St. Louis before transferring to U. of Iowa. I earned B.Sc in Computer Science at Yonsei University in 2006. I'm interested in software/hardware verification and the field of computational logic and programming language theories. I've been using tools based on dependent types to formalize and verify proofs and software. I've developed a proof-generating SAT/SMT solver, clsat. Recently, I've released the first completed version (0.6) of a statically verified modern SAT solver called versat. I'm also working on an efficient verified RUP proof checker, called vercheck.I like this idea of formal techniques, "All the properties of theories and systems should be machine checked" (just the idea, not that it is always possible.). That is the computer science reincarnation of Russell's logicism - "All mathematical truths are logical truths". I'm looking forward to bringing formal techniques to both theoretical computer science and practical software development. C.V. (updated on 9/13, 2012) |