We still recall very vividly the announcement of Nadia Busi's death. It was Wednesday, 5 September 2007, and we were enjoying the half-day excursion at CONCUR 2007, a conference where just before lunch on that very day some of Nadia's latest work had been presented. The weather was splendid and we were enjoying the gorgeous view from the Arrábida Convent, basking in the glorious sunlight and admiring the blue sea in the distance. Everything was a celebration of life until death struck. Mario Bravetti, one of our colleagues from Bologna, received a phone call and broke the news to us that ‘Nadia has passed away’. After receiving this message, a cloud came over all the CONCUR participants who had known her.

This paper shows how PILLY (Polymorphic Intuitionistic/Linear Lambda calculus with a fixed point combinator Y) with parametric polymorphism can be used as a metalanguage for domain theory, as originally suggested by Plotkin more than a decade ago. Using Plotkin's encodings of recursive types in PILLY, we show how parametric models of PILLY give rise to models of FPC, which is a simply typed lambda calculus with recursive types and an operational call-by-value semantics, reflecting a classical result from domain theory. Essentially, this interpretation is an interpretation of intuitionistic logic into linear logic first discovered by Girard, which in this paper is extended to deal with recursive types. Of particular interest is a model based on ‘admissible’ pers over a reflexive domain, the theory of which can be seen as a domain theory for (impredicative) polymorphism. We show how this model gives rise to a parametric and computationally adequate model of PolyFPC, an extension of FPC with impredicative polymorphism. This is to the author's knowledge the first denotational model of a non-linear language with parametric polymorphism and recursive types.

Have you ever seen the Citation Indexes (CIs) for the year 1600? At that time, a very active community was working on the reconstruction of planetary movements by means of epicycles. In principle, any ellipse around the Sun may be approximated by sufficiently many epicycles around the Earth. This is a non-trivial geometrical task, especially given the lack of analytical tools (sums of series). And the books and papers of many talented geometers quoted one another. Scientific knowledge, however, was already taking other directions. Science has a certain ‘inertia’, it is prudent (at times, it has been exceedingly so, mostly for political or metaphysical reasons), but even under the best of conditions, we all know how difficult it is to accept new ideas, to let them blossom in time, away from short-term pressures.

The structure theorem of Joyal, Street and Verity says that every traced monoidal category arises as a monoidal full subcategory of the tortile monoidal category Int. In this paper we focus on a simple observation that a traced monoidal category is closed if and only if the canonical inclusion from into Int has a right adjoint. Thus, every traced monoidal closed category arises as a monoidal co-reflexive full subcategory of a tortile monoidal category. From this, we derive a series of facts for traced models of linear logic, and some for models of fixed-point computation. To make the paper more self-contained, we also include various background results for traced monoidal categories.

In a controversial paper (De Millo et al. 1979) at the end of the 1970's, R. A. De Millo, R. J. Lipton and A. J. Perlis argued against formal verifications of programs, mostly motivating their position by an analogy with proofs in mathematics, and, in particular, with the impracticality of a strictly formalist approach to this discipline. The recent, impressive achievements in the field of interactive theorem proving provide an interesting ground for a critical revisiting of their theses. We believe that the social nature of proof and program development is uncontroversial and ineluctable, but formal verification is not antithetical to it. Formal verification should strive not only to cope with, but to ease and enhance the collaborative, organic nature of this process, eventually helping us to master the growing complexity of scientific knowledge.

The logic of Bunched Implications, through both its intuitionistic version (BI) and one of its classical versions, called Boolean BI (BBI), serves as a logical basis to spatial or separation logic frameworks. In BI, the logical implication is interpreted intuitionistically whereas it is generally interpreted classically in spatial or separation logics, as in BBI. In this paper, we aim to give some new insights into the semantic relations between BI and BBI. Then we propose a sound and complete syntactic constraints based framework for the Kripke semantics of both BI and BBI, a sound labelled tableau proof system for BBI, and a representation theorem relating the syntactic models of BI to those of BBI. Finally, we deduce as our main, and unexpected, result, a sound and faithful embedding of BI into BBI.

A longstanding open problem is whether there exists a non-syntactical model of the untyped λ-calculus whose theory is exactly the least λ-theory λβ. In this paper we investigate the more general question of whether the equational/order theory of a model of the untyped λ-calculus can be recursively enumerable (r.e. for short). We introduce a notion of effective model of λ-calculus, which covers, in particular, all the models individually introduced in the literature. We prove that the order theory of an effective model is never r.e.; from this it follows that its equational theory cannot be λβ or λβη. We then show that no effective model living in the stable or strongly stable semantics has an r.e. equational theory. For Scott's semantics, we investigate the class of graph models and prove that no order theory of a graph model can be r.e., and that there exists an effective graph model whose equational/order theory is the minimum among the theories of graph models. Finally, we show that the class of graph models enjoys a kind of downwards Löwenheim–Skolem theorem.

