Functional programming and typed-functional programming in particular have two fundamental logical underpinnings. The first is Church's l calculus and the second is, what we may call, Curry - Howard - Martin-Löf analogy. Church's l calculus is the prototype functional programming language. It was invented in the early forties by the American logician Alonso Church. The interest of l calculus lies essentially in what we may phrase as the Church-Landin's thesis, which says the following: programming languages are l calculus sweetened with specific sugar. This is a concise way of describing the so-called denotational approach to semantics as opposed to Turing's approach which was more operational given in terms of Turing machines. So we can summarise this by saying that functional languages are extremely useful especially because they are language description languages.