Friday, March 31, 2006

Permission-based ownership: encapsulating state in higher-order typed languages

Permission-based ownership: encapsulating state in higher-order typed languages by Neel Krishnaswami and Jonathan Aldrich. In PLDI'05.

I'm still puzzling through the examples, but it looks pretty cool. The essential idea is to use the type system (an extension of System F with references and ownership called System Fown) to ensure that the internal details of modules cannot be messed with.

They give an illustrative example involving customers in one domain, banking machinery in a second and account details in a third. The customers are allowed to call the banking machinery, and the banking machinery can access the account details, and all other access is invalid. The goal of System Fown is to prove these sorts of properties.

ACM | Google | Del.icio.us | CiteULike

No comments: