Programming Language Laboratory - Welcome!

Computer Science and Engineering Department
Pohang University of Science and Technology

학생 및 Scala 전임개발자 모집

POSTECH 프로그래밍언어 연구실에서는 삼성 미래기술육성사업의 지원을 받아서 2015년 9월부터 밀기모델 기반의 차세대 Hadoop 계산 엔진 개발 연구를 수행하고 있습니다. 연구의 최종목표는 MapReduce, Tez, Spark보다 속도는 빠르고 프로그래밍 인터페이스는 동일한 새로운 Hadoop 계산 엔진 MR3를 개발하는 것입니다. MR3 개발은 Scala 언어를 이용합니다.

프로그래밍언어 연구실에서는 빅데이터, Hadoop, 분산 처리 시스템, 오픈소스 개발에 관심있는 석사/박사/통합 과정 대학원생 및 학부생 연구원을 모집합니다. 참여 학생은 MR3 관련 연구에 참여하게 되며 삼성 미래기술육성사업으로부터 지원을 받게 됩니다. Scala 프로그래밍 경험은 필요하지 않으며 컴퓨터공학 학부 핵심 과목을 충실하게 이해하고 있으면 됩니다.

프로그래밍언어 연구실에서는 MR3 개발에 참여할 Scala 전임개발자를 모십니다. Scala 프로그래밍 경험은 필요하지는 않으나 multi-threaded/distributed Java 프로그래밍 경험은 필수입니다. 특히 함수형언어 OCAML 또는 Haskell 프로그래밍에 익숙하면 우대합니다. Hadoop 환경에 익숙하면 좋지만 필수 요구 조건은 아닙니다. 삼성 미래기술육성사업을 통해서 대기업 수준으로 대우하며 자유로운 근무환경을 제공합니다.

자세한 문의는 박성우 교수에게 이메일을 보내시면 됩니다 (gla at postech.ac.kr).

Graduate student and Scala developer positions available

Programming Language Laboratory at POSTECH has recently started a new project entitled "Developing a next-generation computing engine for Hadoop based on the push model," which is sponsored by a grant from Samsung Research Funding Program for Future Technologies. Our goal is to design and implement a new computing engine for Hadoop, called MR3, that supports DAG, fault tolerance, and in-memory computing, thus delivering superior performance to existing technologies such as MapReduce, Tez, and Spark while providing the same programming interface. We are developing MR3 in the Scala programming language.

We are looking for new graduate students, at both master's and doctoral levels, in the fields of big data computing, Hadoop, distributed computing, and open source software. A prerequisite is a solid background in undergraduate computer science, and no prior experience with Scala programming or Hadoop is required.

We are also hiring regular developers who will contribute to the MR3 project. Prior experience with Scala programming is NOT required, but applicants should have working experience with multi-threaded or distributed Java programming. We are especially interested in hiring experts in functional programming with OCAML or Haskell. No prior experience with Hadoop is required. The salary, at par with the best in the industry, will be competitive and commensurate with the level of expertise and programming experience.

Applicants are invited to contact Professor Sungwoo Park (gla at postech.ac.kr).

Members

• Members
  - 박성우, Sungwoo Park
  - Dinh Hoang Mai
  - Le Minh Hoang
  - Jacob Morton

• Past Students
  - 임현승, Hyeonseung Im (PhD 06). Thesis: A Syntactic Type System for Recursive Modules. Defended in August 2012. Postdoc at INRIA. Assistant professor at 강원대.
  - 손민영, Minyoung Son (MS 06). SAIT (삼성전자 종합기술원).
  - 김진하, Jinha Kim (MS 06). POSTECH Data Mining 연구실.
  - 김태경, Taekyung Kim (MS 07). 중소기업은행.
  - 박종현, Jonghyun Park (PhD 08). Thesis: A Theorem Prover for Boolean BI. Defended in December 2012. Samsung Electronics.
  - 김동원, Dongwon Kim (PhD 09). SK.
  - 임정표, Jeongpyo Lim (MS 09). 현대 모비스.
  - 서정봉, Jeongbong Seo (MS 11). Samsung Electronics.
  - 박형철, Hyungchul Park (MS 12). Google.
  - 이원열, Wonyeol Lee (Undergraduate 13). PhD student at Stanford Computer Science.
  - Dinh Hoang Mai (MS 14). POSTECH Programming Language 연구실.
  

