Publication View

λ-calculus and types Lecture notes (2008)

Thorsten Altenkirch

Abstract

1.1 A short history The λ-calculus was introduced by Alonzo Church in the 40ies. The initial goal was formalisation of mathematical reasoning, I believe. Then Turing showed that the λ-definable functions on encodings of natural numbers are the same as the

Publication details

Download	http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.66.971
Source	http://www.cs.nott.ac.uk/~txa/publ/mgs04.pdf
Contributors	CiteSeerX
Repository	CiteSeerX - Scientific Literature Digital Library and Search Engine (United States)
Type	text
Language	English
Relation	10.1.1.36.418, 10.1.1.46.8519, 10.1.1.106.2126, 10.1.1.35.5017, 10.1.1.118.8751