David Corfield (University of Kent): Modal and graded modal type theory
Abstract In my recent book (Modal homotopy type theory, Oxford University Press, 2020) I argue that philosophy would greatly profit from adopting a form of dependent type theory as its basic formalism, especially in the areas of philosophy of language and metaphysics. In this talk I will focus on an area with great potential, modal dependent type theory. While computer scientists with related, yet different interests to philosophers have provided ways to attach modalities to types in general and not merely propositions, the philosophical interpretation of such systems has barely begun. I will explore a range of ways we might look to exploit them and their more recently developed graded variants.