Graded modal dependent type theory

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

Mathematics Subject Classification ID

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