Skip to main content
Kent Academic Repository

Graded Modal Dependent Type Theory

Moon, Benjamin, Eades, Harley, Orchard, Dominic (2021) Graded Modal Dependent Type Theory. Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, . (doi:10.1007/978-3-030-72019-3_17) (KAR id:91712)

Abstract

Graded type theories are an emerging paradigm for augmenting the reasoning power of types with parameterizable, fine-grained analyses of program properties. There have been many such theories in recent years which equip a type theory with quantitative dataflow tracking, usually via a semiring-like structure which provides analysis on variables (often called ‘quantitative’ or ‘coeffect’ theories). We present Graded Modal Dependent Type Theory (Grtt for short), which equips a dependent type theory with a general, parameterizable analysis of the flow of data, both in and between computational terms and types. In this theory, it is possible to study, restrict, and reason about data use in programs and types, enabling, for example, parametric quantifiers and linearity to be captured in a dependent setting. We propose Grtt, study its metatheory, and explore various case studies of its use in reasoning about programs and studying other type theories. We have implemented the theory and highlight the interesting details, including showing an application of grading to optimising the type checking procedure itself.

Item Type: Article
DOI/Identification number: 10.1007/978-3-030-72019-3_17
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Dominic Orchard
Date Deposited: 24 Nov 2021 10:34 UTC
Last Modified: 29 Nov 2021 10:18 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/91712 (The current URI for this page, for reference purposes)

University of Kent Author Information

Moon, Benjamin.

Creator's ORCID:
CReDIT Contributor Roles:

Orchard, Dominic.

Creator's ORCID: https://orcid.org/0000-0002-7058-7842
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.