교원프로필

박성우 사진
교원에 대한 정보를 나타내는 표입니다.
성명 박성우
소속 컴퓨터공학과
전화번호 279-2386
E-mail gla@postech.ac.kr
Homepage http://pl.postech.ac.kr/

학력

  • 1999.09 ~ 2005.08 CARNEGIE MELLON UNIV. (박사-전산학)
  • 1996.03 ~ 1998.02 한국과학기술원 (석사-전산학)
  • 1991.03 ~ 1996.02 한국과학기술원 (학사-전산학)

주요경력

  • 2006.01 ~ 2006.08 : POSTECH
  • 2005.08 ~ 2005.12 : Carnegie Mellon Univ.
  • 1999.01 ~ 1999.06 : KAiST
  • 1998.01 ~ 1999.01 : 시스템공학연구소

전문분야

  • 프로그래밍언어
  • 전산논리

학술지

국제전문학술지

  • Mechanizing Metatheory without Typing Contexts, Journal of Automated Reasoning, , 52, 215-239 (2014)
  • A Proof System for Separation Logic with Magic Wand, SIGPLAN Notices, , 49, 477-490 (2014)
  • A Theorem Prover for Boolean BI, ACM SIGPLAN NOTICES, , , 219-231 (2013)
  • Judgmental Subtyping Systems with Intersection Types and Modal Types, Acta Informatica, , 50, 359-380 (2013)
  • Group Skyline Computation, INFORMATION SCIENCES, , 188, 151-169 (2012)
  • Computing Exact Skyline Probabilities for Uncertain Databases, IEEE Transactions on Knowledge and Data Engineering, , 24, - (2012)
  • Computing Exact Skyline Probabilities for Uncertain Databases, IEEE Transactions on Knowledge and Data Engineering, , 24, 2113-2126 (2012)
  • Parallel Skyline Computation on Multicore Architectures, INFORMATION SYSTEMS, , 36, 808-823 (2011)
  • A calculus for hardware description, JOURNAL OF FUNCTIONAL PROGRAMMING, , 21, 21-58 (2011)
  • A Modal Logic Internalizing Normal Proofs, INFORMATION AND COMPUTATION, , 209, 1519-1535 (2011)
  • Type-safe higher-order channels with channel locality, JOURNAL OF FUNCTIONAL PROGRAMMING, , 19, 107-142 (2009)
  • TYPE-SAFE HIGHER-ORDER CHANNELS WITH CHANNEL LOCALITY, JOURNAL OF FUNCTIONAL PROGRAMMING, , 19, 107-142 (2009)
  • Functional netlists, ACM SIGPLAN NOTICES, , 43, 353-365 (2008)
  • A Probabilistic Language Based on Sampling Functions, ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, , 31, - (2008)
  • A PROBABILISTIC LANGUAGE BASED ON SAMPLING FUNCTIONS, ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, , 31, - (2008)
  • Functional netlists, ACM SIGPLAN NOTICES, , 43, 353-365 (2008)
  • Type-safe higher-order channels in ML-like languages factors for erosive oesophagitis and non-erosive reflux disease: a nationwide multicentre prospective study in Korea, ACM SIGPLAN NOTICES, , 42, 191-202 (2007)

국내전문학술지

  • 선형논리에 기반한 불확실성 데이터베이스 의미론, 정보과학회논문지 : 소프트웨어 및 응용, , 37, 148-154 (2010)

일반학술지

  • 포항공과대학교 컴퓨터공학과 교과과정 개편안에 대한 소개, 정보과학회지, , 28, 45-48 (2010)
  • 컴퓨터학과 학부 프로그램 재고, 정보과학회지, , 27, 21-25 (2009)
  • 파서생성기 생성기의 구현, 한국정보과학회 프로그래밍언어논문지, , 22, 1-13 (2008)

학술회의논문

  • Parallel Skyline Computation on Multicore Architectures, PROCEEDINGS OF THE 25TH INTERNATIONAL CONFERENCE ON DATA ENGINEERING, 0, 0, - (2009)
  • A Logical Account of Uncertain Databases based on Linear Logic, PROCEEDINGS OF THE 12TH INTERNATIONAL CONFERENCE ON DATABASE THEORY, 0, 0, - (2009)
  • Functional netlists, PROCEEDINGS OF THE 13TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, 0, 0, - (2008)
  • Type-safe higher-order channels in ML-like languages, PROCEEDINGS OF THE 12TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, 0, 0, - (2007)
  • A modal language for the safety of mobile values, PROCEEDINGS OF THE FOURTH ASIAN SYMPOSIUM ON PROGRAMMING LANGUAGES AND SYSTEMS, 0, 0, - (2006)
  • A modal language for distributed computation, Lecture Notes in Computer Science, 0, 0, 217-233 (2006)
  • A Probabilistic Language based upon Sampling Functions, 발표논문집, 0, 0, - (2005)
  • A Calculus for Probabilistic Languages, 발표논문집, 0, 0, - (2003)

