¹Ú¼º¿ì Sungwoo Park - ȯ¿µÇÕ´Ï´Ù Welcome! Associate Professor ºÎ±³¼ö Programming Language Laboratory ÇÁ·Î±×·¡¹Ö¾ð¾î¿¬±¸½Ç Computer Science and Engineering Department ÄÄÇ»ÅÍ°øÇаú Pohang University of Science and Technology (POSTECH)

I received my BS and MS in Computer Science from KAIST. I received my PhD in Computer Science from Computer Science Department of Carnegie Mellon University under the supervision of Professor Frank Pfenning in 2005. I joined Computer Science and Engineering Department of POSTECH in 2006.

Research

Current events:

• PEPM 2014 (PC member)
• ICFP 2013 (PC member)

• A theorem prover for separation logic
  Despite its relatively short history, separation logic is revolutionizing the way that low-level programs are verified and will be of increasing importance in the years to come. We are currently designing and implementing a theorem prover for separation logic. Unlike existing theorem provers, our work aims at developing a theorem prover for full separation logic which includes not only the separating conjunction but also separating implication, commonly known as magic wand. As a preliminary step, we have built a theorem provef for Boolean BI, the underlying logic of separation logic, which was published at POPL 2013.
• Streamlining data flows in Hadoop
• A parallel web browser (Our secret weapon is: ³ª¶õÈ÷ ´Þ¸®´Â ³«Å¸!)
• A syntactic subtyping system with intersection and union types
• A theorem prover for intuitionistic modal logic S5
• Judgmental subtyping systems with intersection types and modal types

1. Hyeonseung Im, Keiko Nakata, and Sungwoo Park. Contractive Signatures with Recursive Types, Type Parameters, and Abstract Types. ICALP 2013. [PDF]
2. Jonghyun Park, Jeongbong Seo, Sungwoo Park, and Gyesik Lee. Mechanizing Metatheory without Typing Contexts. Journal of Automated Reasoning, April 2013. [Webpage] (with a solution to the POPLmark challenge)
3. Jonghyun Park, Jeongbong Seo, and Sungwoo Park. A Theorem Prover for Boolean BI. POPL 2013. [Webpage] (¼ø¼ö Çѱ¹´ëÇÐ ÃÖÃÊ)
4. Dongwon Kim, Hyeonseung Im, and Sungwoo Park. Computing Exact Skyline Probabilities for Uncertain Databases. IEEE Transactions on Knowledge and Data Engineering (TKDE), December 2012. [PDF]
5. Hyeonseung Im and Sungwoo Park. Group Skyline Computation. Information Sciences 188:151-169, April 2012. [PDF]
6. Sungwoo Park and Hyeonseung Im. A Modal Logic Internalizing Normal Proofs. Information and Computation 209(12):1519-1535, October 2011. [PDF]
7. Hyeonseung Im, Keiko Nakata, Jacques Garrigue, and Sungwoo Park. A Syntactic Type System for Recursive Modules. OOPSLA 2011. [PDF] (Çѱ¹ µÎ¹ø°, Æ÷½ºÅØ µÎ¹ø°)
8. Hyeonseung Im, Jonghyun Park, and Sungwoo Park. Parallel skyline computation on multicore architectures. Information Systems 36(4):808-823, June 2011. [PDF]
9. Sungwoo Park and Hyeonseung Im. A calculus for hardware description. Journal of Functional Programming 21(1):21-58, January 2011. [PDF]
10. Sungwoo Park and Hyeonseung Im. Type-safe higher-order channels with channel locality. Journal of Functional Programming 19(1):107-142, January 2009. [PDF]
11. Sungwoo Park and Seung-won Hwang. A logical account of uncertain databases based on linear logic. ICDT 2009. [PDF] (Çѱ¹ ÃÖÃÊ)
12. Sungwoo Park, Taekyung Kim, Jonghyun Park, Jinha Kim, and Hyeonseung Im. Parallel skyline computation on multicore architectures. ICDE 2009. [PDF]
13. Sungwoo Park, Frank Pfenning, and Sebastian Thrun. A probabilistic language based upon sampling functions. TOPLAS 31(1), December 2008. [PDF]
14. Sungwoo Park, Jinha Kim, and Hyeonseung Im. Functional netlists. ICFP 2008. ACM SIGPLAN Notices 43(9), September 2008. [PDF] (Çѱ¹ µÎ¹ø°)
15. Sungwoo Park. Type-safe higher-order channels in ML-like languages. ICFP 2007. ACM SIGPLAN Notices 42(9), September 2007. [PDF] (Çѱ¹ ÃÖÃÊ)
16. Sungwoo Park. A modal language for the safety of mobile values. APLAS 2006. LNCS 4279, pp. 217--233, 2006. [PDF]
17. Sungwoo Park, Frank Pfenning, and Sebastian Thrun. A probabilistic language based upon sampling functions. POPL 2005. ACM SIGPLAN Notices 40(1), January 2005. [PDF] (¹Ú»ç°úÁ¤ ¿¬±¸ °á°ú)
18. Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, Stephen Magill, and Sungwoo Park. The inverse method for the Logic of Bunched Implications. LPAR 2004. LNAI 3452, pp. 466-480, March 2005. [PDF]
19. Sungwoo Park. A calculus for probabilistic languages. TLDI 2003. ACM SIGPLAN Notices 38(3), March 2003. [PDF]
20. Sungwoo Park and Taisook Han. Iterative inversion of fuzzified neural networks. IEEE Transactions on Fuzzy Systems 8(3):266-280, June 2000. [PDF] (KAIST ¼®»çÇÐÀ§ ³í¹®)
21. Sungwoo Park and Taisook Han. Object-oriented VRML for multi-user environments. VRML 97. [ACM DL] (óÀ½À¸·Î ÇÐȸ¿¡ ¹ßÇ¥ÇÑ ³í¹® :-))

