Open bisimilarity is defined for open process terms in which free variables may appear. The insight is, in order to characterise open bisimilarity, we move to the setting of intuitionistic modal logics. The intuitionistic modal logic introduced, called $\mathcal{OM}$, is such that modalities are closed under substitutions, which induces a property known as intuitionistic hereditary. Intuitionistic hereditary reflects in logic the lazy instantiation of free variables performed when checking open bisimilarity. The soundness proof for open bisimilarity with respect to our intuitionistic modal logic is mechanised in Abella. The constructive content of the completeness proof provides an algorithm for generating distinguishing formulae, which we have implemented. We draw attention to the fact that there is a spectrum of bisimilarity congruences that can be characterised by intuitionistic modal logics.

Quasi-open bisimilarity is the coarsest notion of bisimilarity for the π-calculus that is also a congruence. This work extends quasi-open bisimilarity to handle mismatch (guards with inequalities). This minimal extension of quasi-open bisimilarity allows fresh names to be manufactured to provide constructive evidence that an inequality holds. The extension of quasi-open bisimilarity is canonical and robust --- coinciding with open barbed bisimilarity (an objective notion of bisimilarity congruence) and characterised by an intuitionistic variant of an established modal logic. The more famous open bisimilarity is also considered, for which the coarsest extension for handling mismatch is identified. Applications to checking privacy properties are highlighted. Examples and soundness results are mechanised using the proof assistant Abella.

The Mendler style catamorphism (which corresponds to weak induction) always terminates even for negative inductive datatypes. The Mendler style histomorphism (which corresponds to strong induction) is known to terminate for positive inductive datatypes. To our knowledge, the literature is silent on its termination properties for negative datatypes. In this paper, we prove that histomorphisms do not always termintate by showing a counter-example. We also enrich the Mendler collection of recursion combinators by defining a new form of Mendler style catamorphism (msfcata), which terminates for all inductive datatypes, that is more expressive than the original. We organize the collection of combinators by placing them into a hierarchy of ever increasing generality, and describing the termination properties of each point on the hierarchy. We also provide many examples (including a case study on a negative inductive datatype), which illustrate both the expressive power and beauty of the Mendler style. One lesson we learn from this work is that weak induction applies to negative inductive datatypes but strong induction is problematic. We provide a proof of weak induction by exhibiting an embedding of our new combinator into Fω. We pose the open question: Is there a safe way to apply strong induction to negative inductive datatypes?

A newtype declaration in Haskell introduces a new type renaming an existing type. The two types are viewed by the programmer as semantically different, but share the same runtime representation. When operations on the two semantic views coincide, the run-time cost of conversion between the two types is reduced to zero (in both directions) because of this common representation.