Suggestions for textbook?

To: Types dist list <types@cis.upenn.edu>
Subject: Suggestions for textbook?
From: Mitchell Wand <wand@ccs.neu.edu>
Date: Thu, 26 Jun 2003 15:20:20 -0400

This fall I will be teaching a 1-credit seminar for freshmen in our
honors program.

They will be taking this at the same time as they get the introductory
CS course (out of How to Design Programs, by Felleisen et al), and a
discrete math course (taught out of Rosen, Discrete Mathematics and
its Applications 5ed).

My goal is to give them something that will challenge but not
overwhelm them and that will somehow complement what they are getting
in these courses.

My plan is to give them a look at computability theory, using
lambda-calculus as a vehicle.  This will allow them to think about
doing mathematics about programs and writing programs about
mathematical objects.

If I can get them through the undecidability of the halting problem in the
term, I will count myself successful.

Does anyone have suggestions for a text or other materials that might
be suitable for this?

Chris Hankin's book on Lambda Calculi is about right, but is out of
print.  Barendregt's article on Functional Programming and Lambda
Calculus in the Handbook of Theoretical Computer Science B covers the
right material, but is probably scary for freshmen.

Additional parameters:  I will have these folks for 1 hour per week
for 15 weeks.  The average SAT will be 1250-1300 or so.  I could cover
the material using some other machine model, but they will get this
material again in Theory of Computation, using the standard models,
and I'd like to avoid making life difficult for the instructor in that
course.  

Any thoughts?

--Mitch