Abstract
Is the Curry-Howard correspondence just a pleasant coincidence between intuitionistic logic and typed lambda-calculus, both of which are not very expressive? Numerous extensions appearing in the 1970s and 1980s show that this is not the case.
Polymorphic typing is the first of these extensions. It appeared independently in the work of Girard (1971) and Reynolds (1974). Reynolds was a computer scientist who sought to make lambda-calculus typing more flexible, so as to be able to type generic functions such as sorting, which apply the same algorithm to data of different types. Girard is a logician looking for a functional interpretation (like the BHK interpretation) for second-order arithmetic, a logic powerful enough to express analysis. They converged on the same type system, called polymorphic lambda-calculus by Reynolds and system F by Girard, which proved extremely expressive.