학회발표

  • A Proof System for Separation Logic with Magic Wand, ., 0, 0, - (2014)
  • Contractive Signatures with Recursive Types, Type Parameters, and Abstract Types, ., 0, 0, - (2013)
  • A Theorem Prover for Boolean BI, ., 0, 0, - (2013)
  • A Syntactic Type System for Recursive Modules, ., 0, 0, - (2011)
  • Towards a Cut-free Sequent Calculus for Boolean BI, ., 0, 0, - (2010)
  • A module system independent of base languages, ., 0, 0, - (2009)
  • A critique of R, Japanese R Users' Meeting, 0, 0, - (0000)

단행본

연구실적

  • 건설적 논리체계에서 직접적 증명을 위한 방법 개발, 포항공과대학교 (2006-2007)
  • 건설적 논리 체계에서 직접적 증명에 관한 연구, 한국학술진흥재단 (2006-2007)
  • 타입이론에 기반을 둔 차세대 함수형 언어의 개발, 학생의료공제회 (2006-2007)
  • 타입이론에 기반을 둔 차세대 함수형 언어의 개발, 포항공과대학교 (2007-2008)
  • 멀티코어 컴퓨팅 환경을 위한 병렬 프로그래밍 언어의 개발, 한국과학재단 (2007-2008)
  • COMPUTATIONAL SCIENCE FOR 2020 SCIENCE, 포항공과대학교 (2007-2008)
  • 멀티코어 컴퓨팅 환경을 위한 병렬 프로그래밍 언어의 개발, 한국과학재단 (2008-2009)
  • 4.1770_2차년도의 이월과제, 한국과학재단 (2008-2009)
  • 람다 계산식에 기초한 함수형 하드웨어 기술언어의 개발, 한국학술진흥재단 (2008-2009)
  • 멀티코어 컴퓨팅 환경을 위한 병렬 프로그래밍 언어의 개발, 한국과학재단 (2009-2010)
  • (학생)인건비풀링과제, 포항공대산학협력단 (2009-2020)
  • 인건비풀링과제, 포항공과대학교 (2009-2015)
  • 자체연구개발과제, 포항공과대학교 (2009-2016)
  • 4.2647_2차년도의 이월과제, 한국과학재단 (2009-2010)
  • 범용 프로그래밍 언어를 위한 고차 모듈 시스템 개발, 한국과학재단 (2009-2010)
  • 그룹 스카이라인 계산(학부생연구프로그램), 포항공과대학교 (2009-2010)
  • 범용프로그래밍 언어를 위한 고차 모듈 시스템 개발, 재단법인한국연구재단 (2010-2011)
  • 4.4097 1차년도 이월과제, 재단법인한국연구재단 (2010-2011)
  • 분리 논리에 기초한 C 프로그램용 연역 검증 도구의 개발, 재단법인한국연구재단 (2010-2011)
  • 범용 프로그래밍 언어를 위한 고차 모듈 시스템 개발, 재단법인한국연구재단 (2011-2012)
  • 4.5453/5803_2차년도 이월과제, 재단법인한국연구재단 (2011-2012)
  • 분리 논리에 기초한 C 프로그램용 연역 검증 도구의 개발, 재단법인한국연구재단 (2011-2012)
  • 4.5955_1차년도 이월과제, 재단법인한국연구재단 (2011-2012)
  • 분리 논리에 기초한 C 프로그램용 연역 검증 도구의 개발, 재단법인한국연구재단 (2012-2013)
  • 4.7297/7626_2차년도 이월과제, 재단법인한국연구재단 (2012-2013)
  • 구문 서브타이핑 이론 연구 및 XML 변환 언어 개발, 재단법인한국연구재단 (2013-2014)
  • 구문 서브타이핑 이론 연구 및 XML 변환 언어 개발, 재단법인한국연구재단 (2014-2015)
  • 4.10368의 이월과제, 재단법인한국연구재단 (2014-2015)
  • 자체연구개발과제[2015년 신설], 포항공과대학교 (2015-2041)
  • 밀기 모델 기반의 차세대 HADOOP 계산 엔진 개발, 재단법인 삼성미래기술육성재단 (2015-2018)
  • 구문 서브타이핑 이론 연구 및 XML 변환 언어 개발, 재단법인한국연구재단 (2015-2016)
  • 4.11586_이월과제, 재단법인한국연구재단 (2015-2016)

IP