Policy as Types

2013/07/30 by Lucius G Meredith, Lucius Gregory Meredith, Meredith, Lucius G +4 · 1 voice
Computer Science · #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.CR #cs.LO

paper · pdf · doi:10.48550/arxiv.1307.7766

openalex publication_date 2013/07/30 · arxiv created 2013/07/31 · arxiv updated 2013/08/01 · openalex created_date 2024/04/11 · openalex updated_date 2026/07/28

Abstract

Drossopoulou and Noble argue persuasively for the need for a means to express policy in object-capability-based systems. We investigate a practical means to realize their aim via the Curry-Howard isomorphism. Specifically, we investigate representing policy as types in a behavioral type system for the RHO-calculus, a reflective higher-order variant of the pi-calculus.

Discussions

• Policy (in capability object systems) as Types [lobsters, 10 points, 0 comments]

Related

• Policy as Code, Policy as Type
• On Policy Reuse: An Expressive Language for Representing and Executing General Policies that Call Other Policies
• π2vec: Policy Representations with Successor Features
• Using First-Order Logic to Reason about Policies
• Curry-style type Isomorphisms and Game Semantics