(Or "second order typed lambda-calculus", "System F", "Lambda-2"). An extension of typed lambda-calculus allowing functions which take types as parameters. Polymorphic lambda-calculus was invented by Jean-Yves Girard in 1971 and independently by John C. Reynolds in 1974.