Integrating Linear and Dependent Types

From MaRDI portal

Revision as of 18:19, 3 February 2024 by Import240129110113 (talk | contribs) (Created automatically from import240129110113)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Publication:2819785

Jump to:navigation, search

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 types intersection types separation logic linear types Hoare triples proof 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

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:2819785&oldid=15736488"