Abstract
The first lecture traced the three paths leading to Curry and Howard's discovery : the lambda-calculus, intuitionistic logic, and simple type systems.
Around 1930, Church introduced the lambda-notation λx.e to designate the function that associates e with x, and used it to unify various mathematical notations involving related variables (sums, limits, quantifiers, etc.). His first lambda-calculus, published in 1932 and 1933, is a mathematical logic that uses lambda-notation to represent sets. This logic was quickly abandoned as incoherent. By 1936, however, pure lambda-calculus, stripped of its logical connectors, had established itself as a fundamental formalism of computability, in equivalence with Turing machines, and then, starting with the Lisp language (1960), as the core of functional programming languages.
Intuitionistic logic, introduced by Glivenko and Heyting around 1928, formalizes the notion of constructive demonstration, which is an important aspect of intuitionism, the philosophy of mathematics founded by Brouwer. According to the BHK (Brouwer, Heyting, Kolmogorov) interpretation of intuitionism, the only true propositions in intuitionistic logic are those that are justified by a construction, i.e. a mathematical object that attests to their veracity. Thus, a construction of ∃x.P is a pair of a value for x and a construction of P(x). Non-constructive demonstrations of ∃x.P are therefore excluded.
