Before revision: It was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds Whereas simply typed lambda calculus has variables ranging over terms, and binders for them, System F additionally has variables ranging over types, and binders for them.
After revision: It was discovered independently by logician Jean-Yves Girard and computer scientist John C. Reynolds Whereas simply typed lambda calculus has variables ranging over terms, and binders for them, System F additionally has variables ranging over types, and binders for them.