ABSTRACT. Kozen's celebrated completeness result introduced Kleene algebra (with tests) as a ubiquitous tool for lightweight reasoning about program equivalence, and yet numerous variants of it have subsequently emerged to answer the demand for more refined flavours of semantics, such as stateful, concurrent, exceptional, hybrid, branching-time. From a high-level perspective, the standard notion of Kleene algebra is not robust under the addition of various programming features, essentially because Kleene algebra axioms often collide with program equivalences of the domain of interest. This raises the question of determining the most basic axiomatisation of Kleene iteration, which could potentially serve as a unified, uncontroversial base for reasoning about non-deterministic iterative behaviour in various settings. I will talk about recent advances, challanges and insights in identifying such a notion.

ABSTRACT. We study the system of classes of superintuitionistic predicate logics induced by the equivalence relation identifying logics with the same positive fragment. We call these classes positive slices. We identify a condition under which logics of classes of Kripke frames and Kripke sheaves have the same positive fragment, and so belong to the same slice, and apply this condition to prove that positive fragments of some well-known logics are identical. We also present an example of a countable family of logics whose slices are singletons.

ABSTRACT. In this paper, we explore a logic of the modality of informative presupposition in the context of propositional intuitionistic inquisitive logic. This modality allows us to reduce a given question to its informative content, i.e., a declarative statement that expresses the presupposition of the corresponding question. We present a natural deduction calculus for this logic (i.e., intuitionistic logic + split rule + introduction and elimination rules for the new modality) and show that it is sound and strongly complete with respect to a Kripke semantics based on inquisitive Kripke models and an algebraic semantics based on the notion of inquisitive nucleus. We argue that our setting allows us to shed some light on the relation between different approaches to intuitionistic inquisitive logic, namely, the approach developed by Wesley Holliday, on one side, and approaches based on the tensor disjunction, on the other side. Furthermore, we assess the connections of the presupposition modality to other related notions such as lax modality and truncation modality.

ABSTRACT. We present a cyclic sequent calculus for intuitionistic modal logic with the master modality. Formulas of the logic are evaluated over bi-relational Kripke models with three different frame conditions: functional frames, `triangle' confluent frames, and arbitrary frames. It is shown that the calculus is sound and complete for all three classes of models. This, in particular, proves that intuitionistic modal logic with the master modality cannot distinguish between arbitrary models and functional models. Soundness is established by a standard argument while completeness is proven via a detour to non-wellfounded proofs, using a proof-search argument that draws on analyticity of the calculus. The framework is robust in the sense that it can be naturally adapted to account for various frame conditions, such as serial models, reflexive models or S4-models, as well as for a polymodal extension that can be interpreted as intuitionistic common knowledge logic.

ABSTRACT. Non-wellfounded proof theory results from allowing proofs of infinite height in proof theory. To guarantee that there is no vicious infinite reasoning, it is usual to add a constraint to the possible infinite paths appearing in a proof. Among these conditions, one of the simplest is enforcing that any infinite path goes through the premise of a rule infinitely often. Systems of this kind appear for modal logics with conversely well-founded frame conditions like GL or Grz.

In this paper, we provide a uniform method to define proof translations for such systems, guaranteeing that the condition on infinite paths is preserved. In addition, as particular instances of our method, we establish cut-elimination for non-wellfounded systems of the logics Grz and wGrz. Our proof relies only on the categorical definition of corecursion via coalgebras, while an earlier proof by Savateev and Shamkanov uses ultrametric spaces and a corresponding fixed point theorem.

ABSTRACT. The concurrent refinement algebra has been developed to support rely/\-guarantee reasoning about concurrent programs. The algebra supports atomic commands and defines parallel composition as a synchronous operation, as in Milner's SCCS. In order to allow specifications to be combined, the algebra also provides a weak conjunction operation, which is also a synchronous operation that shares many properties with parallel composition. The three main operations, sequential composition, parallel composition and weak conjunction, all respect a (weak) quantale structure over a lattice of commands.Further structure involves combinations of pairs of these operations: sequential/parallel, sequential/weak conjunction and parallel/weak conjunction, each pair satisfying a weak interchange law similar to Concurrent Kleene Algebra. Each of these pairs satisfies a common biquantale structure. Additional structure is incorporated in the form of compatible sets of commands, including tests and atomic commands.These facilitate stronger (equality) interchange and distributive laws.This paper describes the result of restructuring the algebra to better exploit these commonalities. The algebra is implemented in Isabelle/HOL.

ABSTRACT. Higher-dimensional automata (HDA) are a formalism to faithfully model the behaviour ofconcurrent systems.For ordinary automata, there is a correspondence between regular expressions, regular languages andfinite automata, which provides a powerful link between algebraic proofs and operational behaviour.It has been shown by Fahrenberg~et~al. that finite HDA correspond with interfaced interval pomsetlanguages generated by sequential and parallel composition and non-empty iteration, and thereby toa variant of Kleene algebras (KA) with parallel composition.It is known that this correspondence cannot be extended to concurrent KA, whichadditionally have process replication.An alternative to finite HDA are locally compact HDA, in which every state reaches only finitely many other states, and finitely branching HDA.In this paper, we show that both classes of HDA are closed under process replication and thus models of concurrent KA.To achieve this, we prove that the category of HDA is locally finitely presentable, where the finite HDA generate all other HDA. We then prove that this has the unfortunate side-effect that all HDA are locally compact, which means that the correspondence with concurrent KA trivialises.Similarly, we show that, even though finitely branching HDA are closed under process replication, the resulting HDA necessarily have infinitely many initial states.

ABSTRACT. We show that the equational theory is undecidable and ∏₀1-complete for the positive calculus of relations with transitive closure and the difference constant. Furthermore, we show that the emptiness (unsatisfiability) problem is also  ∏₀1--complete for propositional while- programs with graph loops on functional structures. To this end, we give a hypothesis elimination using graph loops. Using this, we give reductions from the periodic domino problem.