Interference and dependence are closely related concepts: interference being the observable phenomenon connected with dependence. Essentially, interference means that the behaviour of some parts of a dynamic system may influence the behaviour of other parts of the same system, while dependence specifies how the semantics of sub-components of a dynamic system are related. Identifying, measuring and controlling interference is essential in many aspects of modern computer science, in particular, in security, program analysis and verification, debugging, systems specification, model checking, program manipulation, program slicing, reverse engineering, data mining, distributed databases and systems biology. In all these fields, dependency and interference play a key role in designing suitable abstractions or in partitioning complex systems into simpler ones. Reasoning about dependency and interference requires theories, models and semantics, as well as algorithms and tools for their analysis. Beginning in 2004, the series of Programming Language Interference and Dependence (PLID) workshops has been devoted to promoting and spreading cutting-edge research in this field, with a particular emphasis on unpublished results with great impact on the theoretical basis. PLID2007, which was held at the The Technical University of Denmark on 21 August 2007, was particularly successful, and constituted the ideal forum for announcing a call for papers for a special journal issue on programming language interference and dependence, which would not necessarily be restricted to PLID2007 contributions. From the many expressions of interest, we selected six contributions by leading researchers in the field, some of which had been presented at the PLID2007 workshop. The selected papers focus on foundational aspects of dependency and interference, with applications in language-based security, data-base management systems and program slicing.

A general approach is proposed for transforming objects to methods on the fly in the framework of the π-calculus. The power of the approach is demonstrated by applying it to generate an encoding of the full lambda calculus in the π-calculus. The encoding is proved to preserve and reflect beta reduction, and is shown to be fully abstract with respect to Abramsky's applicative bisimilarity.

We establish Choquet–Kendall–Matheron theorems on non-Hausdorff topological spaces. This typical result of random set theory is profitably recast in purely topological terms using intuitions and tools from domain theory. We obtain three variants of the theorem, each one characterising distributions, in the form of continuous valuations, over relevant powerdomains of demonic, angelic and erratic non-determinism, respectively.

In (hyper)coherence semantics, proofs/terms are cliques in (hyper)graphs. Intuitively, the vertices represent the results of computations and the edge relation witnesses the ability to carry out the computation assembled into a single piece of data or a single (strongly) stable function, at arrow types.

In (hyper)coherence semantics, the argument of a (strongly) stable functional is always a (strongly) stable function. As a consequence, compared to the relational semantics where there is no edge relation, some vertices are missing. Recovering these vertices is essential if we are to reconstruct proofs/terms from their interpretations. It will also be useful for comparing with other semantics, such as game semantics.

Bucciarelli and Ehrhard (2001) introduced a non-uniform coherence space semantics, where no vertex is missing. By constructing the co-free exponential, we get a new version of this semantics, together with non-uniform versions of hypercoherences and multicoherences. This provides a new semantics in which an edge is a finite multiset. Thanks to the co-free construction, these non-uniform semantics are deterministic in the sense that the intersection of a clique and an anti-clique contains at most one vertex, which is a result of interaction, and they then extensionally collapse onto the corresponding uniform semantics.

The Coalgebraic Logic seminar took place between the 6th and 9th of December 2009 at the Leibniz Forschungszentrum Schloss Dagstuhl. The event was very well received, with more than 35 scientists from Europe, the United States, Canada and China attending, and with more than thirty presentations during the three days. Given the unforeseen enthusiasm of the meeting's reception, we thought that it would be a good idea for us to put together a special journal issue dedicated to this topic. We were also encouraged by the positive response we received from Guiseppe Longo, who indicated his interest in a special issue for Mathematical Structures in Computer Science, and here we are.

This special issue of Mathematical Structures in Computer Science is devoted to the theme of ‘Interactive theorem proving and the formalisation of mathematics’.

The formalisation of mathematics started at the turn of the 20th century when mathematical logic emerged from the work of Frege and his contemporaries with the invention of the formal notation for mathematical statements called predicate calculus. This notation allowed the formulation of abstract general statements over possibly infinite domains in a uniform way, and thus went well beyond propositional calculus, which goes back to Aristotle and only allowed tautologies over unquantified statements.

Nominal sets are a sets-based first-order denotation for variables in logic and programming. In this paper we extend nominal sets to two-level nominal sets. These preserve much of the behaviour of nominal sets, including notions of variable and abstraction, but they include a denotation for both variables and meta-variables. Meta-variables are interpreted as infinite lists of distinct variable symbols. We use two-level sets to define, amongst other things, a denotation for meta-variable abstraction, and nominal style datatypes of syntax-with-binding with meta-variables. We discuss the connections between this and nominal terms and prove a soundness result.

