--- /dev/null
+
+<!--
+Once we get up and running, the central focii of the course will be
+**continuations**, **types**, and **monads**. One of the on-going themes will
+concern evaluation order and issues about how computations (inferences,
+derivations) unfold in (for instance) time. The key analytic technique is to
+form a static, order-independent model of a dynamic process. We'll be
+discussing this in much more detail as the course proceeds.
+
+The logical systems we'll be looking at include:
+
+* the "pure"/untyped lambda calculus
+* combinatorial logic
+* the simply-typed lambda calculus
+* polymorphic types with System F
+* some discussion of dependent types
+* if time permits, "indeterministic" or "preemptively parallel" computation and linear logic
+
+
+Other keywords:
+ recursion using the Y-combinator
+ evaluation-order stratgies
+ normalizing properties
+ the Curry-Howard isomorphism(s)
+ monads in category theory and computation
+-->