L^3: a linear language with locations

MaRDI QIDQ3593499zbMATH OpenFDO

Authors Amal Ahmed, Matthew T. Fluet, Greg Morrisett

Publication date 20 July 2007

zbMATH Keywords

spatial logicslinear lambda calculus

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18)

Recommendations

• Typed Lambda Calculi and Applications
• scientific article; zbMATH DE number 2087536
• On regions and linear types (extended abstract)
• Strong update, disposal, and encapsulation in bunched typing
• A type system with usage aspects

Cited in

(11)

• Context-free session type inference
• A step-indexed model of substructural state
• scientific article; zbMATH DE number 1956559 (Why is no real title available?)
• Safe session-based concurrency with shared linear state
• Typed Lambda Calculi and Applications
• A bisimulation-like proof method for contextual properties in untyped \(\lambda \)-calculus with references and deallocation
• ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
• scientific article; zbMATH DE number 1629948 (Why is no real title available?)
• POPLMark reloaded: mechanizing proofs by logical relations
• Strong update, disposal, and encapsulation in bunched typing
• scientific article; zbMATH DE number 1822438 (Why is no real title available?)

Describes a project that uses

Uses Software

• Thaw

This page was built for publication: \(L^3\): a linear language with locations

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