For a $T_0$ space X, let $\mathsf{K}(X)$ be the poset of all nonempty compact saturated subsets of X endowed with the Smyth order $\sqsubseteq$. $(\mathsf{K}(X), \sqsubseteq)$ (shortly $\mathsf{K}(X)$) is called the Smyth power poset of X. In this paper, we mainly discuss some basic properties of the Scott topology on Smyth power posets. It is proved that for a well-filtered space X, its Smyth power poset $\mathsf{K}(X)$ with the Scott topology is still well-filtered, and a $T_0$ space Y is well-filtered iff the Smyth power poset $\mathsf{K}(Y)$ with the Scott topology is well-filtered and the upper Vietoris topology is coarser than the Scott topology on $\mathsf{K}(Y)$. A sober space Z is constructed for which the Smyth power poset $\mathsf{K}(Z)$ with the Scott topology is not sober. A few sufficient conditions are given for a $T_0$ space X under which its Smyth power poset $\mathsf{K}(X)$ with the Scott topology is sober. Some other properties, such as local compactness, first-countability, Rudin property and well-filtered determinedness, of Smyth power spaces, and the Scott topology on Smyth power posets, are also investigated.

We use the technique of “classical realizability” to build new models of ZF + DC in which R is not well ordered. This gives new relative consistency results, which are not obtainable by forcing. This gives also a new method to get programs from proofs of arithmetical formulas with dependent choice.

The flow shop scheduling problem based on ideal and precise conditions has been a focus of considerable research since the first easy scheduling problem was formulated. In reality, some uncertain factors always restrict the scheduling optimisation problem. In this paper, taking uncertain processing time as an example, we use generalised rough sets theory to transform the rough flow shop scheduling model into the precise scheduling model. We adopt a cooperative co-evolutionary particle swarm optimisation algorithm based on a niche sharing scheme (NCPSO) to minimise the makespan in comparison with the particle swarm optimiser (PSO) and co-evolution particle swarm optimiser (CPSO) algorithms. The new algorithm is characterised by a strengthening of the ability to reserve excellent particles and searching the optimal solution. Experimental results show that the new algorithm is more effective and efficient than the others.

We introduce a new fragment of linear temporal logic (LTL) called LIO and a new class of Büchi automata (BA) called almost linear Büchi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. As we expect there to be applications of our results in model checking, we use two standard sources of specification formulae, namely Spec Patterns and BEEM, to study the practical relevance of the LIO fragment, and to compare our translation of LIO to ALBA with two standard translations of LTL to BA using alternating automata. Finally, we demonstrate that the LIO to ALBA translation can be much faster than the standard translation, and the resulting automata can be substantially smaller.

This paper presents a proof-theoretic observation about two kinds of proof systems for bisimilarity between cyclic term graphs.

First we consider proof systems for demonstrating that μ term specifications of cyclic term graphs have the same tree unwinding. We establish a close connection between adaptations for μ terms over a general first-order signature of the coinductive axiomatisation of recursive type equivalence by Brandt and Henglein (Brandt and Henglein 1998) and of a proof system by Ariola and Klop (Ariola and Klop 1995) for consistency checking. We show that there exists a simple duality by mirroring between derivations in the former system and formalised consistency checks, which are called ‘consistency unfoldings', in the latter. This result sheds additional light on the axiomatisation of Brandt and Henglein: it provides an alternative soundness proof for the adaptation considered here.

We then outline an analogous duality result that holds for a pair of similar proof systems for proving that equational specifications of cyclic term graphs are bisimilar.

We present a simple module calculus where selection and execution of a component is possible on open modules, that is, modules that still need to import some external definitions. Hence, it provides a kernel model for a computational paradigm in which standard execution (that is, execution of a single computation described by a fragment of code) can be interleaved with operations at the meta-level, which can manipulate in various ways the context in which this computation takes place. Formally, this is achieved by introducing configurations as basic terms. These are, roughly speaking, pairs consisting of an (open, mutually recursive) collection of named components and a term representing a program running in the context of these components. Configurations can be manipulated by classical module/fragment operators, hence reduction steps can be either execution steps of the program or steps that perform module operations (called reconfiguration steps).

Since configurations combine the features of lambda abstractions (first-class functions), records, environments with mutually recursive definitions and modules, the calculus extends and integrates both traditional module calculi and recursive lambda calculi. We state confluence of the calculus, and propose different ways to prevent errors arising from the lack of some required component, either by a purely static type system or by a combination of static and run-time checks. Moreover, we define a call-by-need strategy that performs module simplification only when needed and only once, leading to a generalisation of call-by-need lambda calculi that includes module features. We prove the soundness and completeness of this strategy using an approach based on information content, which also allows us to preserve confluence, even when local substitution rules are added to the calculus.

