The first-order isomorphism problem is to decide whether two non-recursive types using product- and function-type constructors are isomorphic under the axioms of commutative and associative products, and currying and distributivity of functions over products. We show that this problem can be solved in $O(n \log^2 n)$ time and $O(n)$ space, where $n$ is the input size. This result improves upon the $O(n^2 \log n)$ time and $O(n^2)$ space bounds of the best previous algorithm. We also describe an $O(n)$ time algorithm for the linear isomorphism problem, which does not include the distributive axiom, thereby improving upon the $O(n \log n)$ time of the best previous algorithm for this problem.

We model micro-architectures with non-pipelined instruction processing and pipelined instruction processing using Maurer machines, basic thread algebra and program algebra. We show that stored programs are executed as intended with these micro-architectures. We believe that this work provides a new mathematical approach to the modelling of micro-architectures and the verification of their correctness and the anticipated speed-up results.

Circular string matching is a problem which naturally arises in many contexts. It consists in finding all occurrences of the rotations of a pattern of length m in a text of length n. There exist optimal worst- and average-case algorithms for circular string matching. Here, we present a suboptimal average-case algorithm for circular string matching requiring time $\mathcal{O}$(n) and space $\mathcal{O}$(m). The importance of our contribution is underlined by the fact that the proposed algorithm can be easily adapted to deal with circular dictionary matching. In particular, we show how the circular dictionary-matching problem can be solved in average-case time $\mathcal{O}$(n + M) and space $\mathcal{O}$(M), where M is the total length of the dictionary patterns, assuming that the shortest pattern is sufficiently long. Moreover, the presented average-case algorithms and other worst-case approaches were also implemented. Experimental results, using real and synthetic data, demonstrate that the implementation of the presented algorithms can accelerate the computations by more than a factor of two compared to the corresponding implementation of other approaches.

We discuss new ways of characterizing, as maximal fixed points of monotone operators, observational congruences on λ-terms and, more generally, equivalences on applicative structures. These characterizations naturally induce new forms of coinduction principles for reasoning on program equivalences, which are not based on Abramsky's applicative bisimulation. We discuss, in particular, what we call the cartesian coinduction principle, which arises when we exploit the elementary observation that functional behaviours can be expressed as cartesian graphs. Using the paradigm of final semantics, the soundness of this principle over an applicative structure can be expressed easily by saying that the applicative structure can be construed as a strongly extensional coalgebra for the functor ([Pscr ](- × -))[oplus ]([Pscr ](- × -)). In this paper we present two general methods for showing the soundness of this principle. The first applies to approximable applicative structures – many CPO λ-models in the literature and the corresponding quotient models of indexed terms turn out to be approximable applicative structures. The second method is based on Howe's congruence candidates, which applies to many observational equivalences. Structures satisfying cartesian coinduction are precisely those applicative structures that can be modelled using the standard set-theoretic application in non-wellfounded theories of sets, where the Foundation Axiom is replaced by the Axiom X1 of Forti and Honsell.

There are advantages in the use of quantum computing in the elaboration of attacks on certain pseudorandom generators when compared with analogous attacks using classical computing. This paper presents a polynomial time quantum attack on the Blum–Micali generator, which is considered secure against threats from classical computers. The proposed attack uses a Grover inspired procedure together with the quantum discrete logarithm, and is able to recover previous and future outputs of the generator under attack, thereby completely compromising its unpredictability. The attack can also be adapted to other generators, such as Blum–Micali generators with multiple hard-core predicates and generators from the Blum–Micali construction, and also to scenarios where the requirements on the bits are relaxed. Such attacks represent a threat to the security of the pseudorandom generators adopted in many real-world cryptosystems.

