We use hidden Markov models to motivate a quantitative compositional semantics for noninterference-based security with iteration, including a refinement- or ‘implements’ relation that compares two programs with respect to their information leakage; and we propose a program algebra for source-level reasoning about such programs, in particular as a means of establishing that an ‘implementation’ program leaks no more than its ‘specification’ program.

This joins two themes: we extend our earlier work, having iteration but only qualitative (Morgan 2009), by making it quantitative; and we extend our earlier quantitative work (McIver et al. 2010) by including iteration.

We advocate stepwise refinement and source-level program algebra – both as conceptual reasoning tools and as targets for automated assistance. A selection of algebraic laws is given to support this view in the case of quantitative noninterference; and it is demonstrated on a simple iterated password-guessing attack.

In Fajstrup et al. (1998a) the authors proposed a fast algorithm for deadlock detection, which was based on a geometric model of concurrency. We propose here an extension of this approach to deal with recursive processes (loops) and branchings.

Lambek used categories with indeterminates to capture explicit variables in simply typed λ-calculus. He observed that such categories with indeterminates can be described as Kleisli categories for suitable comonads. They account for ‘functional completeness’ for Cartesian (closed) categories.

Here we refine this analysis, by distinguishing ‘contextual’ and ‘functional’ completeness, and extend it to polymorphic λ-calculi. Since the latter are described as certain fibrations, we are lead to consider indeterminates, not only for ordinary categories, but also for fibred categories. Following a 2-categorical generalisation of Lambek's approach, such fibrations with indeterminates are presented as 'simple slices' in suitable 2-categories of fibrations; more precisely, as Kleisli objects. It allows us to establish contextual and functional completeness results for some polymorphic calculi.

By establishing an appropriate equivalence, we observe that the theory of semi-functors can be fully embedded in the theory of (ordinary) functors. As a result, standard properties and constructions on functors extend automatically to semi-functors.

We study a general algebraic framework that underlies a wide range of computational formalisms that use the notion of names, notably process calculi. The algebraic framework gives a rigorous basis for describing and reasoning about processes semantically, as well as offering new insights into existing constructions. The formal status of the theory is elucidated by introducing its alternative presentation, which is geometric in nature and is based on explicit manipulation of connections among nameless processes. Nameless processes and their relational theory form a coherent universe in their own right, which underlies existing graphical formalisms such as proof nets. We establish the formal equivalence between these two presentations, and illustrate how they can be used complementarily for the precise and effective description of diverse algebras and the dynamics of processes through examples.

This paper deals with runtime enforcement of untimed and timed properties with uncontrollable events. Runtime enforcement consists in defining and using mechanisms that modify the executions of a running system to ensure their correctness with respect to a desired property. We introduce a framework that takes as input any regular (timed) property described by a deterministic automaton over an alphabet of events, with some of these events being uncontrollable. An uncontrollable event cannot be delayed nor intercepted by an enforcement mechanism. Enforcement mechanisms should satisfy important properties, namely soundness, compliance and optimality – meaning that enforcement mechanisms should output as soon as possible correct executions that are as close as possible to the input execution. We define the conditions for a property to be enforceable with uncontrollable events. Moreover, we synthesise sound, compliant and optimal descriptions of runtime enforcement mechanisms at two levels of abstraction to facilitate their design and implementation.

We propose a formalization of standard database management systems using topos theory. In this treatment, all constructions take place within an ambient topos, which thereby serves as the ‘universe of discourse’. A database schema is defined using objects and morphisms in the ambient topos. A database state for a given schema involves not only the ambient topos but also an internal category within the topos. This approach neatly separates the schema from the state data by placing them in distinct category structures. It is shown that database states can either be regarded syntactically as objects in an external topos or semantically as morphisms in an internal slice category. A number of operations are introduced that correspond to operations used in standard database systems. Extraction selects some of the tables, attributes and domains of a database state. The squeeze operation performs an ‘elimination of duplicates’, which can be combined with extraction to obtain an operation called ‘projection’ in standard relational database systems. A join operation is defined, which generalizes the relational join operation and can be used for the cartesian product and selection operations. Finally, ‘boolean’ operations of intersection, union and difference are introduced and related to the other operations.

The partially ordered models of linear logic, a logical system developed by J. Y. Girard, turn out to be a class of quantales called Girard quantales. The notion of a quantaloid is a natural categorical generalization of a quantale and is one possible way of keeping track of types. In this paper, Girard quantales are generalized to Girard quantaloids. The general theory is developed and several key examples are studied. Turning our attention to the theory of categories enriched in a bicategory, it is then shown that if G is a Girard quantaloid, then the quantaloids Bim(G), Matr(G), and Mon(G), consisting of G-bimodules, G-matrices and G-monads respectively, are also Girard quantaloids.

The subtyping relation defined for dyadic session type theories may compromise the liveness of multi-party sessions. In this paper, we define a fair subtyping relation for multi-party session types that preserves liveness, we relate it with the subtyping relation for dyadic session types and provide coinductive, axiomatic and algorithmic characterizations for it.

Lipschitz continuity is used as a tool for analysing the relationship between incomputability and randomness. We present a simpler proof of one of the major results in this area – the theorem of Yu and Ding, which states that there exists no cl-complete c.e. real – and go on to consider the global theory. The existential theory of the cl degrees is decidable, but this does not follow immediately by the standard proof for classical structures, such as the Turing degrees, since the cl degrees are a structure without join. We go on to show that strictly below every random cl degree there is another random cl degree. Results regarding the phenomenon of quasi-maximality in the cl degrees are also presented.

