Programming Languages

Undergraduate / Graduate

This course is an introduction to scientific programming language design, whereby design choices are made according to rigorous and well-founded lines of reasoning. The curriculum includes the lambda calculus, type systems, formal semantics, logic and proof, and, time permitting, a light introduction to machine assisted formal reasoning. Practical exercises in writing language transformers reinforce the the theory. While this course is not a survey of different programming languages, we do examine the design decisions embodied by various popular languages in light of their underlying formal systems.