User loginNavigation 
History of LambdaCalculus and Combinatory logic
F. Cardone and J. R. Hindley. History of LambdaCalculus and Combinatory logic. To appear as a chapter in Volume 5 of the Handbook of the History of Logic.
From the introduction:
Seen in outline, the history of LC and CL splits into three main periods: first, several years of intensive and very fruitful study in the 1920s and â€™30s; next, a middle period of nearly 30 years of relative quiet; then in the late 1960s an upsurge of activity stimulated by developments in higherorder function theory, by connections with programming languages, and by new technical discoveries. The fruits of the first period included the firstever proof that predicate logic is undecidable. The results of the second attracted very little nonspecialist interest, but included completeness, cutelimination and standardization theorems (for example) that found many uses later. The achievements of the third, from the 1960s onward, included constructions and analyses of models, development of polymorphic type systems, deep analyses of the reduction process, and many others probably well known to the reader. The high level of activity of this period continues today. Beware: This is a long paper (but less than you might expect it to be by looking at the page count: about half the pages are dedicated to the bibliography). In the announcement on the TYPES Forum the authors invited comments, suggestions and additional information on the topics of the paper, namely the development of lambdacalculi and combinatory logic from the prehistory (Frege, Peano and Russell) to the end of 20th century. By Ehud Lamm at 20080219 19:21  History  Lambda Calculus  Type Theory  other blogs  10441 reads

Browse archivesActive forum topics 
Recent comments
1 day 9 hours ago
1 day 15 hours ago
1 day 17 hours ago
2 days 3 hours ago
3 days 23 hours ago
5 days 6 hours ago
5 days 6 hours ago
1 week 3 hours ago
1 week 15 hours ago
1 week 3 days ago