projects / lambda.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
links tweaking
[lambda.git] / schedule_of_topics.mdwn
diff --git a/schedule_of_topics.mdwn b/schedule_of_topics.mdwn
index d4c94db..50a9c33 100644 (file)
--- a/schedule_of_topics.mdwn
+++ b/schedule_of_topics.mdwn
@@ -13,26 +13,24 @@ This is very sketchy at this point, but it should give a sense of our intended s
 ## The "pure" or untyped lambda calculus ##
 
 1.     Beta reduction
 ## 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
+1.     Substitution; using alpha-conversion and other strategies
+1.     Conversion versus reduction
+1.     Eta reduction and "extensionality"
+1.     Different evaluation strategies (call by name, call by value, etc.)
+1.     Strongly normalizing vs weakly normalizing vs non-normalizing; Church-Rosser Theorem(s)
+1.     Lambda calculus compared to combinatorial logic<p>
+1.     Encoding pairs (and triples and ...)
+1.     Encoding booleans
+1.     Church-like encodings of numbers, defining addition and multiplication
+1.     Defining the predecessor function; alternate encodings for the numbers
+1.     Homogeneous sequences or "lists"; how they differ from pairs, triples, etc.
+1.     Representing lists as pairs
+1.     Representing lists as folds
+1.     Typical higher-order functions: map, filter, fold<p>
+1.     Recursion exploiting the fold-like representation of numbers and lists ([[!wikipedia Deforestation (computer science)]], [[!wikipedia Zipper (data structure)]])
+1.     General recursion using omega
+1.     The Y combinator(s); more on evaluation strategies<p>
+1.     Introducing the notion of a "continuation", which technique we'll now already have used a few times
 
 ## Types ##
 
 
 ## Types ##
 
@@ -42,61 +40,49 @@ This is very sketchy at this point, but it should give a sense of our intended s
 4.     Zero/bottom types
 5.     Unit type
 6.     Inductive types (numbers, lists)
 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"
-
+7.     "Pattern-matching" or type unpacking<p>
+8.     The simply-typed lambda calculus<p>
+9.     Parametric polymorphism, System F, "type inference"<p>
 10.    [Phil/ling application] inner/outer domain semantics for positive free logic
 10.    [Phil/ling application] inner/outer domain semantics for positive free logic
-       <!-- <http://philosophy.ucdavis.edu/antonelli/papers/pegasus-JPL.pdf> -->
-
-11.    [Phil/ling application] King vs Schiffer in King 2007, pp 103ff.
+       <!-- <http://philosophy.ucdavis.edu/antonelli/papers/pegasus-JPL.pdf> --><p>
+11.    [Phil/ling application] King vs Schiffer in King 2007, pp 103ff. [which paper?](http://rci.rutgers.edu/~jeffreck/pub.php)
 12. [Phil/ling application] King and Pryor on that clauses, predicates vs singular property-designators
 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
-
+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)<p>
+14.    Curry-Howard isomorphism between simply-typed lambda and intuitionistic propositional logic<p>
 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.
 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.    [Phil/ling application] Expletives
-
-18.    Misc references: Chris?
-       *       de Groeten on lambda-mu and linguistics?
-       *       on donkey anaphora and continuations
-       *       Wadler on symmetric sequent calculi
-
+17.    [Phil/ling application] Expletives<p>
+18.    Some references:
+       * [de Groote on the lambda-mu calculus in linguistics](http://www.loria.fr/%7Edegroote/papers/amsterdam01.pdf)
+       * [on donkey anaphora and continuations](http://dx.doi.org/10.3765/sp.1.1)
+       * [Wadler on symmetric sequent calculi](http://homepages.inf.ed.ac.uk/wadler/papers/dual-reloaded/dual-reloaded.pdf)
 19.    Dependent types
 
 ## Side-effects and mutation ##
 
 1.     What difference imperativity makes
 19.    Dependent types
 
 ## Side-effects and mutation ##
 
 1.     What difference imperativity makes
-2.     Monads we've seen, and the "monadic laws" (computer science version)
+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)
 3.     Side-effects in a purely functional setting, via monads
 4.     The basis of monads in category theory
 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)
-
+5.     Other interesting monads: reader monad, continuation monad<p>
+6.     [Phil/ling application] Monsters and context-shifting, e.g. Gillies/von Fintel on "ifs" [not sure which paper]
+7.     Montague / Ben-avi and Winter,  [A modular approach to intensionality](http://citeseerx.ist.psu.edu/viewdocsummary?doi=10.1.1.73.6927)<p>
 8.     Passing by reference
 8.     Passing by reference
-9.     [Phil/ling application] Fine and Pryor or "coordinated contents"
-
+9.     [Phil/ling application] Fine and Pryor on "coordinated contents" (see, e.g., [Hyper-Evaluativity](http://www.jimpryor.net/research/papers/Hyper-Evaluativity.txt))
 
 ## Continuations (continued) ##
 
 
 ## Continuations (continued) ##
 
-1.     Using CPS to handle abortive computations
+1.     Using CPS to handle abortive computations (think: presupposition failure, expressives)
 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)
 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
-
+4.     Delimited (quantifier scope) vs undelimited (expressives, presupposition) continuations
+5.     [Phil/ling application] [Barker/Shan on donkey anaphora](http://dx.doi.org/10.3765/sp.1.1)
 
 ## 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
 
 ## 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
+4.     [Phil/ling application] Barker on free choice, imperatives
 
 
 
 
NYU Lambda Wiki v2