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 typesseparation logicintersection typeslinear typesHoare triplesproof irrelevance

Mathematics Subject Classification ID

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

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

(11)

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

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)