4541.574 Programming Language Theory

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

강의: 월/수 16:00-17:15 @ 302동 317-2호

목표 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

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

숙제 Homeworks

 

진도및 자료 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 New!, slide19 New!
wk 12 existential types, recursive types
  • 교재/Textbooks

    읽을 논문 Papers

  • © Copyright 2007, 이 광근 Kwangkeun Yi