Modal Type Theory and its Semantics

Dr. Ranald Clouston (RSCS)

Type theory offers an alternative foundation for mathematics, particularly suited to automated proof checking. This talk will discuss the design of a new type theory, introducing connectives from modal logic. In particular we will see how the mathematical notion of denotational semantics helps us to establish both the consistency and the expressive power of a type theory.

(Higher) category theory vs (Homotopy) type theory.

Martina Rovelli (MSI) 

Given a category with adjectives, one can talk about its internal language, which is a formal system that encodes the syntax of that category. This construction generally induces a correspondence between the given flavour of category theory and a certain flavour of type theory. In this introductory talk, we will provide a basic dictionary on how to translate categorical information into type theoretical information. We will mention how the internal language of the category of sets can be expressed by means of traditional type theories, while the internal language of the (∞-)category of spaces is homotopy type theory.

This event is free and open to the public. It will be followed by drinks and nibbles on Level 3 of the Hanna Neumann Building (145).

The MSI/RSCS Seminar Series is supported by the Mathematical Sciences Institute at the College of Science and the Research School of Computer Science at the College of Engineering & Computer Science at ANU.