This paper reviews recent work related to the interplay between quantum information and computation on the one hand and classical and quantum chaos on the other.

First, we present several models of quantum chaos that can be simulated efficiently on a quantum computer. Then a discussion of information extraction shows that such models can give rise to complete algorithms including measurements that can achieve an increase in speed compared with classical computation. It is also shown that models of classical chaos can be simulated efficiently on a quantum computer, and again information can be extracted efficiently from the final wave function. The total gain can be exponential or polynomial, depending on the model chosen and the observable measured. The simulation of such systems is also economical in the number of qubits, allowing implementation on present-day quantum computers, some of these algorithms having been already experimentally implemented.

The second topic considered concerns the analysis of errors on quantum computers. It is shown that quantum chaos algorithms can be used to explore the effect of errors on quantum algorithms, such as random unitary errors or dissipative errors. Furthermore, the tools of quantum chaos allows a direct analysis of the effects of static errors on quantum computers. Finally, we consider the different resources used by quantum information, and show that quantum chaos has some precise consequences on entanglement generation, which becomes close to maximal. For another resource, interference, a proposal is presented for quantifying it, enabling a discussion on entanglement and interference generation in quantum algorithms.

The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. However, continuous distributions have to be discretized because the corresponding measures cannot be defined on all subsets of their carriers. This paper proposes the use of synthetic topology to model continuous distributions for probabilistic computations in type theory. We study the initial σ-frame and the corresponding induced topology on arbitrary sets. Based on these intrinsic topologies, we define valuations and lower integrals on sets and prove versions of the Riesz and Fubini theorems. We then show how the Lebesgue valuation, and hence continuous distributions, can be constructed.

This paper presents a short survey of some recent approaches relating two different areas, viz. deterministic chaos and computability. Chaos in classical physics may be approached by dynamical (equationally determined) systems or stochastic ones (as random processes). However, randomness has also been effectively modelled using recursion theoretic tools by P. Martin-Löf. We recall its connections to Kolmogorov complexity and show some applications to dynamical systems. This allows us to introduce results that connect well-established notions of entropy and algorithmic information.

In this paper we characterise the equivalential reducts of classical and intuitionistic logics over a language with two propositional variables. We then investigate the size of the fraction of the tautologies of these logics against all formulas. Some methods from complex analysis are used to achieve this goal.

We define BACI(Boxed Ambients with Communication Interfaces), an ambientcalculus with a flexible communication policy. Traditionally, typed ambientcalculi have a fixed communication policy determining the kind of informationthat can be exchanged with a parent ambient, even though mobility changes theparent. BACI lifts that restriction, allowing differentcommunication policies with different parents during computation. Furthermore,BACI separates communication and mobility by making thechannels of communication between ambients explicit. In contrast with othertyped ambient calculi where communication policies are global, each ambient inBACI is equipped with a description of the communicationpolicies ruling its information exchange with parent and child ambients. Thecommunication policies of ambients increase when they move: more precisely, whenan ambient enters another ambient, the entering ambient and the host ambient canexchange their communication ports and agree on the kind of information to beexchanged. This information is recorded locally in both ambients.

We show the type-soundness of BACI, proving that it satisfies thesubject reduction property, and we study its behavioural semantics by means of alabelled transition system.

We present a concept of robust optimisation design for the spring actuator in a 10 kV/12.5 kA vacuum circuit breaker. We assume the breaking and closing velocity characteristics, which are derived form the technical data of the interrupter, as the specifications for the problem, and take the lengths of the connecting rods of the actuator and the stiffness coefficients of the breaking and closing springs as the optimisation variables. The variance between the specifications and the velocities calculated at each breaking and closing point and the maximal variation allowed by the design variables within acceptable tolerances make up the multiple objective function. The optimal parameters for the spring actuator are given by solving a non-linear programming problem with multiple targets and two-level optimisation.

Almost a decade ago, Girard invented linear logic with the notion of a proof-net. Proof-nets are special graphs built from formulas, links and boxes. However, not all nets are proof-nets. First, they must be well constructed (we say that such graphs are proof-structures). Second, a proof-net is a proof-structure that corresponds to a sequential proof. It must satisfy a correctness criterion. One may wonder what this static criterion means for cut-elimination. We prove that every incorrect proof-structure (without cut) can be put in an environment where reductions lead to two kinds of basically wrong configurations: deadlocks and disconnected proof-structures. Thus, this proof says that there does not exist a bigger class of proof-structures than proof-nets where normalization does not lead to obviously bad configurations.

In this paper, we introduce the notion of consistent F-augmented contexts by adding a special family of finite subsets into the structure of a formal context, which essentially establishes the basis of the representation of general algebraic domains. In particular, we investigate the association rule systems which are derived from the consistent F-augmented contexts and propose the notion of formal association rule systems. By the notion of antecedent connections, we obtain the equivalence between the category of formal association rule systems and that of algebraic domains, which demonstrates that the proposed notion of formal association rule systems provides a concrete approach to representing algebraic domains.

