[Prev][Next][Index][Thread]
the strength of the typed lambda calculus
I'm looking for a proof that the typed lambda calculus defines exactly
the extended polynomials. I have what appears to be the original paper
by Schwichtenberg. Unfortunately this paper seems to skim over some of
the details that I need to see. Does anyone know of another version of
this proof? I would think that this is important enough to be in some
type theory book, but none of the ones I've checked have even
mentioned the result.
A couple of people from comp.lang.functional have pointed me to papers
by Statman, but they seem to be more on deciding beta-reducibility,
rather than what can be computed within the language.
Thanks a lot.
Brian Postow