Graded modal dependent type theory
From MaRDI portal
Publication:2233475
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.
Recommendations
- Multimodal dependent type theory
- Multimodal dependent type theory
- Degrees of relatedness. A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory
- Guarded dependent type theory with coinductive types
- Dependent information flow types
Cites work
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 3485174 (Why is no real title available?)
- scientific article; zbMATH DE number 1241699 (Why is no real title available?)
- scientific article; zbMATH DE number 1302063 (Why is no real title available?)
- scientific article; zbMATH DE number 3349775 (Why is no real title available?)
- A core quantitative coeffect calculus
- A linear logical framework
- A relationally parametric model of dependent type theory
- Bounded Linear Types in a Resource Semiring
- Bounded linear logic: A modular approach to polynomial-time computability
- Coeffects: a calculus of context-dependent computation
- Coeffects: unified static analysis of context-dependence
- Combining effects and coeffects via grading
- Extending higher-order unification to support proof irrelevance
- Finitely stratified polymorphism
- Graded modal dependent type theory
- Hereditary substitution for the \(\lambda \Delta \)-calculus
- I got plenty o' nuttin'
- Integrating linear and dependent types
- Internalizing relational parametricity in the extensional calculus of constructions
- Linear dependent types and relative completeness
- Linear dependent types for differential privacy
- Linear logic
- Logic colloquium '73. Proceedings of the logic colloquium, Bristol, July 1973
- On irrelevance and algorithmic equality in predicative type theory
- On the Lambek calculus with an exchange modality
- Parametric effect monads and semantics of effect systems
- Practical affine types
- Region-based memory management
- Syntax and semantics of quantitative type theory
- The calculus of constructions
- Tridirectional typechecking
- Types for Proofs and Programs
- Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
- Uniqueness Typing Redefined
Cited in
(6)
This page was built for publication: Graded modal dependent type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233475)
