Authorization is a fundamental problem in modern distributed systems, and the ''policies-as-code'' paradigm has emerged as a promising solution to decouple access control logic from application code. However, most policy languages lack the ability to handle stateful policies directly. This limitation forces developers to manage policy-related state within the application code, reintroducing the very coupling that policies as code aims to eliminate and opening the door to security vulnerabilities. To address this gap, we introduce Strobilus, a language designed to express effects over policy-specific data. Strobilus is built to seamlessly complement and integrate with Amazon's Cedar, allowing developers to write stateful policies without modifying Cedar's core syntax or evaluation engine. Strobilus is distinguished by its formal semantics, a strong typing system, and a guarantee of termination, which facilitates rigorous analysis and verification of policies. We have developed a prototype implementation in Rust, which demonstrates that Strobilus may lead to significant performance improvements over external methods for policy data management. This approach aims to fully realizes the promise of ''policies-as-code'' by providing a comprehensive, safe, and verifiable solution for both stateless and stateful authorization policies.

We present a novel, yet rather simple construction within the traditional framework of Scott domains to provide semantics to probabilistic programming, thus obtaining a solution to a long-standing open problem in this area. We work with the Scott domain of random variables from a standard and fixed probability space---the unit interval or the Cantor space---to any given Scott domain. The map taking any such random variable to its corresponding probability distribution provides a Scott continuous surjection onto the probabilistic power domain of the underlying Scott domain, which preserving canonical basis elements, establishing a new basic result in classical domain theory. If the underlying Scott domain is effectively given, then this map is also computable. We obtain a Cartesian closed category by enriching the category of Scott domains by a partial equivalence relation to capture the equivalence of random variables on these domains. The constructor of the domain of random variables on this category, with the two standard probability spaces, leads to four basic strong commutative monads, suitable for defining the semantics of probabilistic programming.

Abstract Session types are a well-established framework for the specification of interactions between components of a distributed systems. An important issue is how to determine the type for an open system, i.e., obtained by assembling subcomponents, some of which could be missing. To this end, we introduce partial sessions and partial (multiparty) session types. Partial sessions can be composed, and the type of the resulting system is derived from those of its components without knowing any suitable global type nor the types of missing parts. To deal with this incomplete information, partial session types represent the subjective views of the interactions from participants’ perspectives; when sessions are composed, different partial views can be merged if compatible, yielding a unified view of the session. Incompatible types, due to, e.g., miscommunications or deadlocks, are detected at the merging phase. In fact, in this theory the distinction between global and local types vanishes. We apply these types to a process calculus for which we prove subject reduction and progress, so that well-typed systems never violate the prescribed constraints. In particular, we introduce a generalization of the progress property, in order to accommodate the case when a partial session cannot progress not due to a deadlock, but because some participants are still missing. Therefore, partial session types support the development of systems by incremental assembling of components.

The aim of this work is to correlate two different approaches to the semantics of programming languages: game semantics and intersection type assignment systems (ITAS). Namely, we present an ITAS that provides the description of the semantic interpretation of a typed lambda calculus in a game model based on innocent strategies. Compared to the traditional ITAS used to describe the semantic interpretation in domain theoretic models, the ITAS presented in this paper has two main differences: the introduction of a notion of labelling on moves, and the omission of several rules, i.e. the subtyping rules and some structural rules.

In this paper we investigate, in the context of functional prototype-based languages, objects which might extend themselves upon receiving a message. The possibility for an object of extending its own "self", referred to by Cardelli, as a self-inflicted operation, is novel in the context of typed object-based languages. We present a sound type system for this calculus which guarantees that evaluating a well-typed expression will never yield a message-not-found run-time error. We give several examples which illustrate the increased expressive power of our system with respect to existing calculi of objects. The new type system allows also for a flexible width-subtyping, still permitting sound method override, and a limited form of object extension. The resulting calculus appears to be a good starting point for a rigorous mathematical analysis of class-based languages.