I took this course when it was PL-focused in 2015ish! It starts with an in-depth exploration of the untyped lambda calculus (with the usual fixins like Church numerals, various combinators, etc), spending half a week or so on semantic expansion rules, reduction strategies, recursion, fixpoints, continuations, how one might encode state with only lexical closures, etc. After maybe the tenth lecture, the class takes a quick detour to talk about predicate logic, Hoare logic, dynamic logic, and Kleene algebra, before deriving a typed variant of the lambda calculus as an illustrative pathway into the latter half of the course featuring algebraic datatypes, unification, type inference, and the duality between formal logic propositions and typing systems. We explored subtype polymorphism, bisimulation, equirecursive equality, and closed on a gentle introduction to monads (of all things) and a teaser of category theory (which IMO should have been taught first but oh well).

As more of a math course than a computer engineering course, 6120 was a first-semester Ph.D. level class, and I certainly wouldn't recommend taking it unless you really wanted to dive deep into the depths of programming language implementation. Incoming students were expected to be fluent in discrete mathematics and formal proofwriting skills. I wasn't, so I found myself falling behind at the start even though I had some familiarity with lambda calculus and algebraic datatypes. You definitely benefit from a strong math background.