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

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.


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


Other resources:

1. An introduction to lambda calculi and arithmetic, by Harold Simmons.
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.

Additional reading:

1. `Funktion und Begriff', Vortrag, gehalten in der Sitzung vom 9. Januar 1891 der Jenaischen Gesellschaft für Medizin und Naturwissenschaft, Jena: Hermann Pohle. Translated as `Function and Concept' by P. Geach in Translations from the Philosophical Writings of Gottlob Frege, P. Geach and M. Black (eds. and trans.), Oxford: Blackwell, third edition, 1980.
2. Grundgesetze der Arithmetik, Jena: Verlag Hermann Pohle, Band I, 1893. Partial translation as The Basic Laws of Arithmetic by M. Furth, Berkeley: U. of California Press, 1964.


Last updated: June 14, 2006, 09:23am PDT