From 2ce9f23d4fc22497ed371d6fe11eed9ade61c8ab Mon Sep 17 00:00:00 2001
From: Jim <jim.pryor@nyu.edu>
Date: Sun, 1 Feb 2015 19:11:49 -0500
Subject: [PATCH] write up course overview

---
 _overview.mdwn | 29 ----------------------------
 index.mdwn     |  2 +-
 overview.mdwn  | 61 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 62 insertions(+), 30 deletions(-)
 delete mode 100644 _overview.mdwn
 create mode 100644 overview.mdwn

diff --git a/_overview.mdwn b/_overview.mdwn
deleted file mode 100644
index b05de227..00000000
--- a/_overview.mdwn
+++ /dev/null
@@ -1,29 +0,0 @@
-*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
--->
diff --git a/index.mdwn b/index.mdwn
index 11bee265..f1be5a1c 100644
--- a/index.mdwn
+++ b/index.mdwn
@@ -134,7 +134,7 @@ course is to enable you to make these tools your own; to have enough
 understanding of them to recognize them in use, use them yourself at least
 in simple ways, and to be able to read more about them when appropriate.
 
-[[More about the topics and larger themes of the course| overview]]
+[[More about the topics and larger themes of the course|overview]]
 
 
 ## Who Can Participate? ##
diff --git a/overview.mdwn b/overview.mdwn
new file mode 100644
index 00000000..d3909644
--- /dev/null
+++ b/overview.mdwn
@@ -0,0 +1,61 @@
+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.
+
+### Topics ###
+
+* Basics of (especially "functional"-style) programming: including pattern matching, recursive definitions, abstract datatypes, **modularity, separating interfaces from implementation**
+* The syntax and proof theory of the untyped lambda calculus; at least some discussion of its semantics
+* Different **evaluation-order strategies** for formal systems, different "normalizing" properties
+* Combinatorial logic, or the dispensability of variables
+* Recursive definitions and recursive types, fixed-point combinators
+* Other **type sophistication**: abstract datatypes, polymorphic types, perhaps dependent types
+* **Mutation** and imperative/iterative idioms
+* **Monads**, especially as a way to **represent "dynamic" computation using "static" or declarative idioms**
+* The origin of monads in category theory
+* **Controlling evaluation order and effects**, especially by means of **continuations**
+* Giving **order-independent characterizations of an order of evaluation**
+* Perhaps some of the relations between typed programming languages and logics (the "Curry-Howard" correspondence or "isomorphism" [sic])
+* Going back and forth between **representing a computational idiom *as a function* versus *as a static structure*&nbsp;**
+* We'll link to, but probably not discuss, material for JP's logic class about formal grammars, automata, and decidability
+* The different styles in which computer scientists give **"semantics" for their languages**, and how this relates to what we think of as semantics
+* If time permits, "indeterministic" or "preemptively parallel" computation and linear logic
+* If time permits, "dynamic" or "epistemic" logics
+
+
+### Themes ###
+
+All of the bolded items in the above list represent recurring themes and special focii of the course:
+
+1. various issues about order, mutation, and the relation between dynamic and static representations
+2. various ways of having fun with, and learning from, the restrictions of a good type system
+3. monads, especially as a tool for modularity, also their connections to issues 1 and 2
+4. continuations, especially their connections to issue 1
+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?
+
+<!--
+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.
+-->
+
+
+### Other lists ###
+
+The logical systems we'll be looking at include:
+
+* the so-called "pure" or untyped (monotyped?) lambda calculus
+* combinatorial logic
+* the simply-typed lambda calculus
+* polymorphic types with System F
+
+The "programming languages" we'll be looking at (which aren't in the list of "logical systems") include:
+
+* Jim's made-up programming language
+* Scheme (using the Racket and/or Chicken implementations)
+* OCaml
+* Haskell (using the GHC implementation)
+
+<!--
+See also the page on [[ applications]].
+-->
-- 
2.11.0