Graded modal dependent type theory
From MaRDI portal
Publication:2233475
DOI10.1007/978-3-030-72019-3_17zbMath1473.68052arXiv2010.13163OpenAlexW3110513392MaRDI QIDQ2233475
Benjamin Moon, Harley III Eades, Dominic A. Orchard
Publication date: 18 October 2021
Full work available at URL: https://arxiv.org/abs/2010.13163
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (4)
When programs have to watch paint dry ⋮ Linearity and uniqueness: an entente cordiale ⋮ A dependent dependency calculus ⋮ Graded modal dependent type theory
Cites Work
- Linear logic
- Region-based memory management
- The calculus of constructions
- Finitely stratified polymorphism
- Bounded linear logic: A modular approach to polynomial-time computability
- Logic colloquium '73. Proceedings of the logic colloquium, Bristol, July 1973
- A linear logical framework
- Graded modal dependent type theory
- Coeffects
- Integrating Linear and Dependent Types
- On Irrelevance and Algorithmic Equality in Predicative Type Theory
- Linear dependent types for differential privacy
- Combining effects and coeffects via grading
- I Got Plenty o’ Nuttin’
- Tridirectional typechecking
- Extending Higher-Order Unification to Support Proof Irrelevance
- Uniqueness Typing Redefined
- Linear Dependent Types and Relative Completeness
- Syntax and Semantics of Quantitative Type Theory
- Coeffects: Unified Static Analysis of Context-Dependence
- A relationally parametric model of dependent type theory
- Parametric effect monads and semantics of effect systems
- Practical affine types
- Bounded Linear Types in a Resource Semiring
- A Core Quantitative Coeffect Calculus
- Types for Proofs and Programs
- Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Graded modal dependent type theory