Programs emit intents checked against policies by a governed runtime before effects occur, with formal specification, Rocq verification of 454 theorems, and BEAM implementation.
hub
IEEE Journal of Selected Areas in Communications 21, 1 (2003), 5–19
4 Pith papers cite this work, alongside 1,893 external citations. Polarity classification is still indexing.
4
Pith papers citing it
1,893
external citations · external index
hub tools
verdicts
UNVERDICTED 4representative citing papers
Extends logical relations to recursive session types for PSNI, proves soundness/completeness via biorthogonality with observation-index stratification, and gives an IFC refinement type system with secrecy polymorphism.
LBAC is a new programming model that enforces user-specified policies on agentic applications by requiring agent-generated programs to be well-typed in the context of the scaffolding code.
AI agents can generate code in a capability-safe Scala dialect that statically prevents information leakage and malicious side effects while preserving task performance.
citing papers explorer
-
Intent-Driven Computing: A Computational Model for Governed Autonomous Systems
Programs emit intents checked against policies by a governed runtime before effects occur, with formal specification, Rocq verification of 454 theorems, and BEAM implementation.
-
Logical Relations for Session-Typed Concurrency
Extends logical relations to recursive session types for PSNI, proves soundness/completeness via biorthogonality with observation-index stratification, and gives an IFC refinement type system with secrecy polymorphism.
-
Language-Based Agent Control
LBAC is a new programming model that enforces user-specified policies on agentic applications by requiring agent-generated programs to be well-typed in the context of the scaffolding code.
-
Tracking Capabilities for Safer Agents
AI agents can generate code in a capability-safe Scala dialect that statically prevents information leakage and malicious side effects while preserving task performance.