현재 연구

• 분리 논리(separation logic with magic wand) 기반 프로그램 검증 시스템 개발
  소프트웨어 결점으로 인한 문제가 심각해지면서 프로그램 자체를 분석하여 실행 중 오류를 미연에 방지하는 기술이 개발되었습니다. 이런 프로그램 분석 기술은 크게 1세대 테스팅(testing)과 2세대 모델검사(model checking), 요약해석(abstract interpretation), 그리고 이런 기술을 조합한 복합 기술로 나누어집니다. 프로그램 검증은 기존 기술의 한계를 넘은 3세대 기술로서 사용자가 검증하고자 하는 프로그램의 성질을 논리식으로 표현한 뒤 자동 정리 증명기(automatic theorem prover)나 증명 보조기(proof assistant)를 이용하여 증명해 냅니다. 본 연구에서는 기존의 Hoare 논리의 한계를 넘어서는 분리 논리에서 Magic Wand 연산자를 활용한 새로운 프로그램 검증 시스템을 개발하고 있습니다.
  연구 결과: [POPL 2014] [POPL 2013]

• 구문 서브타이핑 이론 연구
  XML 문서 처리를 위한 언어가 W3C를 통해서 발표되면서 프로그래밍언어 학계에서는 타입 이론을 이용하여 XML 문서 변환의 안전성을 정적으로 보장하기 위한 연구를 시작했습니다. XML 문서는 일반적으로 재귀적 트리 구조를 가지기 때문에 입력으로 주어진 XML 문서의 구조를 정확하게 알지 못하는 경우에는 원하는 변환이 실패할 수가 있습니다. 본 연구에서는 XML 문서의 구조를 타입을 이용해서 표현하는데 있어 가장 중요한 이론적 난제인 서브타이핑 체계를 개발하고 있습니다.
  예비 연구 결과: [Acta Informatica 2013]

• 차세대 Hadoop 계산 엔진 개발
  

  클러스터 환경용 소프트웨어 프레임워크 Hadoop에서 전체 성능에 가장 큰 영향을 미치는 모듈은 MapReduce, Tez, Spark, Flink와 같은 계산 엔진입니다. Tez, Spark, Flink는 MapReduce를 대체할 차세대 Hadoop 계산 엔진으로 경쟁하고 있지만 현시점에서 특정 계산 엔진이 모든 빅데이터 처리 문제에 일괄적으로 채택되기는 현실적으로 어렵습니다. 이런 상황에서 모든 빅데이터 처리 문제에 일괄적으로 쓸 수 있는 시스템에 대한 필요성이 대두되었습니다. 본 연구에서는 MapReduce, Tez, Spark보다 계산 속도는 빠르고 프로그래밍 인터페이스는 동일한 Hadoop 계산 엔진을 새로 개발하고 있습니다. 엔진 개발은 Scala 언어를 이용합니다.

대표 논문

• A Proof System for Separation Logic with Magic Wand.
  Wonyeol Lee and Sungwoo Park.
  POPL 2014. [Webpage]
  이 논문은 POPL 41년 역사상 두 번째 순수 국내 대학 POPL 논문입니다.

• Judgmental Subtyping Systems with Intersection Types and Modal Types.
  Jeongbong Seo and Sungwoo Park.
  Acta Informatica 50(7):359-380, October 2013. [Webpage]

• Contractive Signatures with Recursive Types, Type Parameters, and Abstract Types.
  Hyeonseung Im, Keiko Nakata, and Sungwoo Park.
  ICALP 2013, Part II, pp. 299-311.

