Show The Graduate Center Menu

Programming Languages & Their Implementation

Instructor: Assistant Professor Liang Huang

Course Description

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

Learning Goals

  • Be able to write simple programs and type systems in Haskell and appreciate the functional programming style

  • Be able to understand and produce inductive proofs for recursive structures

  • Be able to understand and define basic operational semantics

  • Be able to do derivations on untyped λ-calculus

  • Be able to formulate and prove type safety theorems

  • Be able to formulate and reason about key object oriented programming features


  • Weekly Homeworks: 20%

  • Quiz: 7%

  • Midterm: 20%

  • Quiz II: 10+5=15%

  • Final: 28%

  • Class Participation: 10%