We were all taught in high school that two objects $A$ and $B$ are isomorphic iff there exist two functions $f$ and $g$ such that

This paper studies modified bar recursion, a higher type recursion scheme, which has been used in Berardi et al. (1998) and Berger and Oliva (2005) for a realisability interpretation of classical analysis. A complete clarification of its relation to Spector's and Kohlenbach's bar recursion, the fan functional, Gandy's functional $\Gamma$ and Kleene's notion of S1–S9 computability is given.

Craig Squier proved that, if a monoid can be presented by a finite convergent string rewriting system, then it satisfies the homological finiteness condition left-FP3. Using this result, he constructed finitely presentable monoids with a decidable word problem, but that cannot be presented by finite convergent rewriting systems. Later, he introduced the condition of finite derivation type, which is a homotopical finiteness property on the presentation complex associated to a monoid presentation. He showed that this condition is an invariant of finite presentations and he gave a constructive way to prove this finiteness property based on the computation of the critical branchings: Being of finite derivation type is a necessary condition for a finitely presented monoid to admit a finite convergent presentation. This survey presents Squier's results in the contemporary language of polygraphs and higher dimensional categories, with new proofs and relations between them.

We combine the principles of the Floyd-Warshall-Kleene algorithm, enriched categories, and Birkhoff arithmetic, to yield a useful class of algebras of transitive vertex-labeled spaces. The motivating application is a uniform theory of abstract or parametrized time in which to any given notion of time there corresponds an algebra of concurrent behaviors and their operations, always the same operations but interpreted automatically and appropriately for that notion of time. An interesting side application is a language for succinctly naming a wide range of datatypes.

We show how to solve the word problem for simply typed λβη-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for these results is [Pscr ]-category theory, a version of ordinary category theory where each hom-set is equipped with a partial equivalence relation. The part of [Pscr ]-category theory we develop here is constructive and thus permits extraction of programs from proofs. It is important to stress that in our method we make no use of traditional proof-theoretic or rewriting techniques. To show the robustness of our method, we give an extended treatment for more general λ-theories in the Appendix.

We propose a design and verification methodology supporting the early phases of system design for cooperative driver assistance systems, focusing on the realisability of new automotive functions. Specifically, we focus on applications where drivers are supported in complex driving tasks by safe strategies involving the coordinated movements of multiple vehicles to complete the driving task successfully. We propose a divide and conquer approach for formally verifying timed probabilistic requirements on successful completion of the driving task and collision freedom based on formal specifications of a set of given manoeuvring and communication capabilities of the car. In particular, this allows an assessment of whether they are sufficient to implement strategies for successful completion of the driving task.

A ‘hybridization’ of a logic, referred to as the base logic, consists of developing the characteristic features of hybrid logic on top of the respective base logic, both at the level of syntax (i.e. modalities, nominals, etc.) and of the semantics (i.e. possible worlds). By ‘hybridized institutions’ we mean the result of this process when logics are treated abstractly as institutions (in the sense of the institution theory of Goguen and Burstall). This work develops encodings of hybridized institutions into (many-sorted) first-order logic (abbreviated $\mathcal{FOL}$) as a ‘hybridization’ process of abstract encodings of institutions into $\mathcal{FOL}$, which may be seen as an abstraction of the well-known standard translation of modal logic into $\mathcal{FOL}$. The concept of encoding employed by our work is that of comorphism from institution theory, which is a rather comprehensive concept of encoding as it features encodings both of the syntax and of the semantics of logics/institutions. Moreover, we consider the so-called theoroidal version of comorphisms that encode signatures to theories, a feature that accommodates a wide range of concrete applications. Our theory is also general enough to accommodate various constraints on the possible worlds semantics as well a wide variety of quantifications. We also provide pragmatic sufficient conditions for the conservativity of the encodings to be preserved through the hybridization process, which provides the possibility to shift a formal verification process from the hybridized institution to $\mathcal{FOL}$.

Several mathematical ideas have been investigated for quantitative information flow. Information theory, probability, guessability are the main ideas in most proposals. They aim to quantify how much information is leaked, how likely is to guess the secret and how long does it take to guess the secret respectively. In this work, we investigate the relationship between these ideas in the context of the quantitative analysis of deterministic systems. We propose the lattice of information as a valuable foundation for these approaches; not only it provides an elegant algebraic framework for the ideas, but also to investigate their relationship. In particular, we will use this lattice to prove some results establishing order relation correspondences between the different quantitative approaches. The implications of these results w.r.t. recent work in the community is also investigated. While this work concentrates on the foundational importance of the lattice of information its practical relevance has been recently proven, notably with the quantitative analysis of Linux kernel vulnerabilities. Overall, we believe these works set the case for establishing the lattice of information as one of the main reference structure for quantitative information flow.

