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.      Substitution; using alpha-conversion and other strategies
  17 3.      Conversion versus reduction
  18 4.      Eta reduction and "extensionality"
  19 5.      Different evaluation strategies (call by name, call by value, etc.)
  20 6.      Strongly normalizing vs weakly normalizing vs non-normalizing; Church-Rosser Theorem(s)
  21 6.      Lambda calculus compared to combinatorial logic
  22
  23 7.      Encoding pairs (and triples and ...)
  24 8.      Encoding booleans
  25 9.      Church-like encodings of numbers, defining addition and multiplication
  26 10.     Defining the predecessor function; alternate encodings for the numbers
  27 11.     Homogeneous sequences or "lists"; how they differ from pairs, triples, etc.
  28 12.     Representing lists as pairs
  29 13.     Representing lists as folds
  30 14.     Typical higher-order functions: map, filter, fold
  31
  32 15.     Recursion exploiting the fold-like representation of numbers and lists ([deforestation](http://en.wikipedia.org/wiki/Deforestation_%28computer_science%29), [zippers](http://en.wikipedia.org/wiki/Zipper_%28data_structure%29))
  33 16.     General recursion using omega
  34 17.     The Y combinator(s); more on evaluation strategies
  35
  36 18.     Introducing the notion of a "continuation", which technique we'll now already have used a few times
  37
  38 ## Types ##
  39
  40 1.      Product or record types, e.g. pairs and triples
  41 2.      Sum or variant types; tagged or "disjoint" unions
  42 3.      Maybe/option types; representing "out-of-band" values
  43 4.      Zero/bottom types
  44 5.      Unit type
  45 6.      Inductive types (numbers, lists)
  46 7.      "Pattern-matching" or type unpacking
  47
  48 8.      The simply-typed lambda calculus
  49
  50 9.      Parametric polymorphism, System F, "type inference"
  51
  52 10.     [Phil/ling application] inner/outer domain semantics for positive free logic
  53         <!-- <http://philosophy.ucdavis.edu/antonelli/papers/pegasus-JPL.pdf> -->
  54
  55 11.     [Phil/ling application] King vs Schiffer in King 2007, pp 103ff. [which paper?](http://rci.rutgers.edu/~jeffreck/pub.php)
  56 12. [Phil/ling application] King and Pryor on that clauses, predicates vs singular property-designators
  57 13.     Possible excursion: [Frege's "On Concept and Object"](http://www.persiangig.com/pages/download/?dl=http://sahmir.persiangig.com/document/Frege%27s%20Articles/On%20Concept%20And%20object%20%28Jstore%29.pdf)
  58
  59 14.     Curry-Howard isomorphism between simply-typed lambda and intuitionistic propositional logic
  60
  61 15.     The types of continuations; continuations as first-class values
  62 16.     [Phil/ling application] Partee on whether NPs should be uniformly interpreted as generalized quantifiers, or instead "lifted" when necessary. Lifting = a CPS transform.
  63 17.     [Phil/ling application] Expletives
  64
  65 18.     Some references:
  66        * [de Groote on the lambda-mu calculus in linguistics](http://www.loria.fr/%7Edegroote/papers/amsterdam01.pdf)
  67        * [on donkey anaphora and continuations](http://dx.doi.org/10.3765/sp.1.1)
  68        * [Wadler on symmetric sequent calculi](http://homepages.inf.ed.ac.uk/wadler/papers/dual-reloaded/dual-reloaded.pdf)
  69
  70 19.     Dependent types
  71
  72 ## Side-effects and mutation ##
  73
  74 1.      What difference imperativity makes
  75 2.      Monads we've already seen, and the "monadic laws" [computer science version: Wadler](http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf)
  76 3.      Side-effects in a purely functional setting, via monads
  77 4.      The basis of monads in category theory
  78 5.      Other interesting monads: reader monad, continuation monad
  79
  80 6.      [Phil/ling application] Monsters and context-shifting, e.g. Gillies/von Fintel on "ifs" [not sure which paper]
  81 7.      Montague / Ben-avi and Winter,  [A modular approach to intensionality](http://citeseerx.ist.psu.edu/viewdocsummary?doi=10.1.1.73.6927)
  82
  83 8.      Passing by reference
  84 9.      [Phil/ling application] Fine and Pryor on "coordinated contents" (see, e.g., [Hyper-Evaluativity](http://www.jimpryor.net/research/papers/Hyper-Evaluativity.txt))
  85
  86 ## Continuations (continued) ##
  87
  88 1.      Using CPS to handle abortive computations (think: presupposition failure, expressives)
  89 2.      Using CPS to do other handy things, e.g., coroutines
  90 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)
  91 4.      Delimited (quantifier scope) vs undelimited (expressives, presupposition) continuations
  92 5.      [Phil/ling application] [Barker/Shan on donkey anaphora](http://dx.doi.org/10.3765/sp.1.1)
  93
  94 ## Preemptively parallel computing and linear logic ##
  95
  96 1.      Basics of parallel programming: semaphores/mutexes
  97 2.      Contrasting "preemptive" parallelism to "cooperative" parallelism (coroutines, above)
  98 3.      Linear logic
  99 4.      [Phil/ling application] Barker on free choice, imperatives
 100
 101