Schedule.2017
| Date | Leader | Topic |
|---|---|---|
| 30 Nov | Andreas | From simply-typed lambda calculus to cartesian closed categories |
| 07 Dec | Andreas | Cartesian closed categories |
| 14 Dec | Andreas | Exercises around STL and CCC (on paper and/or in Agda) |
To celebrate the end of the term, we meet afterwards in the Rotary Pub which opens 7pm.
December 2017: vote on the suggested topics
(yes = interested, maybe = indifferent, no = less interested.)
Results (green = yes, yellow = maybe):
| Date | Leader | Topic | Remark |
|---|---|---|---|
| 11 Jan | AA | Planning, exercises ctd. | Exam week LP2, POPL 18 |
| 18 Jan | Andrea | Cubical Agda tutorial, exercises | |
| 25 Jan | Folkmar, Jannis, Matthías, Nachi, Sólrún | Short presentations | (Away: Sandro, Andrea, Frederik HI) |
| 01 Feb | Sandro | Categories: Functors etc. | Agda meeting in Budapest (Max opens the room!) |
| 08 Feb | Mattias Olsson | Set theory (ZFC) | room EDIT 8103 |
| 15 Feb | Jesper | Unification, exercises | Studentkårens dag, AA away |
| 22 Feb | AA | Normalization, exercises | Lambda Days (Krakow) |
| 01 Mar | Konstantinos | CwFs, exercises | |
| 08 Mar | Nachi, Frederik HI | Equality issues when formalizing categories in Agda | |
| 15 Mar | AA | Planning LP4 | Exam week LP3 |
| Date | Leader | Topic | Remark |
|---|---|---|---|
| 22 Mar | Konstantinos | Dependent type theory: judgements and rules | absent: AA,SS |
| 29 Mar | Frederik HI | Proofs in Homotopy Type Theory | Thu before Easter; absent: AA |
| 5 Apr | AA | Logical relations, normalization | |
| 12 Apr | Sandro | Pure Type Systems (PTS) | Department day |
| 19 Apr | --- | --- | absent: AA |
| 26 Apr | Sandro | More on PTSs | absent: AA |
| 3 May | Jesper | The Agda's New Sorts: a pure type system with universe polymorphism | |
| 10 May | --- | --- | Ascension day |
| 17 May | Frederik HI | Univalent categories | |
| 24 May | David | Presheaf models of dependent type theory | Room: EDIT 8103; absent: AA |
| 31 May | Karin Wibergh | The Agda refactoring tool project (short presentation) | absent: AA |
| 7 Jun | Pierre | MSc: Actors formalized in Agda | 27th Agda meeting ? |
| 14 Jun | Folkmar | Tree Automata | |
| 21 Jun | --- | --- | --- |
| 28 Jun | Jesper | Vectors are Records, Too! (abstract, slides) | |
| 5 Jul | --- | --- | --- |
| 12 Jul | David | Models of dependent type theory and the univalence axiom | at 3pm in EDIT 8103 |
| 19 Jul | Andreas | Kripke models of intuitionistic propositional logic | BBQ after meeting |
| 30 Aug | Frederik? | Theorems for free / parametricity (?) |