System NEL is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials, or, equivalently, it is MELL augmented with the non-commutative self-dual connective seq. NEL is presented in deep inference, because no Gentzen formalism can express it in such a way that the cut rule is admissible. Other recent work shows that system NEL is Turing-complete, and is able to express process algebra sequential composition directly and model causal quantum evolution faithfully. In this paper, we show cut elimination for NEL, based on a technique that we call splitting. The splitting theorem shows how and to what extent we can recover a sequent-like structure in NEL proofs. When combined with a ‘decomposition’ theorem, proved in the previous paper of this series, splitting yields a cut-elimination procedure for NEL.

In this survey we discuss the generalisation of stochastic Kripke models for general modal logics through predicate liftings for functors over general measurable spaces. We derive results on expressivity and show that selection arguments allow us to incorporate the discussion of bisimilarity, provided the underlying spaces are assumed to be standard Borel.

N. G. de Bruijn, now professor emeritus of the Eindhoven University of Technology, was a pioneer in the field of interactive theorem proving. From 1967 to the end of the 1970's, his work on the Automath system introduced the architecture that is common to most of today's proof assistants, and much of the basic technology. But de Bruijn was a mathematician first and foremost, as evidenced by the many mathematical notions and results that bear his name, among them de Bruijn sequences, de Bruijn graphs, the de Bruijn–Newman constant, and the de Bruijn–Erdös theorem. The quotation above is thus interesting not because it is a reflection on his expertise in formal verification, but, rather, of his convictions as a working mathematician.

We generalise the construction of the formal ball model for metric spaces due to A. Edalat and R. Heckmann in order to obtain computational models for separated -categories. We fully describe -categories that are

1. (a) Yoneda complete

2. (b) continuous Yoneda complete

1. (a) a quasi-metric space X is Yoneda complete if and only if its formal ball model is a dcpo, and

2. (b) a quasi-metric space X is continuous and Yoneda complete if and only if its formal ball model BX is a domain that admits a simple characterisation of approximation.

With the emergence of the new possibilities offered by global computing, new security issues follow from the fact that these possibilities can be equally exploited by parties with malicious intentions. Many attacks arise at the application level, and can be tackled by means of programming language techniques. For instance, confidentiality can be violated during the execution of programs that reveal secret information. This kind of program behaviour can be avoided by information flow analyses that detect the encoding of illegal flows.

This paper studies information flows that occur in distributed programs with code mobility from a language-based security perspective. New forms of security leaks that are introduced by code mobility, which we call migration leaks, are presented and compared with well-known forms of illegal flow. We propose an information flow property that is adequate for networks consisting of a generalisation of the non-disclosure policy. We design a type and effect system for enforcing it on an expressive distributed calculus, and explain a soundness proof methodology in detail.

In secure information flow analysis, the classic Denning restrictions allow a program's termination to be affected by the values of its H variables, resulting in potential information leaks. In an effort to quantify such leaks, in this paper we study a simple imperative language with random assignments. As a thought experiment, we propose a ‘stripping’ operation on programs, which eliminates all ‘high computation’, and prove the fundamental property that stripping cannot decrease the probability of any low outcome. To prove this property, we first introduce a new notion of fast probabilistic simulation on Markov chains and show that it implies a key reachability property. Viewing the stripping function as a binary relation, we then prove that stripping is a fast simulation. As an application, we prove that, under the Denning restrictions, well-typed probabilistic programs are guaranteed to satisfy an approximate probabilistic non-interference property, provided that their probability of non-termination is small.

Partial iterative theories are algebraic theories such that for certain morphisms f the equation ξ = f ⋅ 〈ξ, 1p〉 has a unique solution. Iteration theories are algebraic theories satisfying a certain set of identities. We investigate some similarities between partial iterative theories and iteration theories.

In our main result, we give a sufficient condition ensuring that the partially defined dagger operation of a partial iterative theory can be extended to a totally defined operation so that the resulting theory becomes an iteration theory. We show that this general extension theorem can be instantiated to prove that every Elgot iterative theory with at least one constant morphism 1 → 0 can be extended to an iteration theory. We also apply our main result to theories equipped with an additive structure.

Game semantics describe the interactive behaviour of proofs by interpreting formulas as games on which proofs induce strategies. Such a semantics is introduced here for capturing dependencies induced by quantifications in first-order propositional logic. One of the main difficulties that has to be faced during the elaboration of this kind of semantics is to characterise definable strategies, that is, strategies that actually behave like a proof. This is usually done by restricting the model to strategies satisfying subtle combinatorial conditions, whose preservation under composition is often difficult to show. In this paper we present an original methodology to achieve this task, which requires a combination of advanced tools from game semantics, rewriting theory and categorical algebra. We introduce a diagrammatic presentation of the monoidal category of definable strategies of our model using generators and relations: these strategies can be generated from a finite set of atomic strategies, and the equality between strategies admits a finite axiomatisation, and this equational structure corresponds to a polarised variation of the bialgebra notion. The work described in this paper thus forms a bridge between algebra and denotational semantics in order to reveal the structure of dependencies induced by first-order quantifiers, and lays the foundations for a mechanised analysis of causality in programming languages.

