Abstract
A Community of Practice (CoP) allows practitioners of a clearly defined domain to share knowledge, experience, and best practices. It provides a social context for practitioners, often distributed across multiple organizations, and emerged over the last few decades as a fundamental mechanism for knowledge sharing, management, and generation within organizations. Best practices, innovations, and solutions to shared problems first emerge within CoPs. These are, and must be perceived as, an investment in organizations' future and competitiveness. Establishing a CoP is a straightforward process, the most challenging factor being the recruitment of members to attain critical mass. The challenge is to maintain the CoP active, with members contributing with high quality, innovative content. Increasing a CoP's medium / long-term survival probabilities requires careful planning to avoid incurring in some well-known pitfalls. This paper proposes and discusses a set of nine guidelines for establishing and maintaining a community of practice within the context of Electronic Governance (EGOV) and Government Chief Information Officers (GCIO). This research was motivated by the initiative of the government of a developing country. Results are based on a review of the relevant literature, together with the detailed analysis of interviews to members or coordinators of large communities of practice. This analysis was further validated against the opinions of public servants directly involved on EGOV-GCIO-related functions during two focus groups meetings. © 2018 Association for Computing Machinery.

Abstract
The structure of a reactive transition system can to be modified on the fly by e.g. removing, reversing or adding new transitions. The topic has been studied by D. Gabbay and his collaborators in different contexts. In this paper we take their work a step further, introducing a suitable notion of bisimulation and obtaining a Hennessy-Milner theorem with respect to a hybrid logic in which transition properties can be expressed. Our motivation is to provide a characterisation of equivalence for such systems in order to exploit their possible roles in the formal description of software connectors in Reo, either from a behavioural (semantic) or spatial (syntactic) point of view.

Abstract
Quantum algorithmics is emerging as a hot area of research, with the potential to have groundbreaking impacts on many different fields. The benefits come at a high price, however: quantum programming is hard and finding new quantum algorithms is far from straightforward. This area of research may greatly benefit from mathematical foundations and calculi, capable of supporting algorithm development and analysis. The Quantum Algorithmics Agenda at QuantaLab is contributing by seeking a suitable semantics-calculus-logic trilogy for quantum computation.

Abstract
We introduce HHL, a hierarchical variant of hybrid logic. We study first order correspondence results and prove a Hennessy-Milner like theorem relating (hierarchical) bisimulation and modal equivalence for HHL. Combining hierarchical transition structures with the ability to refer to specific states at different levels, this logic seems suitable to express and verify properties of hierarchical transition systems, a pervasive semantic structure in Computer Science.

Abstract
A reactive model, as studied by D. Gabbay and his collaborators, can be regarded as a graph whose set of edges may be altered whenever one of them is crossed. In this paper we show how reactive models can describe biological regulatory networks and compare them to Boolean networks and piecewise-linear models, which are some of the most common kinds of models used nowadays. In particular, we show that, with respect to the identification of steady states, reactive Boolean networks lie between piecewise linear models and the usual, plain Boolean networks. We also show this ability is preserved by a suitable notion of bisimulation, and, therefore, by network minimisation. © 2019, Springer Nature Switzerland AG.

Abstract
This paper gives a comprehensive and coherent view on permutability in the intuitionistic sequent calculus with cuts. Specifically we show that, once permutability is packaged into appropriate global reduction procedures, it organizes the internal structure of the system and determines fragments with computational interest, both for the computation-as-proof-normalization and the computation-as-proof-search paradigms. The vehicle of the study is a ?-calculus of multiary proof terms with generalized application, previously developed by the authors (the paper argues this system represents the simplest fragment of ordinary sequent calculus that does not fall into mere natural deduction). We start by adapting to our setting the concept of normal proof, developed by Mints, Dyckhoff, and Pinto, and by defining natural proofs, so that a proof is normal iff it is natural and cut-free. Natural proofs form a subsystem with a transparent Curry- Howard interpretation (a kind of formal vector notation for -terms with vectors consisting of lists of lists of arguments), while searching for normal proofs corresponds to a slight relaxation of focusing (in the sense of LJT). Next, we define a process of permutative conversion to natural form, and show that its combination with cut elimination gives a concept of normalization for the sequent calculus. We derive a systematic picture of the full system comprehending a rich set of reduction procedures (cut elimination, flattening, permutative conversion, normalization, focalization), organizing the relevant subsystems and the important subclasses of cut-free, normal, and focused proofs. © José Espírito Santo, Maria João Frade, and Luís Pinto; licensed under Creative Commons License CC-BY 22nd International Conference on Types for Proofs and Programs (TYPES 2016).