Yao et al. (A note on the feasibility of generalized universal composability. Theory and Applications of Models of Computation pp. 474–485, 2007; A note on the feasibility of generalised universal composability. Mathematical Structures in Computer Science, 19 (1), pp. 193–205) claimed a potential limitation on the class of protocols that could be securely implemented in the generalized universal composability (GUC) framework proposed by Canetti et al. (Universally composable security with global setup. Lecture Notes in Computer Science, pp. 61–85, 2007). Specifically, Yao et al. presented a concrete attack on a GUC Zero Knowledge (GUCZK) protocol, a natural adaptation Blum's ZK proof for Directed Hamiltonicity using the general GUC feasibility of Canetti et al. (Universally composable security with global setup. Lecture Notes in Computer Science, pp. 61–85, 2007). Interestingly, the attack was not analysed in the GUC model in Yao et al. (A note on the feasibility of generalised universal composability. Mathematical Structures in Computer Science19 (1), pp. 193–205, 2009) but in the FUC model, a new UC-like framework proposed in the same work. Nonetheless, Yao et al. (A note on the feasibility of generalised universal composability. Mathematical Structures in Computer Science19 (1), pp. 193–205, 2009) argued that, in light of this attack, GUC would lose its concurrent general composability and proof of knowledge properties. Concretely, they argue that GUC composability would now be with respect to some adversaries with limited access to external arbitrary protocols.

In this work, we show that the claimed attack from Yao et al. is indeed harmless and does not contradict the security of the mentioned GUCZK protocol, thus restoring the general feasibility for GUC.

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 investigate the expressiveness of two classical distributed paradigms by defining the first encoding of the pure mobile ambient calculus into the synchronous π-calculus. Our encoding, whose correctness has been proved by relying on the notion of operational correspondence, shows how the hierarchical ambient structure can be reformulated within a flat channel interconnection amongst independent processes, without centralised control. To easily handle the computation for simulating a capability, we introduce the notions of simulating trace (representing the computation that a π-calculus process has to execute to mimic a capability) and of aborting trace (representing the computation that a π-calculus process executes when the simulation of a capability cannot succeed). Thus, the encoding may introduce loops, but, as it will be shown, the number of steps of any trace, therefore of any aborting trace, is limited, and the number of states of the transition system of the encoding processes still remains finite. In particular, an aborting trace makes a sort of backtracking, leaving the involved sub-processes in the same starting configurations. We also discuss two run-time support methods to make these loops harmless at execution time. Our work defines a relatively simple, direct, and precise translation that reproduces the ambient structure by means of channel links, and keeps track of the dissolving of an ambient.

The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer, which can be regarded as an algebraic formulation of type theory. We determine conditions for such models to satisfy the inference rules for dependent sums Σ, dependent products Π and intensional identity types Id, as used in homotopy type theory. It is then shown that a category admits such a model if it has a class of maps that behave like the abstract fibrations in axiomatic homotopy theory: They should be stable under pullback, closed under composition and relative products, and there should be weakly orthogonal factorizations into the class. It follows that many familiar settings for homotopy theory also admit natural models of the basic system of homotopy type theory.

The aim of this paper is to provide mathematical foundations of a graph transformation language, called UnCAL, using categorical semantics of type theory and fixed points. About 20 years ago, Buneman et al. developed a graph database query language UnQL on the top of a functional meta-language UnCAL for describing and manipulating graphs. Recently, the functional programming community has shown renewed interest in UnCAL, because it provides an efficient graph transformation language which is useful for various applications, such as bidirectional computation.

In order to make UnCAL more flexible and fruitful for further extensions and applications, in this paper, we give a more conceptual understanding of UnCAL using categorical semantics. Our general interest of this paper is to clarify what is the algebra of UnCAL. Thus, we give an equational axiomatisation and categorical semantics of UnCAL, both of which are new. We show that the axiomatisation is complete for the original bisimulation semantics of UnCAL. Moreover, we provide a clean characterisation of the computation mechanism of UnCAL called ‘structural recursion on graphs’ using our categorical semantics. We show a concrete model of UnCAL given by the λG-calculus, which shows an interesting connection to lazy functional programming.