Stanford University
Mathematics 291B: Recursion Theory
(Philosophy 351B--Enroll in Math 291B)
Spring 2005-2006
Syllabus

#### Instructor: Ruy de Queiroz (Visiting Professor)

Office hours: Mo We 09:30-10:45am and by arrangement, Room 8, Bolivar House
Class hours: Tu 11:00am-12:00pm, Th 11:00am-12:30pm, Seminar Room, Bolivar House

#### Course description:

The lambda calculus. Term-structure and substitution. Reduction. Combinatory Logic. Weak reduction. The Power of Lambda and Combinators. The fixed-point theorem. Representing the recursive functions. The undecidability theorem. Typed lambda-calculus. Curry-Howard isomorphism.

#### Prerequisites:

Phil 351 (Math 291), or equivalents, or consent of the instructor.

#### Text:

Introduction to Combinators and Lambda-Calculus, by J. Roger Hindley and Jonathan P. Seldin, London Mathematical Society Student Texts 1, Cambridge University Press, 1986.

#### Other resources:

1. An introduction to lambda calculi and arithmetic, by Harold Simmons.
2. http://www.safalra.com/science/lambdacalculus/index.html
3. On-line books, lecture notes, etc (Lambda Calculus)
4. Barendregt and Barendsen's shorter introduction to the lambda calculus
5. Alonzo Church Papers
6. Church, Alonzo, An unsolvable problem of elementary number theory, American Journal of Mathematics, 58 (1936), pp. 345.363. (This paper contains the proof that the equivalence of lambda expressions is in general not decidable.)
7. Church, Alonzo, The calculi of lambda-conversion. Imprint: Princeton, Princeton University Press, 1941 [i.e. 1963]. (Series: Annals of mathematical studies, no. 6)
8. Lambda-Calculus, Types and Models, by J.L. Krivine, Masson, Paris, 1993 (English xlation) ISBN 0-13-062407-1.