X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=schedule_of_topics.mdwn;h=d4c94db25ce5d820a289e2cc4d471b0c971a8dcf;hp=b2ae2d9666f2f489958f7181a72f69b4703ca018;hb=f5c65211617c8e04e87d3009f220f6457a76e9ff;hpb=aaebaca77983fc743304e1bc7daf05f97179b56a;ds=sidebyside diff --git a/schedule_of_topics.mdwn b/schedule_of_topics.mdwn index b2ae2d96..d4c94db2 100644 --- 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. -### Introduction ### +## Introduction ## 1. Declarative vs imperatival models of computation. 2. Variety of ways in which "order can matter." @@ -12,7 +10,7 @@ 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 -### The "pure" or untyped lambda calculus ### +## The "pure" or untyped lambda calculus ## 1. Beta reduction 2. Subtitution; using alpha-conversion and other strategies @@ -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 -### Types ### +## Types ## 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) @@ -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 -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" @@ -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. +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. 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) @@ -79,7 +83,7 @@ This is very sketchy at this point, but it should give a sense of our intended s 9. [Phil/ling application] Fine and Pryor or "coordinated contents" -### Continuations (continued) ### +## Continuations (continued) ## 1. Using CPS to handle abortive computations 2. Using CPS to do other handy things, e.g., coroutines @@ -88,7 +92,7 @@ This is very sketchy at this point, but it should give a sense of our intended s 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)