Teaching

CS 4392: Programming Languages, Georgia Tech, Summer 2020

CS 6390: Programming Languages, Georgia Tech, Fall 2019

I developed and co-taught the gradate-level version of this course with my advisor, and later adapted the curriculum for the undergraduate level, for which I was the instructor. Topics include the fundamentals of semantics and type systems, the simply typed λ-calculus, dependent types, applications to modern programming languages, and an introduction to the Coq proof assistant.

Textbooks

Lecture topics and readings (graduate version)

  • Syntax and Structural Semantics
    PFPL 1, 4.1, 5.1, 5.2; TAPL 3
  • Coq Proof Assistant
    SF Preface, Basics
  • Contextual and Evaluation Semantics
    PFPL 5.3, 7.1, 7.2
  • Untyped λ-Calculus
    PFPL 21; TAPL 5
  • Type Systems
    PFPL 4.2, 6, 7.2, 7.3; TAPL 8
  • Substitution Lemma; Coq Tactics
    PFPL 4.3; SF Lists, Poly, Tactics, Logic
  • Simply Typed λ-Calculus
    PFPL 10, 11; TAPL 9.1-9.3, 11.1-11.10
  • More Finite Types; Termination
    TAPL 12
  • Inductive Types
    PFPL 15.1; TAPL 20
  • Coinductive Types
  • Hoare Logic
  • Language Definitions in Coq
    SF IndProp, Imp
  • Parametric Polymorphism
    PFPL 16; TAPL 23
  • Dependent Types
    PFPL 17; TAPL 24; SF ProofObjects
  • References
    TAPL 13
  • Objects
    TAPL 18
  • Subtyping
    TAPL 15
  • Featherweight Java
    TAPL 19
  • Featherweight X10
    Lee and Palsberg, PPoPP '10
  • Substructural Types
  • CSP and Go
  • Data Races and Deadlocks

Lecture topics (undergraduate version)

  • Syntax and Structural Semantics
  • Substitution; Intro to Coq
  • Contextual and Reduction Semantics
  • Type Systems
  • Untyped λ-Calculus
  • STLC with Products and Sums
  • More Finite Types; Termination
  • Inductive Types
  • Coninductive Types
  • Parametric Polymorphism
  • Calculus of Constructions and Equality
  • Hoare Logic
  • Weakest Pre-conditions