State-based systems and modal logics for reasoning about them often heterogeneously combine a number of features such as non-determinism and probabilities. In this paper, we show that the combination of features can be reflected algorithmically, and we develop modular decision procedures for heterogeneous modal logics. The modularity is achieved by formalising the underlying state-based systems as multi-sorted coalgebras and associating both a logical and algorithmic description with a number of basic building blocks. Our main result is that logics arising as combinations of these building blocks can be decided in polynomial space provided this is also the case for the components. By instantiating the general framework to concrete cases, we obtain PSpace decision procedures for a wide variety of structurally different logics, describing, for example, Segala systems and games with uncertain information.

The Hybrid system (Ambler et al. 2002b), implemented within Isabelle/HOL, allows object logics to be represented using higher order abstract syntax (HOAS), and reasoned about using tactical theorem proving in general, and principles of (co)induction in particular. The form of HOAS provided by Hybrid is essentially a lambda calculus with constants.

Of fundamental interest is the form of the lambda abstractions provided by Hybrid. The user has the convenience of writing lambda abstractions using names for the binding variables. However, each abstraction is actually a definition of a de Bruijn expression, and Hybrid can unwind the user's abstractions (written with names) to machine friendly de Bruijn expressions (without names). In this sense the formal system contains a hybrid of named and nameless bound variable notation.

In this paper, we present a formal theory in a logical framework, which can be viewed as a model of core Hybrid, and state and prove that the model is representationally adequate for HOAS. In particular, it is the canonical translation function from λ-expressions to Hybrid that witnesses adequacy. We also prove two results that characterise how Hybrid represents certain classes of λ-expression.

We provide the first detailed proof to be published that proper locally nameless de Bruijn expressions and α-equivalence classes of λ-expressions are in bijective correspondence. This result is presented as a form of de Bruijn representational adequacy, and is a key component of the proof of Hybrid adequacy.

The Hybrid system contains a number of different syntactic classes of expression, and associated abstraction mechanisms. Hence, this paper also aims to provide a self-contained theoretical introduction to both the syntax and key ideas of the system. Although this paper will be of considerable interest to those who wish to work with Hybrid in Isabelle/HOL, a background in automated theorem proving is not essential.

We discuss a formal development for the certification of Newton's method. We address several issues encountered in the formal study of numerical algorithms: developing the necessary libraries for our proofs, adapting paper proofs to suit the features of a proof assistant and designing new proofs based on the existing ones to deal with optimisations of the method. We start from Kantorovitch's Theorem, which gives the convergence of Newton's method in the case of a system of equations. To formalise this proof inside the proof assistant Coq, we first need to code the necessary concepts from multivariate analysis. We also prove that rounding at each step in Newton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. This proof is based on Kantorovitch's Theorem, but is an original result. An algorithm including rounding is a more accurate model for computations with Newton's method in practice.

Pick's Theorem relates the area of a simple polygon with vertices at integer lattice points to the number of lattice points in its inside and boundary. We describe a formal proof of this theorem using the HOL Light theorem prover. As sometimes happens for highly geometrical proofs, the formalisation turned out to be more work than initially expected. The difficulties arose mostly from formalising the triangulation process for an arbitrary polygon.

Information flow policies are confidentiality policies that control information leakage through program execution. A common way to enforce secure information flow is through information flow type systems. Although type systems are compositional and usually enjoy decidable type checking or inference, their extensibility is very poor: type systems need to be redefined and proved sound for each new variation of security policy and programming language for which secure information flow verification is desired.

In contrast, program logics offer a general mechanism for enforcing a variety of safety policies, and for this reason are favoured in Proof Carrying Code, which is a promising security architecture for mobile code. However, the encoding of information flow policies in program logics is not straightforward because they refer to a relation between two program executions.

The purpose of this paper is to investigate logical formulations of secure information flow based on the idea of self-composition, which reduces the problem of secure information flow of a program P to a safety property for a program derived from P by composing P with a renaming of itself. Self-composition enables the use of standard techniques for information flow policy verification, such as program logics and model checking, that are suitable in Proof Carrying Code infrastructures.

We illustrate the applicability of self-composition in several settings, including different security policies such as non-interference and controlled forms of declassification, and programming languages including an imperative language with parallel composition, a non-deterministic language and, finally, a language with shared mutable data structures.