F^\omega in Di Cosmo's presentation

[Anton Salikhmetov]

Hello,

I have a question regarding Di Cosmo's presentation titled "A brief
history
of rewriting with extensionality", which is available using the
following link:

http://pygx.sourceforge.net/dicosmo.pdf

Specifically, on page 8 the author refer to the system denoted as "F^
\omega".
Unfortunately, I was not able to figure out the meaning of this
notation. I would be grateful to you if you could tell me which
literature sources describe such systems.

With best regards,
Anton Salikhmetov

[Anton Salikhmetov]

I have just found the "System F" article at Wikipedia, which is
available at the following address:

http://en.wikipedia.org/wiki/System_F

The systems Di Cosmo mentions in his presentation belong to
polymorphic lambda calculus.

[cody...@gmail.com]

> I have just found the "System F" article at Wikipedia, which is
> available at the following address:
>
> http://en.wikipedia.org/wiki/System_F
>
> The systems Di Cosmo mentions in his presentation belong to
> polymorphic lambda calculus.

You might also want to take a look at this article:

http://en.wikipedia.org/wiki/Lambda_cube

And the mentioned references.

The lambda cube is a family of type systems which generalize simply
typed lambda calculus which include system F and system F^omega. It is
of interest that these systems are strongly normalizing as rewrite
systems, can be viewed as systems of logic, and are consistent as
systems of logic (this is a consequence of strong normalization)

Cheers

Cody