An online and in-person workshop to discuss the implications of graded modalities for philosophy, linguistics and computer science. To be held 13:00-17:00 UK time (UTC+1), Thursday 16 June 2022.
To join Teams meeting click here.
To attend in person come to SW101, Cornwallis South on the University of Kent campus at Canterbury.
(Note that on the following day there is a Meeting on Graded Types.)
Logicians and philosophers have long taken inspiration from the complexity of natural language to find interesting applications of logical tools. Compositional semantics as a linguistic discipline has been enormously enriched by this work. While the vast majority of this work is pursued within a set-theoretic framework, the recent rise of type theory and category theory as competing frameworks for mathematics and logic serves as an invitation for linguists to look for new insights that might be gained by adopting a new modeling language, and for logicians to look again to natural language as a source of inspiration and challenges. In this vein, I will discuss graded expressions of modality, which are widespread in English and other natural languages. While most linguistic work has followed modal logic in analyzing modal language as involving first-order quantification over sets of worlds, recent work has uncovered a much richer structure underlying many modal concepts that is better thought of as being organized into scales - much like scalar adjectives (“bigger, smaller”, etc). I will survey some of the phenomena in English that have motivated attention to graded modality, and describe the basic formal approach I have pursued in a traditional framework, in the hope that it can be adapted fruitfully into graded modal type theory.
Once we understand many modal notions to be expressing features of types under variation, then different ranges of variation will correspond to different strengths of modality. For instance, in many situations necessity may be considered as expressing invariance under variation, as when a necessarily true proposition remains true in all related settings. Philosophers speak here of possible worlds, but we may consider a type of such worlds simply as a domain of variation. Then it is possible to compare variation over different such types. For instance, we might consider the degree of necessity of an historical event in terms of our understanding of whether the event would have occurred under greater or lesser changes in the prevailing conditions. In this talk, I will explore how such graded modality arises naturally in the context of dependent type theory.
Modal reasoning has been employed in programming languages for decades. For example, monads (having the structure of constructive possibility) are often used to capture side effectful computations, and the exponential modality of linear logic captures non-linearity. In the last decade, there has been a proliferation of the idea of ‘graded modal types’ in programming to make modal reasoning more fine-grained. Various approaches provide forms of graded necessity and graded possibility to expose intensional properties of programs in their types. In this talk, I give an overview of how this idea has developed in programming language theory and practice from a few different angles, and will demonstrate the potential of this approach through our research language Granule which provides various graded modalities within a single unified programming system. I will discuss how graded modalities can be used for reasoning, verification, optimisation, and program synthesis.
Dan Lassiter, Graded modality
Benjamin Moon, Harley Eades III and Dominic Orchard, Graded Modal Dependent Type Theory
David Corfield, Modal homotopy type theory (which became Chap. 4 of my OUP book of the same title)
Harley Eades III, A brief history of graded modalities.
Last revised on June 16, 2022 at 10:39:27. See the history of this page for a list of all contributions to it.