comment about abortable traversals
[lambda.git] / 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* **
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 -->