About

 

I'm a Ph.D candidate in FLINT Group at the Department of Computer Science of Yale University, and my advisor is Zhong Shao. I received a M.S. in Computer Science from KAIST, and B.S.E in School of Information and Communication Enginnering from Sungkyunkwan University. AS a M.S. thesis, I worked on building a type system for a small object oriented program language with Professor Sukyoung Ryu, who is a PI of PLRG in KAIST.

Research Interest

 

  • Operating System Design
  • Concurrent Object Verification
  • Software Verification
  • Information Flow Control
  • Proof Assistants and Automated Proof

 

 

Education

 

  • Ph.D Candidacy in Computer Science, September 2012 - Present,

Computer Science Department, Yale

 

  • M.S. in Computer Science, September 2009 - August 2011,

Computer Science Department, KAIST

Thesis: Proving FFMM Type Safety Using Coq

Advisor: Sukyoung Ryu

 

  • B.S.E. in Computer Engineering, March 2002 - August 2009,

School of Information and Communication Engineering, SKKU

 

 

Work Experience

 

  • Assistant in Research, September 2011 - August 2012

Computer Science Department, KAIST

 

 

Publications

 

  • Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro, "Certified Concurrent Abstraction Layers", Proceedings of 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'18), June 2018.

 

  • Jieung Kim, Vilhelm Sjoberg, Ronghui Gu, and Zhong Shao, "Safety and Liveness of MCS Lock- Layer by Layer", Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS'17), November 2017.

 

  • Ronghui Gu, Zhong Shao, Hao Chen, Newman Wu, Jieung Kim, Vilhelm Sjoberg, David Costanzo, "CertiKOS: An Extenisble Architecture for Building Certified Concurrent OS Kernels (Research Paper)," In Proc. 2016 USENIX Symposium on Operating Systems Design and Implementation (OSDI'16), November 2016.

 

  • Ronghui Gu, Zhong Shao, Hao Chen, Newman Wu, Jieung Kim, Vilhelm Sjoberg, David Costanzo, "CertiKOS: An Extenisble Architecture for Building Certified Concurrent OS Kernels (Poster)," In Proc. 2016 USENIX Symposium on Operating Systems Design and Implementation (OSDI'16), November 2016.

 

  • Jieung Kim, Sukyoung Ryu, Victor Luchangco, and Guy L. Steele Jr., "Fine-Grained Function Visibility for Multiple Dispatch with Multiple Inheritance," Proceedings of the 11th Asian Symposium on Programming Languages and Systems (APLAS'13), December 2013.

 

  • Jieung Kim and Sukyoung Ryu, "Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance," The First International Conference on Certified Programs and Proofs (CPP'11), December 2011.

 

  • Jieung Kim, "Proving FFMM Type Safety Using Coq," Master's Thesis (Awarded as an Outstanding M.S. thesis of the year), Korea Advanced Institute of Science and Technology, August 2011.

 

  • Jieung Kim and Sukyoung Ryu, "Coq Mechanization of Featherweight Basic Core Fortress for Type Soundness," Technical Report (ROSAEC-2011-011), May 2011.

 

 

Contacts

 

  • E-mail

jieung.kim [at] yale.edu

 

  • Address

Room 311

Computer Science Department

51 Prospect Street (AKW) New Haven

CT, U.S.A 06511