(no commit message)

[lambda.git] / schedule_of_topics.mdwn

diff --git a/schedule_of_topics.mdwn b/schedule_of_topics.mdwn
index b2ae2d9..753c058 100644 (file)
--- a/schedule_of_topics.mdwn
+++ b/schedule_of_topics.mdwn
@@ -1,9 +1,7 @@
-## Schedule of Topics ##
-

 This is very sketchy at this point, but it should give a sense of our intended scope.
 
 
 This is very sketchy at this point, but it should give a sense of our intended scope.
 
 

-### Introduction ###
+## Introduction ##

 
 1.     Declarative vs imperatival models of computation.
 2.     Variety of ways in which "order can matter."
 
 1.     Declarative vs imperatival models of computation.
 2.     Variety of ways in which "order can matter."


@@ -12,13 +10,13 @@ This is very sketchy at this point, but it should give a sense of our intended s
 5.     Functions as "first-class values"
 6.     "Curried" functions
 
 5.     Functions as "first-class values"
 6.     "Curried" functions
 

-### The "pure" or untyped lambda calculus ###
+## The "pure" or untyped lambda calculus ##

 
 1.     Beta reduction
 
 1.     Beta reduction

-2.     Subtitution; using alpha-conversion and other strategies
+2.     Substitution; using alpha-conversion and other strategies

 3.     Conversion versus Reduction
 4.     Eta reduction and "extensionality"
 3.     Conversion versus Reduction
 4.     Eta reduction and "extensionality"

-5.     Different evaluation strategies
+5.     Different evaluation strategies (call by name, call by value, etc.)

 6.     Strongly normalizing vs weakly normalizing vs non-normalizing; Church-Rosser Theorem(s)
 
 7.     Encoding pairs (and triples and ...)
 6.     Strongly normalizing vs weakly normalizing vs non-normalizing; Church-Rosser Theorem(s)
 
 7.     Encoding pairs (and triples and ...)


@@ -36,11 +34,11 @@ This is very sketchy at this point, but it should give a sense of our intended s
 
 18.    Introducing the notion of a "continuation", which technique we'll now already have used a few times
 
 
 18.    Introducing the notion of a "continuation", which technique we'll now already have used a few times
 

-### Types ###
+## Types ##

 
 1.     Product or record types, e.g. pairs and triples
 2.     Sum or variant types; tagged or "disjoint" unions
 
 1.     Product or record types, e.g. pairs and triples
 2.     Sum or variant types; tagged or "disjoint" unions

-3.     Maybe/option types
+3.     Maybe/option types; representing "out-of-band" values

 4.     Zero/bottom types
 5.     Unit type
 6.     Inductive types (numbers, lists)
 4.     Zero/bottom types
 5.     Unit type
 6.     Inductive types (numbers, lists)


@@ -53,7 +51,7 @@ This is very sketchy at this point, but it should give a sense of our intended s
 10.    [Phil/ling application] inner/outer domain semantics for positive free logic
        <!-- <http://philosophy.ucdavis.edu/antonelli/papers/pegasus-JPL.pdf> -->
 
 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
+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"
 
 12. [Phil/ling application] King and Pryor on that clauses, predicates vs singular property-designators
 13.    Possible excursion: Frege's "On Concept and Object"
 


@@ -61,10 +59,16 @@ This is very sketchy at this point, but it should give a sense of our intended s
 
 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.    Some references: 
+       *       de Groote on the lambda-mu calculus in linguistics
+       *       on donkey anaphora and continuations
+       *       Wadler on symmetric sequent calculi

 
 

-17.    Dependent types
+19.    Dependent types

 
 

-### Side-effects and mutation ###
+## Side-effects and mutation ##

 
 1.     What difference imperativity makes
 2.     Monads we've seen, and the "monadic laws" (computer science version)
 
 1.     What difference imperativity makes
 2.     Monads we've seen, and the "monadic laws" (computer science version)


@@ -73,26 +77,26 @@ This is very sketchy at this point, but it should give a sense of our intended s
 5.     Other interesting monads: reader monad, continuation monad
 
 6.     [Phil/ling application] Monsters and context-shifting, e.g. Gillies/von Fintel on "ifs"
 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)
+7.     Montague / Ben-avi and Winter,  [A modular approach to intensionality](http://citeseerx.ist.psu.edu/viewdocsummary?doi=10.1.1.73.6927)

 
 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"

 
 
 
 

-### Continuations (continued) ###
+## Continuations (continued) ##

 
 

-1.     Using CPS to handle abortive computations
+1.     Using CPS to handle abortive computations (think: presupposition failure)

 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
+4.     Delimited (quantifier scope) vs undelimited (expressives, presupposition) continuations

 5.     [Phil/ling application] Barker/Shan on donkey anaphora
 
 
 5.     [Phil/ling application] Barker/Shan on donkey anaphora
 
 

-### Preemptively parallel computing and 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
 
 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