Re: [isabelle] Polymorphism and simple type



Actually the term "simply-typed" tends to be used in more than one way.
Some people use it to mean "not dependently-typed" and some people use it to
mean "not polymorphic and not dependently-typed".

When people refer to "simply-typed lambda calculus" they are (usually)
referring to Church's original simply typed lambda calculus (which he
created after his untyped lambda calculus).  This does not have
polymorphism, but Isabelle and HOL, that are based on it, do.

Mark.

on 17/1/11 6:01 PM, Steve W <s.wong.731 at gmail.com> wrote:

> Hi,
>
> I have a question about Isabelle's polymorphism. Since Isabelle has a
> simply-typed lambda calculus, how come the meta-logic is polymorphic?
> Polymorphism is not typically considered simple, right?
>
> Regards
> Steve





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.