This is very sketchy at this point, but it should give a sense of our intended scope. 14. Curry-Howard isomorphism between simply-typed lambda and intuitionistic propositional logic

15. The types of continuations; continuations as first-class values ## Continuations ## 0. [Phil/ling application] Partee on whether NPs should be uniformly interpreted as generalized quantifiers, or instead "lifted" when necessary. Lifting = a CPS transform. 1. Using CPS to handle abortive computations (think: presupposition failure, expressives) 2. Using CPS to do other handy things, e.g., coroutines (cooperative threading) 3. Making evaluation order explicit with continuations 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) 6. The continuation monad ## 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, "logical resource management" 4. [Phil/ling application] Barker on free choice, imperatives ##Other## 17. [Phil/ling application] Expletives

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