CS 258. Introduction to Programming Language Theory

1. Functional programming and typed lambda calculus (Chapter 2)
   1. Boolean, natural number, pairing and function expressions; definition of recursive functions using fixed-point operator (Section 2.2)
   2. Comparison of axiomatic, operational and denotational semantics (Section 2.3)
   3. Properties of reduction; deterministic symbolic interpreters (Section 2.4)
   4. Programming techniques, expressive power, limitations (Section 2.5)
2. Universal algebra and algebraic data types (Chapter 3)
   1. Algebraic terms, equations and algebras (Sections 3.1-3)
   2. Equational proof system, soundness and completeness (Section 3.4)
   3. Homomorphisms and initiality (Section 3.5)
   4. Aspects of algebraic theory of data types (Section 3.6)
3. Semantics of typed lambda calculus and recursion (Parts of Chapters 4 and 5)
   1. Presentation of context-sensitive syntax by typing rules (Sections 4.3.1, 4.3.2, 4.3.5)
   2. General models, summary of soundness and completeness (Sections 4.5.1-4)
   3. Domain-theoretic models of typed lambda calculus with fixed-point operators (Sections 5.1 and 5.2; Sections 5.3 and 5.4 time permitting)
4. Imperative programs (Chapter 6)
   1. Syntax of while programs; L-values and R-values (Section 6.2)
   2. Structured operational semantics (Section 6.3)
   3. Denotational semantics using typed lambda calculus with location and store types, fixed- point operator (Section 6.4)
   4. Partial correctness assertions. Soundness, relative completeness and example proofs (Section 6.5).