We study usage automata, a formal model for specifying policies on the usage of resources. Usage automata extend finite state automata with some additional features, parameters and guards, that improve their expressivity. We show that usage automata are expressive enough to model policies of real-world applications. We discuss their expressive power, and we prove that the problem of telling whether a computation complies with a usage policy is decidable. The main contribution of this paper is a model checking technique for usage automata. The model is that of usages, i.e. basic processes that describe the possible patterns of resource access and creation. In spite of the model having infinite states, because of recursion and resource creation, we devise a polynomial-time model checking technique for deciding when a usage complies with a usage policy.

The notion of a dynamic labeled 2-structure(dℓ2s) is introduced and investigated. It generalizes the notion of a labeled 2-structure (ℓ2s) (Ehrenfeucht and Rozenberg 1990), by making it possible to change the (label) relationships between the nodes. This is achieved by storing in the nodes of a ℓ2s output and input functions that can change the outgoing and incoming labels, respectively. The notion of a clan, which is central in the theory of ℓ2s's is transferred to the framework of dℓ2s's, and the basic properties of clans of dℓ2s's are investigated.

The three classical process algebras CCS, CSP and ACP present several differences in their respective technical machinery. This is due, not only to the difference in their operators, but also to the terminology and ‘way of thinking’ of the community that has been (and still is) working with them. In this paper we will first discuss these differences and try to clarify the different usage of terminology and concepts. Then, as a result of this discussion, we define a generic process algebra where each of the basic mechanisms of the three process algebras (including minimal fixpoint based unguarded recursion) is expressed by an operator, and which can be used as an underlying common language. We show an example of the advantages of adopting such a language instead of one of the three more specialised algebras: producing a complete axiomatisation for Milner's observational congruence in the presence of (unguarded) recursion and static operators. More precisely, we provide a syntactical characterisation (allowing as many terms as possible) for the equations involved in recursion operators, which guarantees that transition systems generated by the operational semantics are finite state. Conversely, we show that every process admits a specification in terms of such a restricted form of recursion. We then present an axiomatisation that is ground complete over such a restricted signature. Notably, we also show that the two standard axioms of Milner for weakly unguarded recursion can be expressed using a single axiom only.

The purpose of this note is to show that the correctness of a multiplicative proof net with mix is equivalent to its semantic correctness: a proof structure is a proof net if and only if its semantic interpretation is a clique, where one given finite coherence space interprets all propositional variables.

This is just an example of what can be done with these kinds of semantic techniques; for more information and further results, the reader is referred to Retoré (1994).

In earlier work we explored the expressiveness and algebraic theory Psi-calculi, which form a parametric framework for extensions of the pi-calculus. In the current paper we consider higher-order psi-calculi through a technically surprisingly simple extension of the framework, and show how an arbitrary psi-calculus can be lifted to its higher-order counterpart in a canonical way. We illustrate this with examples and establish an algebraic theory of higher-order psi-calculi. The formal results are obtained by extending our proof repositories in Isabelle/Nominal.

The stringent security requirements of organisations like banks or hospitals frequently adopt role-based access control (RBAC) principles to represent and simplify their internal permission management. While representing a fundamental advanced RBAC concept enabling precise restrictions on access rights, authorisation constraints increase the complexity of the resulting security policies so that tool support for convenient creation and adequate validation is required. A particular contribution of our work is a new approach to developing and analysing RBAC policies using a UML-based domain-specific language (DSL), which allows the hiding of the mathematical structures of the underlying authorisation constraints implemented in OCL. The DSL we present is highly configurable and extensible with respect to new concepts and classes of authorisation constraints, and allows the developer to validate RBAC policies in an effective way. The handling of dynamic (that is, time-dependent) constraints, their visual representation through the RBAC DSL and their analysis all form another part of our contribution. The approach is supported by a UML and OCL validation tool.

We address the question of injectivity of coherent semantics of linear logic proof-nets. Starting from Girard's definition of experiment, we introduce the key-notion of ‘injective obsessional experiment’, which allows us to give a positive answer to our question for certain fragments of linear logic, and to build counter-examples to the injectivity of coherent semantics in the general case.

Non-interference guarantees the absence of illicit information flow throughout program execution. It can be enforced by appropriate information flow type systems. Much of the previous work on type systems for non-interference has focused on calculi or high-level programming languages, and existing type systems for low-level languages typically omit objects, exceptions and method calls. We define an information flow type system for a sequential JVM-like language that includes all these programming features, and we prove, in the Coq proof assistant, that it guarantees non-interference. An additional benefit of the formalisation is that we have extracted from our proof a certified lightweight bytecode verifier for information flow. Our work provides, to the best of our knowledge, the first sound and certified information flow type system for such an expressive fragment of the JVM.

The $\lambda$-calculus is destructive: its main computational mechanism, beta reduction, destroys the redex, which makes replaying the computational steps impossible. Combinatory logic is a variant of the $\lambda$-calculus that maintains irreversibility. Recently, reversible computational models have been studied mainly in the context of quantum computation, as (without measurements) quantum physics is inherently reversible. However, reversibility also fundamentally changes the semantical framework in which classical computation has to be investigated. We describe an implementation of classical combinatory logic in a reversible calculus for which we present an algebraic model based on a generalisation of the notion of a group.

Seely's paper Locally cartesian closed categories and type theory (Seely 1984) contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-Löf type theories with Π, Σ and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the Bénabou–Hofmann interpretation of Martin-Löf type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development, we employ categories with families as a substitute for syntactic Martin-Löf type theories. As a second result, we prove that if we remove Π-types, the resulting categories with families with only Σ and extensional identity types are biequivalent to left exact categories.