_overview.mdwn

   1 *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.*
   2
   3 <!--
   4 See also the page on [[ applications]].
   5
   6 Once we get up and running, the central focii of the course will be
   7 **continuations**, **types**, and **monads**. One of the on-going themes will
   8 concern evaluation order and issues about how computations (inferences,
   9 derivations) unfold in (for instance) time.  The key analytic technique is to
  10 form a static, order-independent model of a dynamic process. We'll be
  11 discussing this in much more detail as the course proceeds.
  12
  13 The logical systems we'll be looking at include:
  14
  15 *       the "pure"/untyped lambda calculus
  16 *       combinatorial logic
  17 *       the simply-typed lambda calculus
  18 *       polymorphic types with System F
  19 *       some discussion of dependent types
  20 *       if time permits, "indeterministic" or "preemptively parallel" computation and linear logic
  21
  22
  23 Other keywords:
  24         recursion using the Y-combinator
  25         evaluation-order stratgies
  26         normalizing properties
  27         the Curry-Howard isomorphism(s)
  28         monads in category theory and computation
  29 -->