A step-indexed model of substructural state

DOI10.1145/1086365.1086376MaRDI QIDQ2936770zbMATH OpenOpenAlexWikidataFDO

Authors Amal Ahmed, Matthew T. Fluet, Greg Morrisett

Publication date 6 January 2015

Published in Proceedings of the tenth ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL http://nrs.harvard.edu/urn-3:HUL.InstRepos:25620500

zbMATH Keywords

mutable referencesstep-indexed modelsubstructural type system

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Recommendations

• Uniqueness logic
• A very modal model of a modern, major, general type system
• A Step-indexed Semantics of Imperative Objects
• \(L^3\): a linear language with locations
• Flexible recovery of uniqueness and immutability

Cited in

(11)

• Flexible recovery of uniqueness and immutability
• Uniqueness logic
• Strong update, disposal, and encapsulation in bunched typing
• A type system for borrowing permissions
• Hoare type theory, polymorphism and separation
• Type classes for lightweight substructural types
• Connecting effects and uniqueness with adoption
• Modelling unique and affine typing using polymorphism
• A bisimulation-like proof method for contextual properties in untyped -calculus with references and deallocation
• Linearity and uniqueness: an entente cordiale
• A type system for effect handlers and dynamic labels

This page was built for publication: A step-indexed model of substructural state

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