Skip to main content
9 votes
Accepted

System F and System T names

I posted this to TYPES, but its probably worth copying here as well: In "The system F of variable types, fifteen years later", Girard remarks that there was no particular reason for the name F: ...
Neel Krishnaswami's user avatar
7 votes
Accepted

Representable functions on System T

If every term in system T terminates, then $t\overline{n}\leadsto\overline{m}$ for every numeral $n$, and it is easy to show that a normal form $\overline{m}$ in the empty context is a numeral as well ...
cody's user avatar
  • 14k

Only top scored, non community-wiki answers of a minimum length are eligible