overview.mdwn

   1 This page aims to 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 ### Topics ###
   4
   5 * Basics of (especially "functional"-style) programming: including pattern matching, recursive definitions, abstract datatypes, **modularity, separating interfaces from implementation**
   6 * The syntax and proof theory of the untyped lambda calculus; at least some discussion of its semantics
   7 * Different **evaluation-order strategies** for formal systems, different "normalizing" properties
   8 * Combinatory logic, or the dispensability of variables
   9 * Recursive definitions and recursive types, fixed-point combinators
  10 * Other **type sophistication**: abstract datatypes, polymorphic types, perhaps dependent types
  11 * **Mutation** and imperative/iterative idioms
  12 * **Monads**, especially as a way to **represent "dynamic" computation using "static" or declarative idioms**
  13 * The origin of monads in category theory
  14 * **Controlling evaluation order and effects**, especially by means of **continuations**
  15 * Giving **order-independent characterizations of an order of evaluation**
  16 * Perhaps some of the relations between typed programming languages and logics (the "Curry-Howard" correspondence or "isomorphism" [sic])
  17 * Going back and forth between **representing a computational idiom *as a function* versus *as a static structure*&nbsp;**
  18 * We'll link to, but probably not discuss, material for JP's logic class about formal grammars, automata, and decidability
  19 * The different styles in which computer scientists give **"semantics" for their languages**, and how this relates to what we think of as semantics
  20 * If time permits, "indeterministic" or "preemptively parallel" computation and linear logic
  21 * If time permits, "dynamic" or "epistemic" logics
  22
  23
  24 ### Themes ###
  25
  26 All of the bolded items in the above list represent recurring themes and special focii of the course:
  27
  28 1. various issues about order, mutation, and the relation between dynamic and static representations
  29 2. various ways of having fun with, and learning from, the restrictions of a good type system
  30 3. monads, especially as a tool for modularity, also their connections to issues 1 and 2
  31 4. continuations, especially their connections to issue 1
  32 5. in what ways are programming languages usable for what we think of as semantics? in what ways are the "semantics" of those programming languages?
  33
  34 <!--
  35 One of the on-going themes will
  36 concern evaluation order and issues about how computations (inferences,
  37 derivations) unfold in (for instance) time.  The key analytic technique is to
  38 form a static, order-independent model of a dynamic process. We'll be
  39 discussing this in much more detail as the course proceeds.
  40 -->
  41
  42
  43 ### Other lists ###
  44
  45 The logical systems we'll be looking at include:
  46
  47 * the so-called "pure" or untyped (monotyped?) lambda calculus
  48 * combinatory logic
  49 * the simply-typed lambda calculus
  50 * polymorphic types with System F
  51
  52 The "programming languages" we'll be looking at (which aren't in the list of "logical systems") include:
  53
  54 * Jim's made-up programming language
  55 * Scheme (using the Racket and/or Chicken implementations)
  56 * OCaml
  57 * Haskell (using the GHC implementation)
  58
  59 <!--
  60 See also the page on [[ applications]].
  61 -->