We introduce the notion of implicative algebra, a simple algebraic structure intended to factorize the model-theoretic constructions underlying forcing and realizability (both in intuitionistic and classical logic). The salient feature of this structure is that its elements can be seen both as truth values and as (generalized) realizers, thus blurring the frontier between proofs and types. We show that each implicative algebra induces a (Set-based) tripos, using a construction that is reminiscent from the construction of a realizability tripos from a partial combinatory algebra. Relating this construction with the corresponding constructions in forcing and realizability, we conclude that the class of implicative triposes encompasses all forcing triposes (both intuitionistic and classical), all classical realizability triposes (in the sense of Krivine), and all intuitionistic realizability triposes built from partial combinatory algebras.

We present a novel approach to computing the context-sensitive flow of values through procedures and data structures. Our approach combines and extends techniques from two seemingly disparate areas: polymorphic subtyping and interprocedural dataflow analysis based on context-free language reachability. The resulting technique offers several advantages over previous approaches: it works directly on higher-order programs; provides demand-driven interprocedural queries; and improves the asymptotic complexity of a known algorithm based on polymorphic subtyping from O(n8) to O(n3) for computing all queries. For intra-procedural flow restricted to equivalence classes, our algorithm yields linear inter-procedural flow queries.

We survey the main results on computability and totality in Scott–Eršov-domains as well as their applications to the theory of functionals of higher types and the semantics of functional programming languages. A new density theorem is proved and applied to show the equivalence of the hereditarily computable total continuous functionals with the hereditarily effective operations over a large class of base types.

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.

We give an algebraic characterization of the syntax and semantics of a class of untyped functional programming languages.

To this end, we introduce a notion of 2-signature: such a signature specifies not only the terms of a language, but also reduction rules on those terms. To any 2-signature (S, A) we associate a category of ‘models’. We then prove that this category has an initial object, which integrates the terms freely generated by S, and which is equipped with reductions according to the rules given in A. We call this initial object the programming language generated by (S, A). Models of a 2-signature are built from relative monads and modules over such monads. Through the use of monads, the models – and in particular, the initial model – come equipped with a substitution operation that is compatible with reduction in a suitable sense.

The initiality theorem is formalized in the proof assistant Coq, yielding a machinery which, when fed with a 2-signature, provides the associated programming language with reduction relation and certified substitution.

We consider structured specifications built from flat specifications using union, translation and hiding with their standard model-class semantics in the context of an arbitrary institution. We examine the alternative of sound property-oriented semantics for such specifications, and study their relationship to model-class semantics. An exact correspondence between the two (completeness) is not achievable in general. We show through general results on property-oriented semantics that the semantics arising from the standard proof system is the strongest sound and compositional property-oriented semantics in a wide class of such semantics. We also sharpen one of the conditions that does guarantee completeness and show that it is a necessary condition.

The Symmetric Circulant Travelling Salesman Problem asks for the minimum cost tour in a symmetric circulant matrix. The computational complexity of this problem is not known – only upper and lower bounds have been determined. This paper provides a characterisation of the two-stripe case. Instances where the minimum cost of a tour is equal to either the upper or lower bound are recognised. A new construction providing a tour is proposed for the remaining instances, and this leads to a new upper bound that is closer than the previous one.

Motivated by the need to reason about hybrid systems, we study limits in categories of coalgebras whose underlying functor is a Vietoris polynomial one – intuitively, the topological analogue of a Kripke polynomial functor. Among other results, we prove that every Vietoris polynomial functor admits a final coalgebra if it respects certain conditions concerning separation axioms and compactness. When the functor is restricted to some of the categories induced by these conditions, the resulting categories of coalgebras are even complete.

As a practical application, we use these developments in the specification and analysis of non-deterministic hybrid systems, in particular to obtain suitable notions of stability and behaviour.

This paper focuses on the use of linear logic as a specification language for the operational semantics of advanced concepts of programming such as concurrency and object-orientation. Our approach is based on a refinement of linear logic sequent calculi based on the proof-theoretic characterization of logic programming. A well-founded combination of higher-order logic programming and linear logic will be used to give an accurate encoding of the traditional features of concurrent object-oriented programming languages, whose corner-stone is the notion of encapsulation.

