A step-indexed model of substructural state

DOI10.1145/1086365.1086376zbMATH Open1302.68048OpenAlexW2143661661WikidataQ60142694 ScholiaQ60142694MaRDI QIDQ2936770FDOQ2936770

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

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

zbMATH Keywords

substructural type systemmutable referencesstep-indexed model

Mathematics Subject Classification ID

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

Cited In (11)

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

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)