Reading Lists

•

소프트웨어언어 및 시스템 연구실의 연구 주제인 프로그래밍언어, 컴파일러, 소프트웨어공학, 논리 분야의 기초가 되는 논문이나 책 목록을 나열한다.

프로그래밍언어

  • (BOOK) Essentials of Programming Langauges by Friedman, Wand, Haynes.
    • 인터프리터를 작성함으로써 프로그래밍언어 시맨틱스를 이해
  • (BOOK) Types and Programming Languages by Benjamin C. Pierce
    • 일명, TAPL 책으로 부르는 타입 시스템에 대한 훌륭한 입문서이자 참고 서적
    • 주요 내용 : 프로그래밍언어 기초인 람다계산법(Lambda Calculus), 의미규칙(Semantics, Small-step and Operational), 타입 규칙(Type system)
    • 1장, 2장, 3~5장, 7장, 8~11장, 13장, 15장, 20장, 23장, 24장
  • (PAPER) A Syntactic Approach to Type Soundness by A. K. Wright and M. Felleisen
    • Evaluation contexts를 사용하여 Subject reduction과 Progress를 증명함으로써 type soundness를 증명하는 일반적인 테크닉
    • Functional ML에 대한 증명과, State와 Exception을 확장한 A core of Standard ML에 대한 증명을 배울 수 있음.
    • 한가지 언급하고 싶은 점은, 아마도 시대적인 이유로 Hindlely-Milner polymorphism을 고려한 Functional ML calculus에 대한 type soundness를 설명하다보니 증명 테크닉의 key가 약간은 흐려진 느낌. System F에 대한 type soundness나 그냥 the simply typed lambda calculus에 대한 type soundness를 증명하는 내용을 설명했다면 증명 테크닉을 설명하는 더 좋은 예가 되었을 것임.
    • TAPL 책에서 type soundness 증명 스타일과 차이점을 비교하면서 이 논문을 읽어보는 것도 좋음. 예를 들어 이 논문에서는 1) Evaluation contexts를 사용해 operational semantics를 정의하고 있고, 2) Stuck expression의 suepr set으로 Faluty expression을 정의하여 Progress를 증명하는데 TAPL은 다른 방식임.
  • (PAPER) The Essence of Compiling with Continuations by C. Flanagan, A, Sabry, B. F. Duba, M. Felleisen, PLDI 1993.
    • 람다 프로그램을 컴파일하고 실행하는 과정에 대한 기본적인 아이디어
    • 의미규칙. 컴파일러의 중간언어. 추상기계 개념
    • A-Normal form vs. CPS (Continuation-Passing Style)
  • (PAPER) From System F to Typed Assembly Language, G. Morrisett, D. Walker, K. Cray, N. Glew
    • 함수형 언어 컴파일러를 쉽게 배워보고 싶은 경우 추천하는 논문. 직접 구현해보기에 적절하도록 간단함.
    • TAPL 책과 Wright&Felleisen 논문에서 type soundness 증명 테크닉을 연습한 다음 이 논문의 증명을 따라가보는 것도 도움이 될 것임.
    • 이 논문은 continuation으로 제어를 구현하는데, stack으로 제어를 구현하는 논문이 JFP에 있으니 함께 비교해서 볼 것.
  • (PAPER) The Logical Abstract Machine: a Curry-Howard Isormorphism for Machine Code by Atsushi Ohori
    • 이 논문은 위 "From System F to Typed Assembly Language" 논문과 비교하면서 읽을 논문이다. 증명이 상당히 간단해졌는데 그 이유는 타입을 직접 term language에 표현하는가 아니면 그렇지 않은가의 차이 때문이다. 예를 들어 이 논문은 closure 타입으로 위 논문에서 사용했던 Exists x. tau를 사용하지 않는다! value와 type의 logical relation으로 이를 대체하는데 이때 일반 함수 타입 tau -> tau'으로 closure 타이핑을 하는데 충분하다.
  • (PAPER) A Type Theory for Krivine-Style Evaluation and Compilation by Kwanghoon Choi and Atsushi Ohori
    • 앞의 논문들에서 small-step operational semantics를 사용했는데, 이 논문에서는 big-step operational semantics를 사용한다. operational semantics 스타일이 달라지면 type soundness 공식이 어떻게 미묘하게 달라지는지 비교하면 좋다.