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 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

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

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

1. 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; representing "out-of-band" values 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. [which paper?](http://rci.rutgers.edu/~jeffreck/pub.php) 12. [Phil/ling application] King and Pryor on that clauses, predicates vs singular property-designators 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)

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. [Phil/ling application] Expletives