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, which has strong relevance to computer science (type theory, lambda-calculus etc). The course is also suitable for mathematics students interested in category theory and the foundations of mathematics.

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

• Recursion, induction and co-induction in categories.
• The Curry-Howard isomorphism between propositions and types.
• Cartesian closed categories. Categorical combinators. Models of typed and untyped lambda-calculus.
• Normalization proofs.
• Adjoints and monads. Monads and functional programming.
• Functor categories. Presheaves. Cayley's theorem for categories.
• Toposes and their internal logic. Pretoposes.
• Locally cartesian closed categories.
• Martin-Löf type theory.

• J. Lambek and P.J. Scott: Introduction to higher-order categorical logic. Cambridge University Press 1986.

Selected chapters and sections of

• P. Martin-Löf. An intuitionistic theory of types. In G. Sambin and J.M. Smith (eds.) Twenty-Five Years of Constructive Type Theory. Oxford University Press 1998, pp. 127 -- 172.
• B. Jacobs and J. Rutten. A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin 62(1997), pp. 222-259. ( Available through this link.)
• P. Wadler. Monads for functional programming. In: Advanced Functional Programming (ed. J. Jeuring). Springer Lecture Notes in Computer Science, vol 925. Springer. ( Available through this link. )
• E. Palmgren. Constructive Mathematics. Lectures notes for Copenhagen Logic Summer School, 11-22 August, 1997. (This is a brief, first introduction to the foundations of constructive mathematics.)
• Topics in Domain Theory and Point-free Topology 48 pp. U.U.D.M. Lecture Notes 2002:LN2. (Supplementary lecture notes for the course Domänteori MN1.)
• English-Swedish dictionary for the course

Knowledge of category theory is not assumed. Here are some good sources for basic category theory

• Benjamin C. Pierce. Basic Category Theory for Computer Scientists. MIT Press 1991.
• Colin McLarty. Elementary Categories, Elementary Toposes Oxford University Press 1992.
• J. van Oosten. Basic Category Theory. BRICS course notes 1995. Download free copy here.
• R.F.C. Walters. Categories and Computer Science. Cambridge University Press.

Assignments, recommended exercises etc

Some exercises will require the use of the programming language Haskell (Haskell 98). Free versions can be downloaded here: recommended version Hugs 98. Sample program for operating with streams here. A tutorial in Haskell is available here.

Schedule

Student seminars

• Friday 22 Nov, 10.15. Modal logic and coalgebras. Presenter: Kidane Yemane
• Monday 9 Dec, 15.15. Categorical automata theory: minimalization (Chapter 6.3 of Arbib and Manes: Arrows, Structures and Functors). Presenter: Fredrik Dahlgren
• Friday 13 Dec, 10.15. On coalgebra of real numbers (papers by D.Pavlovic,V.Pratt, M Escardo). Presenter: Jesper Carlström.

  ---

  TO BE CONTINUED by

  ---

• Objects and classes, coalgebraically (papers by B. Jacobs). Presenter: Erik Andersson
• Ordinals and lambda-representability. Presenter: Jonas Ransjö
• Bird-Meertens Formalism: categorical datatypes and calculational proofs, by Presenter Johan Glimming.

Lecturer

• Erik Palmgren. Office: room 2137, phone 471 32 85.

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