4190.310 Programming Languages

Lecture Movies

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

목표 Objectives

다양한 프로그래밍 언어들이 품고있는 공통된 원리들은 무엇인가? 현재의 프로그래밍 언어들은 얼마만큼 미개한가? 좀더 나아지기 위해서 필요한 것들은 무엇인가? 새로운 프로그래밍 환경을 효과적으로 운용할 수 있는 언어는 무엇인가? 이 강의에서는 이와같은 질문들에 대한 답을 익히거나, 좋은 답을 만들어내기 위해서 필요한 소양을 닦게 됩니다.

Part 0: 기초

• 프로그래밍 언어란 무엇인가
  • 강의의 목표
  • 강의 내용 개괄
  • 프로그래밍 언어란 무엇인가
  • 프로그래밍 언어의 쓰임새
  • 프로그래밍 언어 배우기
• 귀납법(inductive definitions & inductions)
  • 귀납적인 생각방식
  • 귀납적 정의의 표현법
  • 귀납적 정의 예제
  • 프로그래밍 언어와 귀납법
  • 요약된 문법구조(abstract syntax)
  • 프로그램 의미구조(semantics)
  • 귀납적으로 정의된 집합
  • 귀납적으로 정의된 집합 예제
  • 귀납법으로 증명하기
  • 귀납 증명 예제
• 추론규칙(inference rules)
  • 집합의 정의와 추론규칙(inference rule)
  • 집합의 정의와 추론규칙 예제
  • 추론규칙의 평가, 증명나무(proof tree)
  • 안전성(soundness)과 완전성(completeness)
  • 안전성과 완전성과의 관계
  • 형식논리(formal logic) 표기법

Part I: 상식에 기반한 언어 디자인. 기계중심의 언어, 명령형 언어(imperative language)

• 문법, 의미
  • 명령형 언어 소개
  • 추론 규칙에 의한 의미 정의 1
  • 추론 규칙에 의한 의미 정의 2
  • 메모리와 함수의 의미 정의 1
  • 메모리와 함수의 의미 정의 2
  • 실제 코드 예제로 의미 파악하기
  • 설탕 구조(syntactic sugar)
• 변수, 프로시저(procedure), 유효범위(scope)
  • 변수와 유효범위
  • 유효범위를 정의하는 방법 1
  • 유효범위를 정의하는 방법 2
  • 유효범위 예제
  • 묶여있는 이름(bound variable)과 자유로운 이름(free variable)
  • 프로시저 소개
  • 프로시저를 표현하는 문법
  • 프로그램의 버그
  • 동적인 유효범위(dynamic scoping), 함수 인자 넘기기(parameter passing)
  • 재귀 프로시저(recursive procedure)
  • 메모리 주소의 유효기간(lifetime)
• 타입 시스템(type system)
  • 타입 검사(type checking)의 동기
  • 안전성(soundness)과 완전성(completeness)
  • 타입 검사 1
  • 타입 검사 2
  • 멈춤 문제(halting problem) 1
  • 멈춤 문제(halting problem) 2
  • 타입에 대한 간략한 소개
  • 논리와 계산
  • 타입 추론하기
  • K- 언어와 타입 시스템
  • K- 언어 예제
  • K- 타입 추론 예제 1
  • K- 타입 추론 예제 2
  • 레코드 타입
  • 레코드 타입 예제, 타입 추론
  • 타입 안전성(type safety)
  • K- 언어 전체 의미 파악 예제
• 메모리 관리(memory management)
  • 메모리 관리. 왜 필요한가?
  • 메모리 누수(memory leak)와 메모리 재활용(garbage collection)
  • 메모리 재활용 과정
  • 메모리 재활용 알고리즘
  • "mark & sweep" 알고리즘
  • "stop & copy" 알고리즘
• 번역(translation)과 가상 기계(virtual machine)
  • 용어 정의 및 소개
  • 프로그램 의미로 본 번역의 조건
  • 예제: 정수식, 스택머신
  • 예제: K-- 에서 SM5 로의 변환
  • 언어의 번역
  • 강의 전반부 마무리 및 강의 후반부 소개

Part II: 이론에 기반한 언어 디자인. 값중심의 언어(applicative language)

• 이론에 기반한 언어
  • 프로그래밍언의 모델: 람다 계산법(Lambda Calculus)
  • 람다계산법 소개
  • 자유 변수와 치환
  • 자유 변수와 치환 예제
  • 계산법 정의
  • 계산끝난 식(normal form)
  • 끝을 내는 계산법(normal-order reduction)
  • 끝을 내는 계산법 예
  • 람다 계산법과 기계적인 계산
  • 재귀 함수의 표현
  • 재귀 함수 표현 예제
  • 의미 정의
  • 소극적 계산법(lazy evaluation)과 적극적 계산법(eager evaluation)
  • 값중심의 언어(applicative language)
  • 의미 정의, 설탕 구조
• 단순 타입 추론 시스템(simple type inference system)
  • 타입 추론(type inference)
  • 간단한 타입 추론 예제
  • 함수의 타입, 단형타입(monomorphic type), 다형타입(polymorphic type)
  • 타입 추론시 주목해야 할 점들
  • 타입 시스템의 올바름 증명
  • 진행정리(progress lemma)와 보존정리(preservation lemma) 1
  • 타입 추론 예제
  • 진행정리(progress lemma)와 보존정리(preservation lemma) 2
  • 진행정리의 증명 1
  • 진행정리의 증명 2
  • 치환정리(substitution lemma)
  • 타입 추론의 올바름 증명
  • 타입 추론 알고리즘 예제
  • 타입 추론 알고리즘 직관: 방정식 풀기 1
  • 타입 추론 알고리즘 직관: 방정식 풀기 2
  • 추론 규칙의 구현
  • 타입 연립 방정식 세우기
  • 타입 연립 방정식 세우기 예제
  • 추론 규칙의 올바름 증명
  • 동일화(unification) 알고리즘
  • 동일화 알고리즘은 충실한 구현
• 다형 타입 추론(polymorphic type inference)
  • 함부로 다형 타입으로 일반화하면 불안전
  • let-다형(let-polymorphic) 타입 시스템
  • 타입 추론 규칙
  • 타입 추론 규칙 예제 1
  • 타입 추론 규칙 예제 2
  • 다형 타입 유추 알고리즘 W 1
  • 다형 타입 유추 알고리즘 W 2
  • 다형 타입 유추 알고리즘 M
  • 기계중심 언어의 다형 타입 예제 1
  • 기계중심 언어의 다형 타입 예제 2
  • 기계중심 언어의 다형 타입 추론 1
  • 기계중심 언어의 다형 타입 추론 2
• 계층타입 시스템(subtype system)
  • 소개 및 간단한 예제
  • 타입 추론 규칙
  • 물건중심 언어(object oriented language)와의 관계 1
  • 물건중심 언어(object oriented language)와의 관계 2
• 물건중심의 언어(object-oriented language)
  • 유일한 특성: 상속(inheritance)
  • 실행중 결정되는 함수의 실체(late binding, dynamic binding)
• 강의 마무리: 강의 리뷰