TY - GEN
T1 - Graded Modal Dependent Type Theory
AU - Moon, Benjamin
AU - Eades, Harley
AU - Orchard, Dominic
N1 - Publisher Copyright:
© 2021, The Author(s).
PY - 2021
Y1 - 2021
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85105021714&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85105021714&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-72019-3_17
DO - 10.1007/978-3-030-72019-3_17
M3 - Conference contribution
AN - SCOPUS:85105021714
SN - 9783030720186
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 462
EP - 490
BT - 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, ETAPS 2021, Proceedings
A2 - Yoshida, Nobuko
PB - Springer Science and Business Media Deutschland GmbH
T2 - 30th European Symposium on Programming, ESOP 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021
Y2 - 27 March 2021 through 1 April 2021
ER -