CS 4392: Programming Languages, Georgia Tech, Summer 2020
CS 6390: Programming Languages, Georgia Tech, Fall 2019
I developed and cotaught the gradatelevel 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
 Software Foundations, vol. 1, Pierce et al.
 Practical Foundations for Programming Languages, 2nd ed., Harper (graduatelevel only)
 Types and Programming Languages, Pierce (graduatelevel only)
Lecture topics and readings (graduate version)

Syntax and Structural SemanticsPFPL 1, 4.1, 5.1, 5.2; TAPL 3

Coq Proof AssistantSF Preface, Basics

Contextual and Evaluation SemanticsPFPL 5.3, 7.1, 7.2

Untyped λCalculusPFPL 21; TAPL 5

Type SystemsPFPL 4.2, 6, 7.2, 7.3; TAPL 8

Substitution Lemma; Coq TacticsPFPL 4.3; SF Lists, Poly, Tactics, Logic

Simply Typed λCalculusPFPL 10, 11; TAPL 9.19.3, 11.111.10

More Finite Types; TerminationTAPL 12

Inductive TypesPFPL 15.1; TAPL 20

Coinductive Types

Hoare Logic

Language Definitions in CoqSF IndProp, Imp

Parametric PolymorphismPFPL 16; TAPL 23

Dependent TypesPFPL 17; TAPL 24; SF ProofObjects

ReferencesTAPL 13

ObjectsTAPL 18

SubtypingTAPL 15

Featherweight JavaTAPL 19

Featherweight X10Lee 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 Preconditions