I think Bill Gosper got it: Michael Levin taught a course in logic with Lisp. Now that I have his name, I think that I could find his course notes online somewhere, which I seem to recall were published as a memo by AI or LCS. At 10:37 PM 8/2/2012, Bill Gosper wrote:

Henry, I think you mean Mike Levin and his haltp function. --rwg Before the quadratic equation comes monomials, e.g. units|dimensional analysis. http://news.yahoo.com/energy-dept-spends-43-billion-researching-better-elect... The 2013 Volt model’s battery-only range has been increased three miles to 38 miles, in part because Chevrolet boosted the storage capacity by .5 kilowatts per hour. The DOE research would seek to improve on existing storage capacity.

hgb>

Neither McCarthy nor Chaitin. We discussed this ages ago on math-fun, but my personal archive doesn't go back far enough (i.e., prior to 1997).

At 06:31 PM 8/2/2012, Mike Stay wrote:>On Thu, Aug 2, 2012 at 4:44 PM, Henry Baker <hbaker1@pipeline.com <http://gosper.org/webmail/src/compose.php?send_to=hbaker1%40pipeline.com>> wrote:>> BTW, who was the fellow at MIT in the early 1970's who used Lisp to teach computation theory? He had a very elegant proof of undecidability using a Lisp interpreter.>>You probably mean Greg Chaitin. http://www.cs.auckland.ac.nz/~chaitin/lisp.html>-- >Mike Stay - metaweta@gmail.com <http://gosper.org/webmail/src/compose.php?send_to=metaweta%40gmail.com>