Integrating Linear and Dependent Types

DOI10.1145/2676726.2676969zbMath1345.68109OpenAlexW2114058479MaRDI QIDQ2819785

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 typesintersection typesseparation logiclinear typesHoare triplesproof irrelevance

Mathematics Subject Classification ID

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

Related Items (8)

Linear Dependent Type Theory for Quantum Programming Languages ⋮ I Got Plenty o’ Nuttin’ ⋮ A formal logic for formal category theory ⋮ Additive types in quantitative type theory ⋮ Graded modal dependent type theory ⋮ Fibrational modal type theory ⋮ Dependent Types and Fibred Computational Effects ⋮ Modal dependent type theory and dependent right adjoints

This page was built for publication: Integrating Linear and Dependent Types