Topics in Programming Languge: Theory

이광근 Kwangkeun Yi
(소프트웨어무결점 연구센터)/ 프로그래밍 연구실/CSE/Seoul National University

목표 Objectives

프로그래밍언어 연구에서 다루는 개념들을 익히면서 세 가지 능력을 기른다:

• 핵심만다루기(abstraction): 꼭 필요한 것만 드러내는 능력이다. 그래서 군더더기에 방해받지않고 핵심만 파는 능력이다.
• 떼어놓고다루기(modularity): 독립된 부품으로 따로 떼어 다루는 능력이다. 그래서 부품 조립으로 크고 복잡한 구조물을 만들도록 하는 능력이다.
• 정확히다루기(precision): 애매하지않게 각잡고 다루는 능력이다. 그래서 파생 성질을 엄밀히 확인하고 소통하는 능력이다.

이 세가지 능력은 소프트웨어 전문가의 기초 체력이다. 튼튼할수록 좋다. 이 세가지 능력이 전문가로서의 시점을 상승시켜주기 때문이다. 프로그래밍언어 분야에서 연구하거나 프로그래밍언어를 익힐때 뿐만이 아니다. 일반적으로 소프트웨어를 제작하거나 다룰때도 주요한 기초 체력이다.

또, 프로그래밍언어나 프로그래밍 관련 이야기를 접하거나 물어가며 파들어갈 때도 그렇다. 소개한 개념들을 이해하고 용어를 알고 문답하면 더 깊은 내용을 효과적으로 길어올릴 수 있다. 그리고 그 문답의 바닥을 신속히 만나는데도 수월해질 수 있다.

내용 Contents

• 준비: inductive definition, set, function, relation, formal logic, syntax, semantics, proof rule, soundness, completeness, partial order, cpo, continuous function, fixpoint, least fixpoint
  • slides 0.0
  • slides 0.1
• 프로그램 의미 다루기: dynamic semantics, denotational semantics, proof techniques, lambda calculus, operational semantics, evaluation context, value, binding, environment, memory, continuation, exception, control as value, code as value, abstract semantics
  • slides 1.0
  • slides 1.1
• 타입으로 프로그램 다루기: static semantics, simple type, product type, sum type, curry-howard isomorphism, recursive type, polymorphic type, parametric polymorphism, system F, ad-hoc polymorphism, type class, dependent type, lambda cube, abstract data type, subtype, type checking, type inference

• Practical Foundations of Programming Languages (Robert Harper, Cambridge Univ. Press), Theories of Programming Languages (John C. Reynolds, Cambridge Univ. Press), Types and Programming Languages (Benjamin C. Pierce, MIT Press) 등
• 관련 논문들

규정 Policy

  숙제 90%. 기타 10%. 성적은 절대평가.

숙제 Homeworks

• 숙제는 강의시간에 교수에게 제출합니다.
• 제출기한을 지나 48시간 이내로 늦어지면 10% 감점. 그 이후의 숙제는 받지 않습니다.