Graded modal dependent type theory
From MaRDI portal
Publication:2233475
DOI10.1007/978-3-030-72019-3_17zbMATH Open1473.68052arXiv2010.13163OpenAlexW3110513392MaRDI QIDQ2233475FDOQ2233475
Authors: Benjamin Moon, Harley III Eades, Dominic Orchard 
Publication date: 18 October 2021
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.
Full work available at URL: https://arxiv.org/abs/2010.13163
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
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)
Cites Work
- Practical affine types
- Title not available (Why is that?)
- Title not available (Why is that?)
- Linear logic
- Bounded linear logic: A modular approach to polynomial-time computability
- Linear dependent types and relative completeness
- Title not available (Why is that?)
- The calculus of constructions
- Title not available (Why is that?)
- Finitely stratified polymorphism
- A linear logical framework
- Linear dependent types for differential privacy
- Title not available (Why is that?)
- Title not available (Why is that?)
- Region-based memory management
- On the Lambek calculus with an exchange modality
- A core quantitative coeffect calculus
- Tridirectional typechecking
- Logic colloquium '73. Proceedings of the logic colloquium, Bristol, July 1973
- Internalizing relational parametricity in the extensional calculus of constructions
- Coeffects: a calculus of context-dependent computation
- Integrating linear and dependent types
- Parametric effect monads and semantics of effect systems
- Uniqueness Typing Redefined
- Combining effects and coeffects via grading
- I got plenty o' nuttin'
- Syntax and semantics of quantitative type theory
- Bounded Linear Types in a Resource Semiring
- Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
- Graded modal dependent type theory
- On irrelevance and algorithmic equality in predicative type theory
- Extending higher-order unification to support proof irrelevance
- Hereditary substitution for the \(\lambda \Delta \)-calculus
- Coeffects: unified static analysis of context-dependence
- A relationally parametric model of dependent type theory
- Types for Proofs and Programs
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)
