Linearity and uniqueness: an entente cordiale

DOI10.1007/978-3-030-99336-8_13zbMath1528.68084OpenAlexW4226204098MaRDI QIDQ6166794

Dominic A. Orchard, Daniel F. Marshall, Michael Vollmer

Publication date: 3 August 2023

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-99336-8_13

zbMATH Keywords

substructural logiclinear typesuniqueness types

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A list of successes that can change the world. Essays dedicated to Philip Wadler on the occasion of his 60th birthday
• Bounded linear logic: A modular approach to polynomial-time computability
• A retrospective on region-based memory management
• Graded modal dependent type theory
• Uniqueness logic
• Safe manual memory management in Cyclone
• The best of both worlds: linear functional programming without compromise
• Uniqueness Typing Redefined
• The execution algorithm of mercury, an efficient purely declarative logic programming language
• Cogent: uniqueness types and certifying compilation
• Extending graph rewriting with copying
• Guaranteeing safe destructive updates through a type system with uniqueness information for graphs
• Regular, shape-polymorphic, parallel arrays in Haskell
• Monads need not be endofunctors
• Exploiting vector instructions with generalized stream fusion
• Terminal semantics for codata types in intensional Martin-L\"of type theory
• Practical affine types
• Modelling Unique and Affine Typing Using Polymorphism
• Typed Lambda Calculi and Applications
• A syntax for linear logic