Programming Languages, Graduate Center, Fall 2014

Time and Location	Lectures: T 4:15pm-6:15pm, Room C415A Office Hour: TBD
Personnel	Instructor: Prof. Liang Huang (huang @ cs.qc) Teaching Assistant: Dezhong Deng (ddeng @ gc.cuny)
Prerequisites	1. (required) fluent in at least two languages among C/C++, Java, and Python. 2. (preferred) an undergraduate course on compilers and basic familiarity with predicate logic.
Textbook	Benjamin Pierce (2002). Types and Programming Languages (TAPL). MIT Press.
Grading	Weekly Homework: 20%. Quiz: 7%. Midterm I: 20%. Quiz II: 10+5=15%. Final: 28%. Class Participation: 10%.

Syllabus

This course introduces basic concepts and techniques in the foundational study of programming languages. The central theme is the view of individual programs and whole languages as mathematical objects about which precise claims may be made and proved. Particular topics include functional programming, operational semantics, λ-calculus, type systems and type safety, polymorphism and subtyping, and foundations of object-oriented programming.

Part 0: Background: Functional programming with Haskell; Inductive Proofs
Part I: Basics: Operational semantics; The λ-calculus
Part II: Type systems: Basic types; Simply typed λ-calculus; Type safety; Subtyping

Schedule

T Sep 2	Intro and Haskell: functions, list comprehensions, recursions, pattern-matching slides	HW1: Basic Haskell
T Sep 9	discussions of HW1 Haskell: types and basic type classes, recursive datastructures slides (including HW1 solutions)	HW2: More Haskell
T Sep 16	Inductive Proofs and Operational Semantics (TAPL Ch 1 and Ch 3) slides (including HW2 solutions)	HW3: Inductive Proofs & Operational Semantics
~~T Sep 23~~	Friday Schedule. No PL Class.
T Sep 30	Quiz (20 min). Intro to λ-calculus (TAPL Ch 5)	HW4: λ-calculus I
T Oct 7	Continue on λ-calculus (TAPL Ch 5); same slides as above	HW5: λ-calculus II
T Oct 14	More on λ-calculus (beyond TAPL): full beta-reduction, call-by-name Y-combinator, lists, behaviorial equivalence, inductive proofs about λ-calculus. slides	Review Questions I
T Oct 21	Midterm I	HW6
T Oct 28	Simple Types; Simply Typed Lambda Calculus	HW7 Haskell typechecker for the pair language
T Nov 4	Substitution Lemma; Typability	HW8
T Nov 11	Simple Extensions (unit, ascription, tuples, records, variants)	HW9
T Nov 18	References	HW10
T Nov 25	Quiz II (60 min) subtyping	HW11 ~~(also redo quiz2)~~
T Dec 2	More on subtyping
T Dec 9	Featherweight Java	HW12
T Dec 16	Final Review	review questions

First Exam

Review guidelines here.

Related Courses

Last year's offering (changes in this year: more Haskell, less untyped lambda-calculus, +algorithmic subtyping).
Benjamin Pierce, Software Foundations, University of Pennsylvania.
(very similar to ours, except for OCaml instead of Haskell, and covering more TAPL).
Subash Shanker, previous offerings of this course at CUNY.
(quite different, but with heavy overlap: Haskell, λ-calculus, operational semantics, basic type systems. His version also covers basic compiler theory and heavy Prolog).

Liang Huang

Last modified: Mon Aug 5 18:45:06 EDT 2014