Integrating linear and dependent types

DOI10.1145/2676726.2676969MaRDI QIDQ2819785zbMATH OpenOpenAlexFDO

Authors Neelakantan R. Krishnaswami, Pierre Pradic, Nick Benton

Publication date 29 September 2016

Published in Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2676726.2676969

zbMATH Keywords

dependent typesHoare triplesintersection typeslinear typesproof irrelevanceseparation logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Linear dependent types and relative completeness
• Linear dependent types in a call-by-value scenario
• Parametricity and dependent types
• Linear types and locality
• Dependent types and formal synthesis
• Linear types and approximation
• Dependent types and program equivalence
• Dependent Types for Low-Level Programming
• Enriching an Effect Calculus with Linear Types

Cited in

(12)

• Fibrational modal type theory
• Graded modal dependent type theory
• Dependent types and fibred computational effects
• Linear types and locality
• I got plenty o' nuttin'
• Linear dependent types and relative completeness
• Modal dependent type theory and dependent right adjoints
• A formal logic for formal category theory
• Additive types in quantitative type theory
• Safe session-based concurrency with shared linear state
• Logical foundations of quantitative equality
• Quantitative equality in substructural logic via Lipschitz doctrines

This page was built for publication: Integrating linear and dependent types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2819785)