*This page will summarize the major "topics" (bits of conceptual technology) the course will cover, as well as some connecting "themes" that show up in different ways in several of the topics.*

<!--
See also the page on [[ applications]].

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