Lambda Calculus and System F

The lambda calculus is a theory that treats functions as formulas or expressions. Arithmetic is another example of a language of expressions.  In arithmetic, you have variables (x,y,z..), numbers (1,2,3...) and operators (+, - ...). x+y then denotes the output of applying the addition operator to x and y and this can be extended to more complicated expressions. 

Lambda calculus extends this concept to functions. If we define a function f mapping x to x squared; then consider A = f(10); then in the lambda calculus we simply write A = (lambda x. x^2)(10). The expression (lambda x. x^squared) stands for the function that maps x to x squared rather than the statement that x is mapped to x squared.

One advantage of the lambda calculus, is it allows us to easily consider higher-order functions, i.e. functions with functions as inputs and/or outputs. An example is the expression f maps to f.f which takes the function f and applies it to the function f, the composition of f with itself. In lambda notation we write (lambda x.f(f(x)) and the operation that maps f to f composed with itself is (lambda f . lambda x. f(f(x)). You can see this is easy to extend to triple composition, and so on.

Technically speaking, lambda calculus is Turing-complete, that is, it is a universal model of computation that can be used to simulate any Turing machine.

Now lambda calculus can be typed or untyped, typed is more restrictive - we say it is weaker than untyped lambda calculus. In untyped lambda calculus we are flexible about domains and codomains. For typed calculus we have simply-typed - where we specify the type of every expression and polymorphically typed, where we have types of a specific form X->X but we don't specify the type.

System F is a form of polymorphic lambda calculus.

System F formalizes parametric polymorphism in languages. In so doing, it forms a theoretical basis for languages like ML and Haskell. 

System F was discovered independently by logician Jean-Yves Girard (1972) working in proof theory, and computer scientist John C Reynolds, who held positions at Edinburgh University, Imperial College and Carnegie Mellon.

The ideas aforementioned stemmed from interest and investigation in the 1930s into what does it mean for a function to be "computable" - in other words, have results derivable using (in principle) pencil and paper only.