We investigate laws for predicate transformers for the combination of non-deterministic choice and (extended) probabilistic choice, where predicates are taken to be functions to the extended non-negative reals, or to closed intervals of such reals. These predicate transformers correspond to state transformers, which are functions to conical powerdomains, which are the appropriate powerdomains for the combined forms of non-determinism. As with standard powerdomains for non-deterministic choice, these come in three flavours – lower, upper and (order-)convex – so there are also three kinds of predicate transformers. In order to make the connection, the powerdomains are first characterised in terms of relevant classes of functionals.

Much of the development is carried out at an abstract level, a kind of domain-theoretic functional analysis: one considers d-cones, which are dcpos equipped with a module structure over the non-negative extended reals, in place of topological vector spaces. Such a development still needs to be carried out for probabilistic choice per se; it would presumably be necessary to work with a notion of convex space rather than a cone.

We describe a non-extensional variant of Martin-Löf type theory, which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories.

Several notions of non-interference have been proposed in the literature for studying the problem of confidentiality in concurrent systems. The common feature of these non-interference properties is that they are all defined as extensional properties based on some notion of behavioural equivalence on systems. Here, instead, we address the problem of defining non-interference by looking at the structure of the systems under investigation. We use a simple class of Petri nets, namely, contact-free elementary net systems, as the system model and define structural non-interference properties based on the absence of particular places in the net: such places show that a suitable causality or conflict relation is present between a high-level transition and a low-level one. We characterise one structural property, called PBNI+, which we show to be equivalent to the well-known behavioural property SBNDC. It essentially captures all the positive information flows (that is, a low-level user can deduce that some high-level action has occurred). We start by providing a characterisation of PBNI+ on contact-free elementary net systems, then extend the definition to cope with the richer class of trace nets.

Theory and Applications of Models of Computation (TAMC) is an international conference series with an interdisciplinary character bringing together researchers working in computer science, mathematics (especially logic) and the physical sciences. This interdisciplinary approach, with an emphasis on the theory of computation in a broad sense, gives the series its special appeal within China and internationally. At a time when the pressures are increasingly towards narrowly ad hoc research, and scientific fragmentation, meetings that reassert the importance of theory, fundamental concepts and a wider perspective have an important role to play.

In this paper we introduce the notions of nested constraints and application conditions, short nested conditions. For a category associated with a graphical representation such as graphs, conditions are a graphical and intuitive, yet precise, formalism that is well suited to describing structural properties. We show that nested graph conditions are expressively equivalent to first-order graph formulas. A part of the proof includes transformations between two satisfiability notions of conditions, namely -satisfiability and -satisfiability. We consider a number of transformations on conditions that can be composed to construct constraint-guaranteeing and constraint-preserving application conditions, weakest preconditions and strongest postconditions. The restriction of rule applications by conditions can be used to correct transformation systems by pruning transitions leading to states violating given constraints. Weakest preconditions and strongest postconditions can be used to verify the correctness of transformation systems with respect to pre- and postconditions.

By studying two unsharp quantum structures, namely extended lattice ordered effect algebras and lattice ordered QMV algebras, we obtain some characteristic theorems of MV algebras. We go on to discuss automata theory based on these two unsharp quantum structures. In particular, we prove that an extended lattice ordered effect algebra (or a lattice ordered QMV algebra) is an MV algebra if and only if a certain kind of distributive law holds for the sum operation. We introduce the notions of (quantum) finite automata based on these two unsharp quantum structures, and discuss closure properties of languages and the subset construction of automata. We show that the universal validity of some important properties (such as sum, concatenation and subset constructions) depend heavily on the above distributive law. These generalise results about automata theory based on sharp quantum logic.

The aim of the research domain known as process mining is to use process discovery to construct a process model as an abstract representation of event logs. The goal is to build a model (in terms of a Petri net) that can reproduce the logs under consideration, and does not allow different behaviours compared with those shown in the logs. In particular, process mining aims to verify the accuracy of the model design (represented as a Petri net), basically checking whether the same net can be rediscovered. However, the main mining methods proposed in the literature have some drawbacks: the classical α-algorithm is unable to rediscover various nets, while the region-based approach, which can mine them correctly, is too complex.