It is an open problem whether weak bisimilarity is decidable for Basic Process Algebra (BPA) and Basic Parallel Processes (BPP). A PSPACE lower bound for BPA and NP lower bound for BPP were demonstrated by Stribrna. Mayr recently achieved a result, saying that weak bisimilarity for BPP is $\Pi_2^P$-hard. We improve this lower bound to PSPACE, and, moreover, prove this result for the restricted class of normed BPP. It is also not known whether weak regularity (finiteness) of BPA and BPP is decidable. In the case of BPP there is a $\Pi_2^P$-hardness result by Mayr, which we improve to PSPACE. No lower bound has previously been established for BPA. We demonstrate DP-hardness, which, in particular, implies both NP and co-NP-hardness. In each of the bisimulation/regularity problems we also consider the classes of normed processes. Finally, we show how the technique for proving co-NP lower bound for weak bisimilarity of BPA can be applied to strong bisimilarity of BPP.

In this paper we try to shed some light on the similarities and differences in the different approaches denning the notions of implementation and implementation correctness. For obvious reasons, we do not discuss all existing approaches individually. Instead, a formal framework is introduced in order to discuss the most important ones. Additionally, we discuss some issues, which in our opinion are often misunderstood, concerning transitivity of implementation correctness and its role in the software development process. In particular, on the one hand, we show that for reasonable notions of implementation, it is almost impossible to prove transitivity of implementation correctness at the specification level. On the other hand, we show that this is not really important if the programming language satisfies the properties of horizontal and vertical composition.

The calculus of Mobile Ambients was proposed by Cardelli and Gordon as a foundational calculus for mobile computing. Since its introduction, the computational strength and the decidability of properties have been investigated for several fragments and variants of the standard calculus. We consider the problem of reachability and characterise a public (that is, restriction-free) fragment for which it is decidable. This fragment is obtained by removing the open capability and restricting the application of the replication operator to guarded processes only. This decidability result may appear surprising in combination with the fact that the same fragment was shown to be Turing complete by Maffeis and Phillips. Finally, we extend our decidability result in two ways: we first prove the decidability of a more general property called target reachability (according to which the target of interest for the reachability analysis consists of a possibly infinite set of processes) and then show that our decidability results also hold for a more general calculus, which includes the sophisticated communication mechanisms of Boxed Ambients, which is the most relevant variant of Mobile Ambients without the open capability.

Every compact metric space $X$ is homeomorphically embedded in an $\omega$-algebraic domain $D$ as the set of minimal limit (that is, non-finite) elements. Moreover, $X$ is a retract of the set $L(D)$ of all limit elements of $D$. Such a domain $D$ can be chosen so that it has property M and finite-branching, and the height of $L(D)$ is equal to the small inductive dimension of $X$. We also show that the small inductive dimension of $L(D)$ as a topological space is equal to the height of $L(D)$ for domains with property M. These results give a characterisation of the dimension of a space $X$ as the minimal height of $L(D)$ in which $X$ is embedded as the set of minimal elements. The domain in which we embed an $n$-dimensional compact metric space $X$ ($n \leq \infinity$) has a concrete structure in that it consists of finite/infinite sequences in $\{0,1,\bot\}$ with at most $n$ copies of $\bot$.

Modal and mixed transition systems are specification formalisms that allow the mixing of over- and under-approximation. We discuss three fundamental decision problems for such specifications:

• — whether a set of specifications has a common implementation;

• — whether an individual specification has an implementation; and

• — whether all implementations of an individual specification are implementations of another one.

We show that Friedman's proof of the existence of non-trivial βη-complete models of λ→ can be extended to system F. We isolate a set of conditions that are sufficient to ensure βη-completeness for a model of F (and α-completeness at the level of types), and we discuss which class of models we get. In particular, the model introduced in Barbanera and Berardi (1997), having as polymorphic maps exactly all possible Scott continuous maps, is βη-complete, and is hence the first known complete non-syntactic model of F. In order to have a suitable framework in which to express the conditions and develop the proof, we also introduce the very natural notion of ‘polymax models’ of System F.