From: Jim Pryor Date: Mon, 23 Aug 2010 21:25:31 +0000 (-0400) Subject: draft schedule X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=aaebaca77983fc743304e1bc7daf05f97179b56a draft schedule Signed-off-by: Jim Pryor --- diff --git a/schedule_of_topics.mdwn b/schedule_of_topics.mdwn index 034d2388..b2ae2d96 100644 --- a/schedule_of_topics.mdwn +++ b/schedule_of_topics.mdwn @@ -1 +1,98 @@ -To be added. +## Schedule of Topics ## + +This is very sketchy at this point, but it should give a sense of our intended scope. + + +### Introduction ### + +1. Declarative vs imperatival models of computation. +2. Variety of ways in which "order can matter." +3. Variety of meanings for "dynamic." +4. Schoenfinkel, Curry, Church: a brief history +5. Functions as "first-class values" +6. "Curried" functions + +### The "pure" or untyped lambda calculus ### + +1. Beta reduction +2. Subtitution; using alpha-conversion and other strategies +3. Conversion versus Reduction +4. Eta reduction and "extensionality" +5. Different evaluation strategies +6. Strongly normalizing vs weakly normalizing vs non-normalizing; Church-Rosser Theorem(s) + +7. Encoding pairs (and triples and ...) +8. Encoding booleans +9. Church-like encodings of numbers, defining addition and multiplication +10. Defining the predecessor function; alternate encodings for the numbers +11. Homogeneous sequences or "lists"; how they differ from pairs, triples, etc. +12. Representing lists as pairs +13. Representing lists as folds +14. Typical higher-order functions: map, filter, fold + +15. Recursion exploiting the fold-like representation of numbers and lists +16. General recursion using omega +17. The Y combinator(s); more on evaluation strategies + +18. Introducing the notion of a "continuation", which technique we'll now already have used a few times + +### Types ### + +1. Product or record types, e.g. pairs and triples +2. Sum or variant types; tagged or "disjoint" unions +3. Maybe/option types +4. Zero/bottom types +5. Unit type +6. Inductive types (numbers, lists) +7. "Pattern-matching" or type unpacking + +8. The simply-typed lambda calculus + +9. Parametric polymorphism, System F, "type inference" + +10. [Phil/ling application] inner/outer domain semantics for positive free logic + + +11. [Phil/ling application] King vs Schiffer in King 2007. pp 103ff +12. [Phil/ling application] King and Pryor on that clauses, predicates vs singular property-designators +13. Possible excursion: Frege's "On Concept and Object" + +14. Curry-Howard isomorphism between simply-typed lambda and intuitionistic propositional logic + +15. The types of continuations; continuations as first-class values +16. [Phil/ling application] Partee on whether NPs should be uniformly interpreted as generalized quantifiers, or instead "lifted" when necessary. Lifting = a CPS transform. + +17. Dependent types + +### Side-effects and mutation ### + +1. What difference imperativity makes +2. Monads we've seen, and the "monadic laws" (computer science version) +3. Side-effects in a purely functional setting, via monads +4. The basis of monads in category theory +5. Other interesting monads: reader monad, continuation monad + +6. [Phil/ling application] Monsters and context-shifting, e.g. Gillies/von Fintel on "ifs" +7. Montague / Yoad Winter? (just have this written down in my notes, I assume Chris will remember the reference) + +8. Passing by reference +9. [Phil/ling application] Fine and Pryor or "coordinated contents" + + +### Continuations (continued) ### + +1. Using CPS to handle abortive computations +2. Using CPS to do other handy things, e.g., coroutines +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) +4. Delimited continuations +5. [Phil/ling application] Barker/Shan on donkey anaphora + + +### Preemptively parallel computing and linear logic ### + +1. Basics of parallel programming: semaphores/mutexes +2. Contrasting "preemptive" parallelism to "cooperative" parallelism (coroutines, above) +3. Linear logic +4. [Phil/ling application] Barker on free choice + +