In this paper, we compare different approaches and propose some ideas to counter the weaknesses of the region-based approach.

Given a partial metric space (X, p), we use (BX, ⊑dp) to denote the poset of formal balls of the associated quasi-metric space (X, dp). We obtain characterisations of complete partial metric spaces and sup-separable complete partial metric spaces in terms of domain-theoretic properties of (BX, ⊑dp). In particular, we prove that a partial metric space (X, p) is complete if and only if the poset (BX, ⊑dp) is a domain. Furthermore, for any complete partial metric space (X, p), we construct a Smyth complete quasi-metric q on BX that extends the quasi-metric dp such that both the Scott topology and the partial order ⊑dp are induced by q. This is done using the partial quasi-metric concept recently introduced and discussed by H. P. Künzi, H. Pajoohesh and M. P. Schellekens (Künzi et al. 2006). Our approach, which is inspired by methods due to A. Edalat and R. Heckmann (Edalat and Heckmann 1998), generalises to partial metric spaces the constructions given by R. Heckmann (Heckmann 1999) and J. J. M. M. Rutten (Rutten 1998) for metric spaces.

We study a measurement-free, untyped λ-calculus with quantum data and classical control. This work arises from previous proposals by Selinger and Valiron, and Van Tonder. We focus on operational and expressiveness issues, rather than (denotational) semantics. We prove subject reduction and confluence, and a standardisation theorem. Moreover, we prove the computational equivalence of the proposed calculus with a suitable class of quantum circuit families.

The compact-open topology on the set of continuous functionals from the Baire space to the natural numbers is well known to be zero-dimensional. We prove that the closely related sequential topology on this set is not even regular. The sequential topology arises naturally as the topology carried by the exponential formed in various cartesian closed categories of topological spaces. Moreover, we give an example of an effectively open subset of that violates regularity. The topological properties of are known to be closely related to an open problem in Computable Analysis. We also show that the sequential topology on the space of continuous real-valued functions on a Polish space need not be regular.

A random multivariate polynomial system with more equations than variables is likely to be unsolvable. On the other hand, if there are more variables than equations, the system has at least one solution with high probability. In this paper we study in detail the phase transition between these two regimes, which occurs when the number of equations equals the number of variables. In particular, the limiting probability for no solution is 1/e at the phase transition, over a prime field.

We also study the probability of having exactly s solutions, with s ≥ 1. In particular, the probability of a unique solution is asymptotically 1/e if the number of equations equals the number of variables. The probability decreases very rapidly if the number of equations increases or decreases.

Our motivation is that many cryptographic systems can be expressed as large multivariate polynomial systems (usually quadratic) over a finite field. Since decoding is unique, the solution of the system must also be unique. Knowing the probability of having exactly one solution may help us to understand more about these cryptographic systems. For example, whether attacks should be evaluated by trying them against random systems depends very much on the likelihood of a unique solution.

The investigation into the foundational aspects of linguistic mechanisms for programming long-running transactions (such as the scope operator of WS-BPEL) has recently renewed the interest in process algebraic operators that, due to the occurrence of a failure, interrupt the execution of one process, replacing it with another one called the failure handler. We investigate the decidability of termination problems for two simple fragments of CCS (one with recursion and one with replication) extended with one of two such operators, the interrupt operator of CSP and the try-catch operator for exception handling. More precisely, we consider the existential termination problem (existence of one terminated computation) and the universal termination problem (all computations terminate). We prove that, as far as the decidability of the considered problems is concerned, under replication there is no difference between interrupt and try-catch (universal termination is decidable while existential termination is not), while under recursion this is not the case (existential termination is undecidable while universal termination is decidable only for interrupt). As a consequence of our undecidability results, we show the existence of an expressiveness gap between a fragment of CCS and its extension with either the interrupt or the try-catch operator.

Mathematical modelling is one of the fundamental tools of science and engineering. Very often, models are required to be executable, as a simulation, on a computer. In this paper, we present some contributions to the process-theoretic and logical foundations of discrete-event modelling with resources and processes. We present a process calculus with an explicit representation of resources in which processes and resources co-evolve. The calculus is closely connected to a logic that may be used as a specification language for properties of models. The logic is strong enough to allow requirements that a system has a certain structure: for example, that it is a parallel composite of subsystems. This work consolidates, extends and improves upon aspects of earlier work of ours in this area. An extended example, consisting of a semantics for a simple parallel programming language, indicates a connection with separating logics for concurrency.