Students

• ±èµ¿¿ø Dongwon Kim (PhD 09)
• ¹ÚÇüö Hyungchul Park (MS 12)
• ÀÌ¿ø¿­ Wonyeol Lee (Çкλý)

Past students:

• ¼­Á¤ºÀ Jeongbong Seo (MS 11)
• ¹ÚÁ¾Çö Jonghyun Park (PhD 08). Thesis: A Theorem Prover for Boolean BI. Defended in December 2012. Now at Samsung Electronics.
• ÀÓÇö½Â Hyeonseung Im (PhD 06). Thesis: A Syntactic Type System for Recursive Modules. Defended in August 2012. Postdoc at INRIA.
• ÀÓÁ¤Ç¥ Jungpyo Im (MS 09)
• ±èÅ°æ Taekyung Kim (MS 07)
• ±èÁøÇÏ Jinha Kim (MS 06)
• ¼Õ¹Î¿µ Minyoung Son (MS 06)

Personal

• ÇлýÀ» ¹Ù¶óº¸´Â ½Ã°¢ (2010³â 6¿ù) [Page 1, Page 2, Page 3]
• ÀüÀÚ°è»êÇÐ - °è»êÀû »ç°í¹æ½ÄÀ» ÁÖ¹«±â·Î Çϴ âÁ¶ÀÇ Çй® (2009³â 5¿ù) [Page 1, Page 2, Page 3]
  (±Û ¸»¹Ì¿¡ ¾ð±ÞµÈ Æ丣¸¶ÀÇ ¸¶Áö¸· Á¤¸® Áõ¸íÀ» ÄÄÇ»ÅÍ·Î °ËÁõÇß´Ù´Â ³»¿ëÀº À߸øµÈ Á¤º¸ÀÌ¸ç ¾ÆÁ÷ °ËÁõµÇÁö ¾Ê¾Ò½À´Ï´Ù.)
• StarCraft 2:2 °æ±â (2008³â 10¿ù. with ´ëÈñ, ÁØÈ£, ´ëÇõ. ´ëÇõÀÇ ¸ð´ÏÅ͸¦ ÀÚ¼¼È÷ º¸¸é ºñ¹ÐÀÌ ¼û¾î ÀÖÀ½!)
• Diablo 2 À̾߱â
  2006³â ÇÁ·Î±×·¡¹Ö¾ð¾î °ú¸ñ ¼ö°­»ý 7¸íÀ» follower botÀ¸·Î µ¿¿øÇß´ø À̾߱â [Diablo 321]
• Word lists for GRE (1998³â À¯ÇÐ Áغñ ¸¶Ä£ Á÷ÈÄ ¸¸µç GRE ´Ü¾î À¥ÆäÀÌÁö)

Travel ¿©Çà

• Æä·ç Äí½ºÄÚ ¸¶ÃßÇÈÃß (Peru Cusco Machu Picchu). 2005³â 12¿ù

Teaching

• CSE-321 Programming Languages, Spring 2013. Course notes [PDF]
• CSE-321 Programming Languages, Spring 2012.
• CSE-433 Logic in Computer Science, Fall 2011. Course notes [PDF]
• CSE-321 Programming Languages, Spring 2011.
• CSE-433 Logic in Computer Science, Fall 2010.
• CSE-321 Programming Languages, Spring 2010.
• CSE-499 °úÁ¦¿¬±¸, Spring 2010.
• CSE-433 Logic in Computer Science, Fall 2009.
• CSE-321 Programming Languages, Spring 2009.
• CSE-499 °úÁ¦¿¬±¸, Fall 2008.
• EECS-101 Introduction to Computing, Spring 2008. Course notes (in Korean) [PS, PDF]
• CSE-700 Parallel Programming, Fall 2007
• CSE-433 Logic in Computer Science, Fall 2007.
• CSE-321 Programming Languages, Spring 2007
• CSE-490 Logic in Computer Science, Fall 2006
• CSE-321 Programming Languages, Spring 2006

Office: PIRL 334
Phone: +82-54-279-2386
Fax: +82-54-279-2299
Email: gla at postech dot ac dot kr

»ç¹«½Ç: Á¤º¸Åë½Å¿¬±¸¼Ò 334È£
ÀüÈ­: 054-279-2386
À̸ÞÀÏ: gla at postech.ac.kr
[gmail.com, yahoo.com, samsung.comÀ» Á¦¿ÜÇÑ .com, .net, .co.kr, .or.kr, .info ¸ÞÀÏÀº ¸ðµÎ spamÀ¸·Î 󸮵˴ϴÙ]