* Basics of (especially "functional"-style) programming: including pattern matching, recursive definitions, abstract datatypes, **modularity, separating interfaces from implementation**
* The syntax and proof theory of the untyped lambda calculus; at least some discussion of its semantics
* Different **evaluation-order strategies** for formal systems, different "normalizing" properties
-* Combinatorial logic, or the dispensability of variables
+* Combinatory logic, or the dispensability of variables
* Recursive definitions and recursive types, fixed-point combinators
* Other **type sophistication**: abstract datatypes, polymorphic types, perhaps dependent types
* **Mutation** and imperative/iterative idioms
The logical systems we'll be looking at include:
* the so-called "pure" or untyped (monotyped?) lambda calculus
-* combinatorial logic
+* combinatory logic
* the simply-typed lambda calculus
* polymorphic types with System F