Re: teach untyped lambda calculus?

• To: types@theory.LCS.MIT.EDU
• Subject: Re: teach untyped lambda calculus?
• From: jcm@ra.stanford.edu (John Mitchell)
• Date: Mon, 10 Oct 88 20:14:59 EDT
• Sender: meyer@theory.LCS.MIT.EDU

Date: Mon, 10 Oct 88 11:17:30 PDT
To: hudak-paul@yale.arpa
Cc: types@theory.LCS.MIT.EDU

I agree that untyped lambda calculus should be taught.
Last time I tried a course like this, I started with
untyped lambda calculus, but found that many of the
things I wanted to say (about semantics for example,
and "run time type errors" when constants like 0,1, +
are added) required some notion of type. So this time
I thought I'd start with typed lambda calculus, and
consider "untyped" lambda calculus a syntactic variant
of typed lambda calculus with domain equation t=t->t.
I can tell you later how well this works, as compared with
my last attempt.

John

• Prev: Re: comments on my course outline
• Next: Hoare logic and lambda calculus
• Index(es):
  • Main
  • Thread