|
Joonwon Choi
Research Associate, |
I moved to MIT CSAIL
since 2014 Fall.
Research Interests
My general research interests are as follows:- Verified (Certified) software, and any techniques related to proofs.
I have been working on verifying following software.
- Static analyzers (based on abstract interpretation)
- Compilers
- Automated and scalable proofs for practical uses
- Type-theoretical structures: dependent types, type classes, and (co-)induction.
Education
-
Feb 2013, B.S. summa cum laude,
Department of Computer Science and Engineering,
Seoul National University
(Double major in Department of Mathematical Sciences) - Feb 2006, graduated from Incheon Science High School
Publications
-
Towards Scalable Translation Validation of
Static Analyzers
Jeehoon Kang, Sungkeun Cho, , Chung-Kil Hur, and Kwangkeun Yi
Planned to submit -
B.S. Thesis (Computer Science) Unstaging Translation of
Cross-Stage Persistent Multi-Staged Programs into Context Calculus
[paper] -
B.S. Thesis (Mathematics) Pushouts, Pullbacks and
Their Properties
[paper] -
Unstaging Translation of Cross-Stage Persistent
Multi-Staged Programs
, Jeehoon Kang, Daejun Park, and Kwangkeun Yi
Technical Paper
[paper] -
(Domestic/Korean) SparrowBerry: A Verified Validator for an Industrial-Strength
Static Analyzer
, Sungkeun Cho, Jeehoon Kang, and Kwangkeun Yi
In KIISE(Korean Institute of Information Scientists and Engineers) Conference 2013.
[paper] -
(Domestic/Korean) A Comparison between Two Representative Multi-Staged
Languages Lisp and MetaML
, Jeehoon Kang, Daejun Park, and Kwangkeun Yi
In KIISE(Korean Institute of Information Scientists and Engineers) Conference 2012, 39(1):437-439, 2012.
[paper]
Talks
2013
-
2013.10.11 SparrowBerry: Towards Scalable Validator.
ROPAS Weekly Show & Tell
[slides] -
2013.08.20 SparrowBerry: Technical Issues.
ROPAS Weekly Show & Tell
[not available now] -
2013.07.09 Validation and Correctness Proofs of Accessibility Information
ROPAS Weekly Show & Tell
[slides] -
2013.05.31 Proof Automation: Existing Techniques and My Idea
ROPAS Weekly Show & Tell
[slides] -
2013.03.15 A Tutorial on Coinduction and Bisimulation
ROPAS Weekly Show & Tell
[slides] -
2013.01.25 JavaScript: Features, Trends, and Static Analysis
ROPAS Weekly Show & Tell
[slides] -
2013.04.19 Formalizing Concrete and Abstract Semantics for the Access-based Localization
ROPAS Weekly Show & Tell
[slides]
2012
-
2012.12.28 Type checking between two languages with
foreign function interface
ROPAS Weekly Show & Tell
[slides] -
2012.11.09 Current progress on validator of Sparrow
ROPAS Weekly Show & Tell
[slides] -
2012.06.01 Galois Connection in Coq
ROPAS Weekly Show & Tell
[slides] -
2012.04.13 Duality in Multi-Staged Calculus
ROPAS Weekly Show & Tell
[slides] -
2012.02.24 Static Analysis of Cross-Stage Persistent
Multi-Staged Programs with translation and projection
ROPAS Weekly Show & Tell
[slides] -
2012.01.25 Translation from Multi-Staged Calculus
to Context Calculus
POPL 2012: The 39th ACM SIGPLAN Symposium on Principles of Programming Languages (lightning talk session) [slides] -
2012.01.06 Facts and Ideas about Unstaging Translation of
Language-orthodox Multi-staged Calculus
ROPAS Weekly Show & Tell
[slides]
2011
Teaching
- 2013 Fall: Programming Languages (TA)
Awards and Honors
- Feb 2013, Top Honor (summa cum laude) Certification
- Jul 2012, Best Paper Presentation Awards by KIISE (Korean Institute of Information Scienctists and Engineers)
- Mar 2006 - Feb 2013, Presidential Science Scholarship
Work Experiences
- Mar 2013 - Apr 2013, Visiting Researcher, Microsoft Research Cambridge
- Apr 2009 - Oct 2011, Software Engineer, allm Games (Skilled Industry Personnel)
- Jan 2009 - Apr 2009, Software Engineering Intern(SWE), Google Korea
- Jul 2007 - Aug 2007, Intern, SK Communications
