schedule_of_topics.mdwn

   1 This is very sketchy at this point, but it should give a sense of our intended scope.
   2
   3
   4 ## Introduction ##
   5
   6 1.      Declarative vs imperatival models of computation.
   7 2.      Variety of ways in which "order can matter."
   8 3.      Variety of meanings for "dynamic."
   9 4.      Schoenfinkel, Curry, Church: a brief history
  10 5.      Functions as "first-class values"
  11 6.      "Curried" functions
  12
  13 ## The "pure" or untyped lambda calculus ##
  14
  15 1.      Beta reduction
  16 2.      Subtitution; using alpha-conversion and other strategies
  17 3.      Conversion versus Reduction
  18 4.      Eta reduction and "extensionality"
  19 5.      Different evaluation strategies
  20 6.      Strongly normalizing vs weakly normalizing vs non-normalizing; Church-Rosser Theorem(s)
  21
  22 7.      Encoding pairs (and triples and ...)
  23 8.      Encoding booleans
  24 9.      Church-like encodings of numbers, defining addition and multiplication
  25 10.     Defining the predecessor function; alternate encodings for the numbers
  26 11.     Homogeneous sequences or "lists"; how they differ from pairs, triples, etc.
  27 12.     Representing lists as pairs
  28 13.     Representing lists as folds
  29 14.     Typical higher-order functions: map, filter, fold
  30
  31 15.     Recursion exploiting the fold-like representation of numbers and lists
  32 16.     General recursion using omega
  33 17.     The Y combinator(s); more on evaluation strategies
  34
  35 18.     Introducing the notion of a "continuation", which technique we'll now already have used a few times
  36
  37 ## Types ##
  38
  39 1.      Product or record types, e.g. pairs and triples
  40 2.      Sum or variant types; tagged or "disjoint" unions
  41 3.      Maybe/option types; representing "out-of-band" values
  42 4.      Zero/bottom types
  43 5.      Unit type
  44 6.      Inductive types (numbers, lists)
  45 7.      "Pattern-matching" or type unpacking
  46
  47 8.      The simply-typed lambda calculus
  48
  49 9.      Parametric polymorphism, System F, "type inference"
  50
  51 10.     [Phil/ling application] inner/outer domain semantics for positive free logic
  52         <!-- <http://philosophy.ucdavis.edu/antonelli/papers/pegasus-JPL.pdf> -->
  53
  54 11.     [Phil/ling application] King vs Schiffer in King 2007, pp 103ff.
  55 12. [Phil/ling application] King and Pryor on that clauses, predicates vs singular property-designators
  56 13.     Possible excursion: Frege's "On Concept and Object"
  57
  58 14.     Curry-Howard isomorphism between simply-typed lambda and intuitionistic propositional logic
  59
  60 15.     The types of continuations; continuations as first-class values
  61 16.     [Phil/ling application] Partee on whether NPs should be uniformly interpreted as generalized quantifiers, or instead "lifted" when necessary. Lifting = a CPS transform.
  62 17.     [Phil/ling application] Expletives
  63
  64 18.     Dependent types
  65
  66 ## Side-effects and mutation ##
  67
  68 1.      What difference imperativity makes
  69 2.      Monads we've seen, and the "monadic laws" (computer science version)
  70 3.      Side-effects in a purely functional setting, via monads
  71 4.      The basis of monads in category theory
  72 5.      Other interesting monads: reader monad, continuation monad
  73
  74 6.      [Phil/ling application] Monsters and context-shifting, e.g. Gillies/von Fintel on "ifs"
  75 7.      Montague / Yoad Winter? (just have this written down in my notes, I assume Chris will remember the reference)
  76
  77 8.      Passing by reference
  78 9.      [Phil/ling application] Fine and Pryor or "coordinated contents"
  79
  80
  81 ## Continuations (continued) ##
  82
  83 1.      Using CPS to handle abortive computations
  84 2.      Using CPS to do other handy things, e.g., coroutines
  85 3.      Making evaluation order explicit with continuations (could also be done earlier, but I think will be helpful to do after we've encountered mutation)
  86 4.      Delimited continuations
  87 5.      [Phil/ling application] Barker/Shan on donkey anaphora
  88
  89
  90 ## Preemptively parallel computing and linear logic ##
  91
  92 1.      Basics of parallel programming: semaphores/mutexes
  93 2.      Contrasting "preemptive" parallelism to "cooperative" parallelism (coroutines, above)
  94 3.      Linear logic
  95 4.      [Phil/ling application] Barker on free choice
  96
  97