Linearity is a multi-faceted and ubiquitous notion in the analysis and development of programming language concepts. We study linearity in a denotational perspective by picking out programs that correspond to linear functions between domains.

We propose a PCF-like language imposing linear constraints on the use of variable to program only linear functions. To entail a full abstraction result, we introduce some higher-order operators related to exception handling and parallel evaluation. We study several notions of operational equivalence and show them to coincide with our language. Finally, we present a new operational evaluation of the language that provides the base for a real implementation. It exploits the denotational linearity to provide an efficient evaluation semantics SECD-like, that avoids the use of closures.

In the theory of sequential programming languages, Berry's stability property is an important step claiming that values have unique origins in their calculations. It has been shown that Bohm trees are stable in the λ-calculus, meaning that there is a unique minimum prefix of any lambda term which computes its Bohm tree. Moreover this property is also true for finite prefixes of Bohm trees. The proof relies on Curry's standardization theorem as initially pointed out by Plotkin in his famous article LCF considered as a programming language. In this paper we will show that the stability property also holds for redexes. Namely for any redex family, there is a unique minimum calculation and a unique redex which computes this family. This property was already known in the study of optimal reductions, but we stress here on stability and want to show that stability is inside the basic objects of calculations. The proof will be based on nice commutations between residuals and creations of new redexes. Our tool for proving this property will be the labelled lambda calculus used in the study of optimal reductions.

Even though the multiplicative–additive fragment of linear logic forbids structural rules in general, is does admit a bounded form of exponential modalities enjoying a bounded form of structural rules. The approximation theorem, originally proved by Girard, states that if full linear logic proves a propositional formula, then the multiplicative–additive fragment proves every bounded approximation of it. This may be understood as the fact that multiplicative–additive linear logic is somehow dense in full linear logic. Our goal is to give a technical formulation of this informal remark. We introduce a Cauchy-complete space of infinitary affine term-proofs and we show that it yields a fully complete model of multiplicative exponential polarised linear logic, in the style of Girard's ludics. Moreover, the subspace of finite term-proofs, which is a model of multiplicative polarised linear logic, is dense in the space of all term-proofs.

We condense the theory of UTxO blockchains down to a simple and compact set of four type equations (Idealised EUTxO), and to an algebraic characterisation (abstract chunk systems), and exhibit an adjoint pair of functors between them. This gives a novel account of the essential mathematical structures underlying blockchain technology, such as Bitcoin.

The study of the sobriety of Scott spaces has got a relatively long history in domain theory. Lawson and Hoffmann independently proved that the Scott space of every continuous directed complete poset (usually called domain) is sober. Johnstone constructed the first directed complete poset whose Scott space is non-sober. Soon after, Isbell gave a complete lattice with a non-sober Scott space. Based on Isbell’s example, Xu, Xi, and Zhao showed that there is even a complete Heyting algebra whose Scott space is non-sober. Achim Jung then asked whether every countable complete lattice has a sober Scott space. The main aim of this paper is to answer Jung’s problem by constructing a countable complete lattice whose Scott space is non-sober. This lattice is then modified to obtain a countable distributive complete lattice with a non-sober Scott space. In addition, we prove that the topology of the product space $\Sigma P\times \Sigma Q$ coincides with the Scott topology of the product poset $P\times Q$ if the set Id(P) and Id(Q) of all incremental ideals of posets P and Q are both countable. Based on this, it is deduced that a directed complete poset P has a sober Scott space, if Id(P) is countable and $\Sigma P$ is coherent and well filtered. In particular, every complete lattice L with Id(L) countable has a sober Scott space.

Web of Linked Data introduces common format and principles for publishing and linking data on the Web. Such a network of linked data is publicly available and easily consumable. This paper introduces a calculus for modelling networks of linked data with encoded privacy preferences.

In that calculus, a network is a parallel composition of users, where each user is named and consists of data, representing the user's profile, and a process. Data is a parallel composition of triples with names (resources) as components. Associated with each name and each triple of names are their privacy protection policies, that are represented by queries. A data triple is accessible to a user if the user's data satisfies the query assigned to that triple.

The main contribution of this model lies in the type system which together with the introduced query order ensures that static type-checking prevents privacy violations. We say that a network is well behaved if

• — access to a triple is more restrictive than access to its components and less restrictive than access to the user name it is enclosed with,

• — each user can completely access their own profile,

• — each user can update or partly delete profiles that they own (can access the whole profiles), and

• — each user can update the privacy preference policy of data of another profile that they own or write data to another profile only if the newly obtained profile stays fully accessible to their owner.

We prove that any well-typed network is well behaved.