4541.574 Programming Language Theory

이광근 Kwangkeun Yi
Programming Research Lab./CSE/Seoul National University

목표 Objectives

이 강의의 목표는 프로그래밍 언어 분야에서 축적된 주요 내용과 그것을 엄밀하게 표현하고 응용하는 과학적인 솜씨를 익히게 하는 것이다.

이러한 강의가 왜 필요한 것일까?

• 소프트웨어 이론의 많은 기초가 프로그래밍 언어 이론을 학습하면서 효과적으로 준비된다.
• 소프트웨어에 대한 "엄밀한"(formal) 논문을 읽고 쓰는 데 익숙해 진다. 소프트웨어를 모델하고 기술하고 살펴보고 확인하며 그 성질의 좋은 점을 설득하는 논문을 쓰는 방식을 익히게 된다.
• 고부가 소프트웨어 개발은 나날히 엄밀한 기술이 되가고 있고, 그 한 축이 보다 정교하고 편리한 타입 시스템을 갖춘 프로그래밍 언어의 사용이다.
• 대부분의 소프트웨어 시스템들이 컴퓨터 언어를 처리하는 부품을 품고 있게 되는데, 이 부품들이 프로그래밍 언어 분야에서 축적한 이론과 실제에 대한 성과를 이해하고 설계될 필요가 있다.

내용 Contents

• 가로
  • Semantic formalisms: natural semantics, structural operational semantics, abstract machine semantics, evaluation contexts
  • Proof techniques/principles: induction, structural induction, fixpoint induction, induction on proof size, logical relation
• 세로
  • Preliminaries: abstract syntax, binding, scope, renaming, compositional semantics, logics and inference
  • Lambda Calculus: operational semantics, normal-order/eager-order reduction, Church thesis, lambda encodings, domain theory
  • Applicative Language: datatypes, functions, exceptions, continuations, continuation-passing-style transformation, abstract machines
  • Type System: monomorphic type system, polymorphic type system, existential type system, subtype system, typeful compilation

규정 Policy

• 성적은 절대평가.
• 출석 100%는 필수. 어쩔 수 없는 경우는 반드시 사전 허락을 받는다.

숙제 Homeworks

• HW1: OCaml programming. Due 10/10 24:00.
• HW2: Semantics, Lambda Calculus evaluator. Due 10/29 24:00.
• HW3: simple type system proof for exceptions. Due 11/19 16:00.
• HW4: let-polymorphic type inference. Due 12/05 24:00
  The M Language

진도및 자료 Slides & Resources

wk 1	part -1: induction, logic, inference, proofs	slide0, book5-24, slide1
wk 2	part -1: abstract syntax, operational semantics	slide2
wk 3	part 0: HOT (higher-order & typed) programming I	slide3
wk 4	part 0: HOT programming II	slide4
wk 5	language model: lambda calculus	slide5, slide6, slide7
wk 6	simply typed lambda calculus	slide8, slide9, slide10
wk 7	extensions on to a real language	slide11, slide12, slide13
wk 8	simple type reconstruction	slide14
wk 9	let-polymorhpic types	slide15
wk 10	let-polymorphic type reconstruction	slide16
wk 11	subtypes	slide17, slide18 , slide19
wk 12	existential types, recursive types

• To view/print PS(Postscript) files: Ghostview
• To view/print PDF files: Acrobat Reader