##
Course Outline |
||

Introduction to typed and untyped lambda calculi and their semantics. Syntax of the lambda calculus, conversion, fixed points, reduction, Church-Rosser theorem, representation of recursive functions, lambda models. Category theory, cartesian closed categories and categorical models of lambda calculus.

Week |
Date |
Topics |

1 | Jan 06/08 | Introduction, Simply typed λ-calculus with explicit pairs |

2 | Jan 13/15 | Simply typed λ-calculus with explicit pairs, Confluence (Church-Rosser) |

3 | Jan 20/22 | Categories, Morphisms |

4 | Jan 27/29 | Constructions, Cartesian closed categories (Test 1) |

5 | Feb 03/05 | Constructions, Functors and Adjunctions |

6 | Feb 10/12 | Categorical semantics of the simply typed λ-calculus |

7^{*} |
Feb 24/26 | Variant types and recursion |

8 | Mar 03/05 | Untyped λ-calculus (Test 2) |

9 | Mar 10/12 | Recursive Domain Equations |

10 | Mar 17/19 | Recursive Domain Equations (continued) |

11 | Mar 24/26 | Algebras, primitive recursion and catamorphisms (Test 3) |

12 | Mar 31/Apr 02 | Second order λ-calculus, Review |

- The main text book: Categories, Types, and Structures
- Additional Material on the lambda calculus: Lambda Calculus
- H. Barendregt: Lambda Calculi with Types

COSC 5P05 Home Page