Working Group "Operations, Sets, and Types" (WGOST)
- Wednesday from 15:15 to 18:00
In this working group we discuss a series of topics that are closely related to actual research done in connection with the project "The Operational Paradigm: its Mathematical and Philosophical Frontiers".
So-called operational theories provide a conceptual framework for all sorts of abstract computations and type systems as they are used today in the discussion of the foundations of mathematics and computer science. They are closely related to forms of the (typed and untyped) lambda calculus and partial combinatory algebras.
In this semester we focus on Topos Theory and the problem of identity types in Martin-Löf Type Theory and Explicit Mathematics.
This course is well suited for students who are interested in the foundations of mathematics and computer science and have a good background in mathematical logic. It introduces into a research area that is actively pursued in our research group. Upon successful completion of this course, the students will have a good basis for doing own research along the lines of our project.
Good basic knowledge in mathematical logic.
To be announced during the lecture.