Konstruktiv logik och lambdakalkyl D

(Constructive logic and lambda-calculus)

Contents

The emphasis of the course will be on category theoretic modelling of constructive logics and calculi. The course includes an introduction to category theory. The course is suitable for students of mathematics, philosophy and computer science interested in category theory and the foundations of mathematics. A certain amount of mathematical maturity is required.

Topics included besides an introduction to basic category theory (functors, limits, adjoints):

• Algebraic logic, Heyting algebras -- Boolean algebras.
• Recursion, induction and structures in categories.
• The Curry-Howard isomorphism between propositions and types.
• Cartesian closed categories. Categorical combinators. Models of typed and untyped lambda-calculus.
• Normalization proofs. Proof-theoretic and semantic methods.
• Functor categories. Presheaves.
• Toposes and their internal logic.
• Predicative aspects of topos theory.

• C. McLarty: Elementary Categories, Elementary Toposes. Oxford University Press 1992.

In addition, we use supplementary lecture notes and some parts of

• A.M. Pitts: Categorical logic. Cambridge University Computer Laboratory Tech. Rept. No. 367, May 1995.
• P. Dybjer and A. Filinski. Normalization and partial evaluation. In Applied Semantics, Advanced Lectures, LNCS 2395, 2002. Tutorial notes from the International Summer School, Caminha, Portugal, September 2000.
• E. Palmgren. Constructive mathematics. Course notes for Copenhagen Logic Summer School 1997.

Recommended supplementary reading:

• A. Heyting. Intuitionism. North-Holland 1971. (Chapter I and II)
• P. Martin-Löf. On the meanings of the logical constants and the justification of the logical laws. Nordic Journal of Philosophical Logic Vol. 1, No. 1, 1996, pp. 11-60.

• T. Altenkirch, M. Hofmann and T. Streicher. Categorical reconstruction of a reduction free normalization proof. presented at the CLICS/TYPES workshop 1995.
• E. Bishop and D.S. Bridges. Constructive Analysis. Springer 1985.
• T. Coquand and P. Dybjer. Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science 7(1997), pp 75-94. See also earlier electronic version.
• R.L. Crole. Categories for Types. Cambridge University Press 1993.
• J.R. Hindley and J.P Seldin. Introduction to Combinators and Lambda Calculus. Cambridge University Press.
• P.T. Johnstone. Stone Spaces. Cambridge University Press 1982.
• P.T. Johnstone. Sketches of an Elephant: a Topos Theory Compendium, vol. 1 and 2. Oxford University Press 2002.
• J. Lambek and P.J. Scott: Introduction to higher-order categorical logic. Cambridge University Press 1986.
• S. Mac Lane. Categories for the Working Mathematician . Springer.
• P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis 1984.
• B. Nordström, K. Peterson and J. Smith. Programming in Martin-Löf Type Theory , Oxford 1990. Out of print, but available in electronic form here .
• H. Schwichtenberg and A.S. Troelstra. Basic Proof Theory. Cambridge University Press.
• A.S. Troelstra and D. van Dalen. Constructivism in Mathematics, vol. 1 and 2. North-Holland 1988.
• S. Vickers. Topology via Logic. Cambridge University Press.

This course was given previously in 2002. The old webpage is here.

Schedule

Problems

• Problem sheet 1 (Fredrik Dahlgren)
• Problem sheet 2
• Problem sheet 3
• Problem sheet 4

Examination

Lecturers

• Erik Palmgren, professor. Office: room 3339, phone 471 32 85.
• Fredrik Dahlgren, assistant, PhD-student in Mathematical Logic.

This page is : www2.math.uu.se/~palmgren/kl