Show The Graduate Center Menu

Programming Languages


Professor Douglas Troeger


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. The course is intended for students from all areas of computer science who want an introduction to key concepts in the theory of programming languages. The plan is to develop introductory material, examples and case studies. The text is Types and Programming Languages, by Benjamin C. Pierce, MIT Press.

Topic List

  1. Background

    • Functional programming with OCaml

    • Inductive Proofs

  2. Basics

    • Operational semantics

    • The λ-calculus

  3. Type Systems

    • Basic types

    • Simply typed λ-calculus

    • Type safety

    • Subtyping

Learning Goals

  • Be able to write simple programs and type systems in OCaml 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 in the untyped and simply typed λ-calculus

  • Be able to formulate and prove type safety theorems

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


  • Class Presentations: 70%

  • Final: 30%