Graded Modal Dependent Type Theory

Benjamin Moon, Harley Eades, Dominic Orchard

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 30th European Symposium on Programming, ESOP 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Proceedings
EditorsNobuko Yoshida
PublisherSpringer Science and Business Media Deutschland GmbH
Pages462-490
Number of pages29
ISBN (Print)9783030720186
DOIs
StatePublished - 2021
Event30th European Symposium on Programming, ESOP 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021 - Luxembourg, Luxembourg
Duration: Mar 27 2021Apr 1 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12648 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference30th European Symposium on Programming, ESOP 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021
Country/TerritoryLuxembourg
CityLuxembourg
Period3/27/214/1/21

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Graded Modal Dependent Type Theory'. Together they form a unique fingerprint.

Cite this