X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;f=More_about_the_topics_and_larger_themes_of_the_course.mdwn;fp=More_about_the_topics_and_larger_themes_of_the_course.mdwn;h=46505815b238eda754774cd91d1c8e60a8776182;hb=fa757b935541b00dbe0542cbe96e3021e9c30337;hp=0000000000000000000000000000000000000000;hpb=746a07a53869dcf2d25f7b2ded47ee0f3985bbe9;p=lambda.git

diff --git a/More_about_the_topics_and_larger_themes_of_the_course.mdwn b/More_about_the_topics_and_larger_themes_of_the_course.mdwn
new file mode 100644
index 00000000..46505815
--- /dev/null
+++ b/More_about_the_topics_and_larger_themes_of_the_course.mdwn
@@ -0,0 +1,27 @@
+*Coming, please wait...*
+
+<!--
+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
+-->