Topics in Programming Languge: Theory

강의: 화/목 14:00-15:15 @ 302동 309-1호

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

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

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

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

실라부스.
강의에서는 가능하면 [쉬운전문용어]를 사용합니다.

준비: 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
타입으로 프로그램 다루기: static semantics, simple type, product type, sum type, curry-howard isomorphism, recursive type, polymorphic type, parametric polymorphism, system F, ad-hoc polymorphism, type class, lambda cube, dependent type, calculus of constructions, 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), Handbook of Logic in Computer Science, Vol.2 (Background: Computational Structures) (Edited by S. Abramsky et al., Oxford Science Publications)
관련 논문들