Programming language foundations

Students will learn how to formalize common programming constructs using operational, denotational, and axiomatic models; to prove properties about programs using language-based reasoning tools; and to apply these ideas in the design of a new domain-specific language.

Note that the list of topics is tentative and different topics will be explored at different levels of detail. In class participation is strongly recommended.

Introduction and Mathematical Preliminaries

• Coures overview and motivation; sets, relations, functions, induction, etc.

Operational Semantics

• Large and small-step semantics; evaluation rules; proofs by induction.

Denotational Semantics

• Relational models; fixpoints; relationship to operational semantics

Axiomatic Semantics

• Partial and total correctness; Hoare logic; soundness and relative completeness

Imperative Features

• Pointers and heaps; separation logic

Lambda Calculus

• Syntax and semantics; substitution; encodings; fixed-point combinators

Type Systems

• Typing rules; type soundness; normalization

Polymorphism

• System F; type inference; relational parametricity

Continuations

• Continuation-passing style; exceptions and control operators; compilation

Effects

• Monads, effect handlers

Relational Reasoning

• Program equivalence; algebraic methods; relational logics

Concurrency

• Interleaving semantics; message-passing; bisimulation

Domain-Specific Languages

• Case studes from selected domains (e.g., databases, graphics, networking, etc.)

Victory Lap

• Project presentations; research in programming languages