+ Reduction reltions
  -- see midterm 2

+ Curry-Howard
  -- Agda Cheat Sheet
  -- ADT constructors ~= inference rules

+ Prolog ... ie Oz
  -- computation ~= inference rules

+ Fundamental of PL paradagims
  -- jargon: strongly typed, unityped
  -- State, environments, reductions
  -- type theory
  -- type inference; e.g., "3" + 2
  -- polymorphism in OOP & FP
     -- duck typing a la Ruby
     
+ Algebraic Data Types [AgdaCheatSheet]
  -- induction
  -- recursion
  -- Exercise: Argue that Nat-induction
               is just for-loops.
  -- Pattern matching < induction

+ Super simple coding
  -- Look at the midterms & hmwrks
  -- Be aware of infinite/lazy notions