4190.310 Programming Languages (Spring 2026)

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

강의: 화/목 09:30-10:45 @ 302동 209호
면담: 화/목 강의후, 강의실 주변

목표 Objectives

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

규정 Policy

숙제: 90%, 기타: 10%, 챌린지.

성적은 절대평가입니다.
프로그램 숙제가 베낀것으로 적발되면 숙제점수 모두 0점 처리됩니다. 프로그램이 얼마만큼 비슷한지를 자동으로 감별해주는 소프트웨어 CloneChecker가 사용됩니다.

숙제 Homeworks

프로그래밍 숙제:
- 프로그램 숙제는 OCaml로 작성합니다.
- 왜 ML로 실습하는가?
- 컴퓨터를 통해 제출합니다.
- 제출기한을 지나 48시간 이내로 늦어지면 10% 감점. 그 이후의 숙제는 받지 않습니다.
- 프로그램 숙제가 복제로 판정되면, 숙제 점수 모두가 0점 처리됩니다.
- 프로그램 복제여부는 CloneChecker에 의해 자동으로 감별된다.
- Clonechecker가 검사하는 숙제 코드들 = 여러분이 제출한 코드 + 역대 학생들의 코드 + LLM이 다양하게 만드는 코드
논술 숙제: 자료를 읽고 요약하고 느낀점을 논술하는 숙제입니다.
- 글쓰기 핵심 요령, 이메일 에티켓
챌린지: 여러분 정도라면 한번 도전해 볼 만한 문제들입니다. 한 문제를 올바르게 해결하면 최종 성적이 1-3 단계 상승합니다.
숙제/챌린지 시간표
- HW1: due 3/14 24:00. OCaml Programming I
- HW2: due 3/21 24:00. OCaml Programming II
- HW3: due ~~4/04~~ 4/06 24:00. Tiny imperative K-- interpreter (K-- definition)
- HW4: due 4/18 24:00. Imperative K- interpter, K- programming, new treasure island (K- definition)
- HW5: due ~~5/02~~ 5/04 00:00 (PDF on-line submission) + 09:30 (print in-class submission).
- HW6: due 5/16 24:00. Translation, virtual machine language, garbage collection
- HW7: due 5/30 24:00. Continuation, de-sugaring exceptions, M interpreter, M sound simple type system, M definition
- HW8: due 6/13 24:00. M let-polymorphic type system, RosettaX engine
- Challenges: due 6/22 16:00.

조교팀 TA team

안중원, 신채환, 302동312-2호
조교는 수강생 여러분을 도와주기 위해서 있습니다.
조교는 과목 웹보드와 조교페이지를 통해서 정보를 공지하고 여러분의 어려움을 돕습니다.
조교는 여러분의 숙제와 퀴즈를 채점합니다.

진도및 자료 Slides & Resources

강의에서는 가능하면 [쉬운전문용어]를 사용합니다.
실라부스
교재/Textbook
Notes on Programming Languages, Kwangkeun Yi
참고서/Reference (중앙도서관 지정도서)
- Practical Foundations for Programming Languages (2nd Edition), Robert Harper, Cambridge University Press, 2016.
To view/print PDF files: Acrobat Reader

Part 0	[1.pdf (handout), 2.pdf (handout), 2-1.pdf ]
	language, syntax, semantics
	abstract syntax, concrete syntax, inductive definitions
	logic systems, inference rules, inductions

Part I	[3.pdf (handout), 3-1.pdf, 4-1.pdf (handout), remind-overview.pdf (handout), 4-2.pdf (handout), 4-3.pdf (handout)]
	imperative language: basic syntax, inference rules as semantics

	scopes, environment
	static/dynamic scoping, parameter passing
	procedures, data structures
	role of types, static/dynamic type system
	memory leak, dangling pointer, garbage collection
	translation, virtual machine
Part II	[Overview: programming principles, languages, and tools (handout)]
	[Overview: two genesis, two programming pillars (handout)]
	[ 5-0.pdf (handout), 5-1.pdf (handout), 5-1simple-type.pdf (handout), 5-1poly-type.pdf, 5-1oo.pdf, 5-2curryhoward.pdf, 5-3.pdf ]
	language model: lambda calculus
	reduction strategies
	high-order applicative language
	safe type system, static type system, type discipline
	let-polymorphic type system, parametric polymorphism, subtype system
	type system as language design
	data abstraction, modularity
	translation, virtual machine
	essence of object-oriented language, object, inheritance, subtype polymorphism
	logic vs computation, curry-howard correspondence
	partial evaluation, staged programming
	overview, future issues