XD2: Designing Lesson for Typesystem Teaching

The "concepts of programming language" course provides an introduction to functional programming and programming language theory. What lessons could a follow-up course with more info on programming language theory, modern type systems, and advancend functional programming concepts look like? Attached are some ideas:

lecture 1: first-order languages
  theory
    arithmetic,
    booleans,
    products,
    sums,
    stack vs register languages / SKI / mu calculus 
    pattern matching
    formation / introduction / elimination / eta / beta / commutative rules
    inference rules
    harmony
  lean
    peano numbers
    binary numbers
    equivalence

lecture 2: lambda calculus
  let binding
  - capture avoiding substitution
  - first-order syntax: namefull, nameless
  - (parametric) higher-order syntax

  functions
  - untyped lambda calculus
  - simply typed lambda calculus
  - environment-passing-style evaluation

lecture 3 semantics
  abstract machine
    ...
  relational semantics
    microstep semantics
    smallstep semantics
    bigstep semantics
    equational theory
  function semantics
    definitional interpreter
    denotational semantics
  program logic
    predicate transformer
  logic and compilation
    continuation passing style
    environment passing style

lecture 4
  progress and preservation
  normalization / partial evaluation

lecture 5
  polymoprhism
  parametricity
  free theorems
  dinaturality

lecture 4 effects and coeffects
  linear and uniqueness types
  quantitative type theory

Other inspiration could be the course called "introduction to type systems" that was given a few years ago. We might find together, or I can search for some other good books or courses on the internet, to design inspirations for.

Goals

• look for other courses on the topic and compare and identify what people teach, and from your perspective as a student consider how one can make it approachable/interesting
• you learning the stuff with the material found online
• you trying yourself at designing a few lesson/homework/solution packages that could fit into such a lecture
• if we notice after a few weeks, that this topic doesnt work out and the scope is no good fit for you, we can turn it into a regular "Advanced Functional Programming in Lean" project topic (see other topic with that name)

References

• Programming Language Theory (link collection)
• Introduction to Type Systems. Peters. Moodle 2021/22

For programming language theory, trying out Lean for some homework/solutions in should be a good idea:

• https://lean-lang.org/
• https://lean-lang.org/functional_programming_in_lean/
• https://leanprover-community.github.io/mathematics_in_lean/

For other tasks things, specific languages with the exact feature that is covered by the topic may be better.