• Mechanizing Metatheory without Typing Contexts.
  Jonghyun Park, Jeongbong Seo, Sungwoo Park, and Gyesik Lee.
  Journal of Automated Reasoning 52(2):215-239, April 2013. [Webpage] (with a solution to the POPLmark challenge)

• A Theorem Prover for Boolean BI.
  Jonghyun Park, Jeongbong Seo, and Sungwoo Park.
  POPL 2013. ACM SIGPLAN Notices 48(1):219-232, January 2013. [Webpage]
  이 논문은 POPL 40년 역사상 최초의 순수 국내 대학 POPL 논문입니다.

• Computing Exact Skyline Probabilities for Uncertain Databases.
  Dongwon Kim, Hyeonseung Im, and Sungwoo Park.
  IEEE Transactions on Knowledge and Data Engineering (TKDE) 24(12):2113-2126, December 2012.

• Group Skyline Computation.
  Hyeonseung Im and Sungwoo Park.
  Information Sciences 188:151-169, April 2012. [PDF]

• A Modal Logic Internalizing Normal Proofs.
  Sungwoo Park and Hyeonseung Im.
  Information and Computation 209(12):1519-1535, October 2011. [PDF]

• A Syntactic Type System for Recursive Modules.
  Hyeonseung Im, Keiko Nakata, Jacques Garrigue, and Sungwoo Park.
  OOPSLA 2011. ACM SIGPLAN Notices 46(10):993-1012, October 2011. [PDF]
  이 논문은 OOPSLA 25년 역사상 국내 대학 두 번째 OOPSLA 논문입니다.

• Parallel skyline computation on multicore architectures.
  Hyeonseung Im, Jonghyun Park, and Sungwoo Park.
  Information Systems 36(4):808-823, June 2011. [PDF]
  Sungwoo Park, Taekyung Kim, Jonghyun Park, Jinha Kim, and Hyeonseung Im.
  ICDE 2009, pp. 760-771. [PDF]

• A calculus for hardware description.
  Sungwoo Park and Hyeonseung Im.
  Journal of Functional Programming 21(1):21-58, January 2011. [PDF]
  Functional netlists.
  Sungwoo Park, Jinha Kim, and Hyeonseung Im.
  ICFP 2008. ACM SIGPLAN Notices 43(9):353-366, September 2008. [PDF]
  이 논문은 국내 대학 두 번째 ICFP 논문입니다.

• Type-safe higher-order channels with channel locality.
  Sungwoo Park and Hyeonseung Im.
  Journal of Functional Programming 19(1):107-142, January 2009. [PDF]
  Type-safe higher-order channels in ML-like languages.
  Sungwoo Park.
  ICFP 2007. ACM SIGPLAN Notices 42(9):191-202, September 2007. [PDF]
  이 논문은 국내 대학 최초의 ICFP 논문입니다.

• A logical account of uncertain databases based on linear logic.
  Sungwoo Park and Seung-won Hwang.
  ICDT 2009, pp. 141-148. [PDF]
  이 논문은 국내 대학 최초의 ICDT 논문입니다.

• A probabilistic language based upon sampling functions.
  Sungwoo Park, Frank Pfenning, and Sebastian Thrun.
  TOPLAS 31(1), Article 4, December 2008. [PDF]
  POPL 2005. ACM SIGPLAN Notices 40(1):171-182, January 2005. [PDF]

• A modal language for the safety of mobile values.
  Sungwoo Park.
  APLAS 2006. LNCS 4279, pp. 217-233, November 2006. [PDF]

연구 결과

• A Proof System for Separation Logic with Magic Wand
• A theorem prover for intuitionistic modal logic S5
• BBeye: A Theorem Prover for Boolean BI (Bunched Implications)
• Mechanizing Metatheory without Typing Contexts
• Judgmental subtyping systems with intersection types and modal types
• PGG (Parser Generator Generator for functional languages)
• QuickParanoid

Life @ 프로그래밍 언어 연구실

• 우리들의 이야기 (Our Story)

Office: PIRL, 354
Phone: +82-54-279-5878

Web page maintained by Sungwoo Park