schedule_of_topics.mdwn

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