We propose a new category-theoretic formulation of relational parametricity based on a logic for reasoning about parametricity given by Abadi and Plotkin. The logic can be used to reason about parametric models, such that we may prove consequences of parametricity that to our knowledge have not been proved before for existing category-theoretic notions of relational parametricity. We provide examples of parametric models and describe a way of constructing parametric models from given models of the second-order lambda calculus.

This paper extends the ‘lens’ concept for view updating in Computer Science beyond the categories of sets and ordered sets. It is first shown that a constant complement view updating strategy also corresponds to a lens for a categorical database model. A variation on the lens concept called a c-lens is introduced, and shown to correspond to the categorical notion of Grothendieck opfibration. This variant guarantees a universal solution to the view update problem for functorial update processes.

We show that the Borel hierarchy of the class of context free $\omega$-languages, or even of the class of $\omega$-languages accepted by Büchi 1-counter automata, is the same as the Borel hierarchy of the class of $\omega$-languages accepted by Turing machines with a Büchi acceptance condition. In particular, for each recursive non-null ordinal $\alpha$, there exist some ${\bf \Sigma}^0_\alpha$-complete and some ${\bf \Pi}^0_\alpha$-complete $\omega$-languages accepted by Büchi 1-counter automata. And the supremum of the set of Borel ranks of context free $\omega$-languages is an ordinal $\gamma_2^1$ that is strictly greater than the first non-recursive ordinal $\omega_1^{\mathrm{CK}}$. We then extend this result, proving that the Wadge hierarchy of context free $\omega$-languages, or even of $\omega$-languages accepted by Büchi 1-counter automata, is the same as the Wadge hierarchy of $\omega$-languages accepted by Turing machines with a Büchi or a Muller acceptance condition.

We define weak inclusion systems as a natural extension of inclusion systems. We prove that several properties of factorisation systems and inclusion systems remain valid under this extension and we obtain new properties as algebraic tools in abstract model theory.

Milner's action calculus implements abstraction in monoidal categories, so that familiar λ-calculi can be subsumed together with the π-calculus and the Petri nets. Variables are generalised to names, which allow only a restricted form of substitution.

In the present paper, the well-known categorical semantics of the λ-calculus is generalised to the action calculus. A suitable functional completeness theorem for symmetric monoidal categories is proved: we determine the conditions under which the abstraction is definable. Algebraically, the distinction between the variables and the names boils down to the distinction between the transcendental and the algebraic elements. The former lead to polynomial extensions, like, for example, the ring ℤ[x]; the latter lead to algebraic extensions like ℤ[√2] or ℤ[i].

Building upon the work of P. Gardner, we introduce action categories, and show that they are related to the static action calculus in exactly the same way as cartesian closed categories are related to the λ-calculus. Natural examples of this structure arise from allegories and cartesian bicategories. On the other hand, the free algebras for any commutative Moggi monad form an action category. The general correspondence of action calculi and Moggi monads will be worked out in a sequel to this work.

