There is a deep correspondence between logic, computation (type theories) and categories. To start with, a well-known correspondence between logic and computation, called Curry-Howard correspondence. Then, given a type theory or a kind of logic - in general a formal language - there is a category that serve as a model/semantics, of the formal language. Conversly, given a category with suitable structures, one can find some formal languages, the internal languages, of it, so that mathematical reasoning can be done internal to the category.
The correspondence allows
- a deeper insight into abstract, categorical structures behind geometry and topology,
- category-theoretic foundations of mathematics alternative to set theoretical foundations,
- the formalization of constructive mathematics in programming and the development of proof assistants,
- syntax-independent view of the structures of logic.
- new kinds of models and interpretations of logic.
In this seminar, we will study the correspondence, with a focus on topos. Fragment by fragment, we will build up categories with more and more structures, by adding various first-order logical connectives and quantifiers, and finally see how the axioms for a topos arises 'logically'. Depending on the preference of participants, the seminar can be turned less about topos and more about category-theoretic structures in functional programming (e.g. monad, dependent type), but the default route is from general categorical logic to topos theory, leaving dependent types optional.
- Dozent/in: Young Min Kim