A reactive system can be specified by a labelled transition system, which indicates static structure, along with temporal-logic formulas, which assert dynamic behaviour. But refining the former while preserving the latter can be difficult, because:

(i) Labelled transition systems are ‘total’ – characterised up to bisimulation – meaning that no new transition structure can appear in a refinement.

(ii) Alternatively, a refinement criterion not based on bisimulation might generate a refined transition system that violates the temporal properties.

In response, Larsen and Thomson proposed modal transition systems, which are ‘partial’, and defined a refinement criterion that preserved formulas in Hennessy–Milner logic. We show that modal transition systems are, up to a saturation condition, exactly the mixed transition systems of Dams that meet a mix condition, and we extend such systems to non-flat state sets. We then solve a domain equation over the mixed powerdomain whose solution is a bifinite domain that is universal for all saturated modal transition systems and is itself fully abstract when considered as a modal transition system. We demonstrate that many frameworks of partial systems can be translated into the domain: partial Kripke structures, partial bisimulation structures, Kripke modal transition systems, and pointer-shape-analysis graphs.

A formulation of lattice theory as a system of rules added to sequent calculus is given. The analysis of proofs for the contraction-free calculus of classical predicate logic known as G3c extends to derivations with the mathematical rules of lattice theory. It is shown that minimal derivations of quantifier-free sequents enjoy a subterm property: all terms in such derivations are terms in the endsequent.

An alternative formulation of lattice theory as a system of rules in natural deduction style is given, both with explicit meet and join constructions and as a relational theory with existence axioms. A subterm property for the latter extends the standard decidable classes of quantificational formulas of pure predicate calculus to lattice theory.

We propose the design of a programming language for quantum computing. Traditionally, quantum algorithms are frequently expressed at the hardware level, for instance in terms of the quantum circuit model or quantum Turing machines. These approaches do not encourage structured programming or abstractions such as data types. In this paper, we describe the syntax and semantics of a simple quantum programming language with high-level features such as loops, recursive procedures, and structured data types. The language is functional in nature, statically typed, free of run-time errors, and has an interesting denotational semantics in terms of complete partial orders of superoperators.

A purely syntactic and untyped variant of Normalisation by Evaluation for the $\lambda$-calculus is presented in the framework of a two-level $\lambda$-calculus with rewrite rules to model the inverse of the evaluation functional. Among its operational properties there is a standardisation theorem that formally establishes the adequacy of implementation in functional programming languages. An example implementation in Haskell is provided. The relation to the usual type-directed Normalisation by Evaluation is highlighted, using a short analysis of $\eta$-expansion that leads to a perspicuous strong normalisation and confluence proof for $\beta\eta\!\up$-reduction as a byproduct.