A concept of equation morphism is introduced for every endofuctor $F$ of a cocomplete category $\Ce$. Equationally defined classes of $F$-algebras for which free algebras exist are called varieties. Every variety is proved to be monadic over $\Ce$, and, conversely, every monadic category is equivalent to a variety. The Birkhoff Variety Theorem is also proved for $`{\sf Set}\hbox{-like}'$ categories.

By dualising, we arrive at a concept of coequation such that covarieties, that is, coequationally specified classes of coalgebras with cofree objects, correspond precisely to comonadic categories. Natural examples of covarieties are presented.

We present a formalism of trees with pointers, called abstract Böhm trees, that provide a suitable abstract framework in which various cut-free proofs or normal terms of several λ-calculus based languages (including PCF and Parigot's λμ-calculus) can be faithfully encoded. A simple abstract machine called the View Abstract Machine (VAM) allows us to compute over abstract Böhm trees. The VAM is closely related to Coquand's interaction sequences and debates. The VAM execution over finite abstract Böhm trees always terminates. We next introduce an abstract notion of type that fits the purpose of guaranteeing that the VAM cannot go into deadlock, i.e., that it always reaches a satisfactory final state. Typed abstract Böhm trees can be turned into a category – more naturally a ‘multi-category’ where the domains of arrows are sets of named objects or records. We then go from the abstract to the concrete by giving examples. Our sets of abstract (typed) Böhm trees are relative to an alphabet and a set of types. By instantiating these two parameter sets appropriately, we recover, successively: (η-long) typed Böhm trees; PCF trees as considered in the game models of Hyland–Ong or of Abramsky–Jagadeesan–Malacaria; a notion of classical Böhm tree due to Herbelin that provides a classical version of PCF trees in the style of λμ-calculus; and, finally, cut-free proofs in Novikov's infinitary propositional logic as investigated by Coquand. In a companion paper, we investigate the operational aspects of (untyped) Böhm trees in more depth.

We introduce a natural deduction-like formalisation of Parigot's λμ-calculus. From this, we derive an environment machine that allows any well-typed λμ-term to be reduced to its weak head normal form. The soundness and completeness of the machine is proved.

We introduce a new class of higher order rewriting systems, called Interaction Systems (IS's). IS's are derived from Lafont's (Intuitionistic) Interaction Nets (Lafont 1990) by dropping the linearity constraint. In particular, we borrow from Interaction Nets the syntactical bipartitions of operators into constructors and destructors and the principle of binary interaction. As a consequence, IS's are a subclass of Klop's Combinatory Reduction Systems (Klop 1980), where the Curry-Howard analogy still ‘makes sense’. Destructors and constructors, respectively, correspond to left and right logical introduction rules: interaction is cut and reduction is cut-elimination.

Interaction Systems have been primarily motivated by the necessity of extending the practice of optimal evaluators for λ-calculus (Lamping 1990; Gonthier et al. 1992a) to other computational constructs such as conditionals and recursion. In this paper we focus on the theoretical aspects of optimal reductions. In particular, we generalize the family relation in Lévy (1978; 1980), thus defining the amount of sharing an optimal evaluator is required to perform. We reinforce our notion of family by approaching it in two different ways (generalizing labelling and extraction in Levy (1980)) and proving their coincidence. The reader is referred to Asperti and Laneve (1993c) for the paradigmatic description of optimal evaluators of IS's.

In this paper we propose a quantum random number generator (QRNG) that uses an entangled photon pair in a Bell singlet state and is certified explicitly by value indefiniteness. While ‘true randomness’ is a mathematical impossibility, the certification by value indefiniteness ensures that the quantum random bits are incomputable in the strongest sense. This is the first QRNG setup in which a physical principle (Kochen–Specker value indefiniteness) guarantees that no single quantum bit that is produced can be classically computed (reproduced and validated), which is the mathematical form of bitwise physical unpredictability.

We discuss the effects of various experimental imperfections in detail: in particular, those related to detector efficiencies, context alignment and temporal correlations between bits. The analysis is very relevant for the construction of any QRNG based on beam-splitters. By measuring the two entangled photons in maximally misaligned contexts and using the fact that two bitstrings, rather than just one, are obtained, more efficient and robust unbiasing techniques can be applied. We propose a robust and efficient procedure based on XORing the bitstrings together – essentially using one as a one-time-pad for the other – to extract random bits in the presence of experimental imperfections, as well as a more efficient modification of the von Neumann procedure for the same task. We also discuss some open problems.

In his 1903, Principles of Mathematics, Bertrand Russell mentioned possible definitions of conjunction, disjunction, negation and existential quantification in terms of implication and universal quantification, exploiting impredicative universal quantifiers over all propositions. In his 1965 Ph.D. thesis Dag Prawitz showed that these definitions hold in intuitionistic second order logic. More recently, these definitions have been used to represent logic in various impredicative type theories. This treatment of logic is distinct from the more standard Curry–Howard representation of logic in a dependent type theory.

The main aim of this paper is to compare, in a purely logical, non type-theoretic setting, this Russell–Prawitz representation of intuitionistic logic with other possible representations. It turns out that associated with the Russell–Prawitz representation is a lax modal operator, which we call the Russell–Prawitz modality, and that any lax modal operator can be used to give a translation of intuitionistic logic into itself that generalises both the double negation interpretation, double negation being a paradigm example of a lax modality, and the Russell–Prawitz representation.

Inspired by a question of Riecke, we consider the interaction of totality and full abstraction, asking whether full abstraction holds for Scott's model of cpos and continuous functions if one restricts to total programs and total observations. The answer is negative, as there are distinct operational and denotational notions of totality. However, when two terms are each total in both senses, they are totally equivalent operationally iff they are totally equivalent in the Scott model. Analysing further, we consider sequential and parallel versions of PCF and several models: Scott's model of continuous functions, Milner's fully abstract model of PCF and their effective submodels. We investigate how totality differs between these models. Some apparently rather difficult open problems arise that essentially concern whether the sequential and parallel versions of PCF have the same expressive power, in the sense of total equivalence.