7 June 2019, Ludwig-Maximilians-Universität München
| 09:55 | Opening |
| 10:00 - 10:45 | Fredrik Nordvall Forsberg: Open games in type theory |
| 10:45 - 11:15 | Coffee break |
| 11:15 - 12:00 | Nicolai Kraus: Homotopical ideas in type theory |
| 12:00 - 14:30 | Lunch break |
| 14:30 - 15:15 | Iosif Petrakis: Types and Bishop sets |
| 15:15 - 16:00 | Burak Ekici: Univalent Typoids in Coq |
| 16:00 - 16:30 | Coffee break |
| 16:30 - 17:15 | Gidon Ernst: Applications of type theory for software verification |
| Fredrik Nordvall Forsberg: Open games in type theory |
| Open games is a model of economic game theory, whose purpose is to enable a compositional framework, where complex games can be constructed by plugging together smaller, well-understood games. This is achieved by equipping games with open "ports" for communicating with their environment, heavily inspired by techniques from basic category theory. After giving a gentle introduction to the above, I will argue that it is advantageous to move to a framework of open games incorporating dependent types, both for accurate modelling of economic games, and for mathematical reasons. This also brings up type-theoretical issues such as uniform function spaces that might be of independent interest. |
| Nicolai Kraus: Homotopical ideas in type theory |
| I will explain basic concepts of homotopy type theory, and demonstrate which way of reasoning these ideas encourage. As a concrete example, I will show two different looking but equivalent implementations of the concept of a group: first, as a tuple (G,comp,id,inv,...), which is the standard representation; and second, as a pointed connected 1-truncated type, which is the "homotopy type theory representation". |
| Iosif Petrakis: Types and Bishop sets |
| The standard way of formalizing a Bishop set is through the notion of a setoid in intensional Martin-Loef type theory. We explain why this formalization is not faithful, in Feferman's sense, and we briefly describe BST, a faithful reconstruction of Bishop's theory of sets. As an application to constructive topology, we use the corresponding theory of set-indexed families of sets and subsets in the study of spectra of Bishop spaces and their limits. |
| Burak Ekici: Univalent Typoids in Coq |
| In this talk I will give an overview of (univalent) typoids, Coq and my representation of the former into the latter. |
| Gidon Ernst: Applications of type theory for software verification |
| In software verification one aims to prove strong functional properties about programs. It is natural to view this problem as one of constructive mathematics, via the well-known interpretation of proofs as programs and types as specifications. This approach is not only theoretically elegant but works well in practice, too. However, the influence of type theory on state-of-the-art verification tools is often not quite obvious ‐ ideas are selectively adapted and integrated into the respective methodology of such tools. We will take a tour to review and discuss a few examples. |
There is no registration fee. But to aid planning, please contact Chuangjie Xu (xu@math.lmu.de) if you're interested in participating in the workshop.