Structural operational semantics (SOS) is one of the most common formalisms for specifying language semantics. There has been much interest in automatically deriving small-step SOS definitions from big-step definitions and vice versa, as well as towards extrapolating language implementations from these inductive, declarative definitions. This work presents Computation-Tree Semantics (CTS) in which semantic configurations are tree-structured, unlike standard SOS-configurations which are “flat”. This tree-structure is key in making our approach algorithmic, meaning it is able to describe how a transition is produced, contrary to the traditional declarative approach taken by SOS. We show how one can -- in a straight-forward manner -- obtain a CTS from the big-step semantics of a simple arithmetic language, a simple while language, and the call-by-need lambda-calculus as given by Launchbury. From the resulting CTS, we then obtain a small-step understanding of all these languages. The arithmetic language example is formalised in Coq/Rocq.

Editor calculi make it possible to describe the actions of syntax-directed editing and provide guarantees of safety through their specialized type system: Well-typed editor scripts produce well-formed programs. So far, such calculi have been language-specific. In this paper we present a generalized editor calculus, which can be used to specify a specialized syntax-directed editor for any language, given its abstract syntax. Moreover we show how to implement an editor generator that allows one to generate an editor calculus-based syntax-directed editor from a language specification. The generalized editor calculus can be encoded into a simply typed lambda calculus, extended with pairs, booleans, pattern matching and fixed points. This implies a general type safety result that holds for any instantiation.

The Higher-Order Ψ-calculus framework (HOΨ) by Parrow et al. is a generalisation of many first- and higher-order extensions of the π-calculus. In this paper we present a generic type system for HOΨ-calculi. It satisfies a subject reduction property and can be instantiated to yield both existing and new type systems for calculi, that can be expressed as HOΨ-calculi. In this paper, we consider the type system for termination in HOπ by Demangeon et al. Moreover, we derive a new type system for the ρ-calculus of Meredith and Radestock and present a type system for non-interference for mobile code.

Mungo is an object-oriented language that uses typestates with a behavioural type system to ensure the absence of null-dereferencing. Typestates are usages that specify the admissible sequences of method calls on objects. Previous type systems for Mungo have all had a linearity constraint on objects. We present an extension of these systems, where usage specifications can now include a parallel construct that lets us describe separate local behaviour. A parallel usage describes a separation of the heap, and this allows us to reason about aliasing and to express arbitrary interleaving of local protocols. This also solves the state-space explosion problem for usages. Our extension retains the safety properties of previous type systems for Mungo.

The Lightning Network is a second layer protocol that sits on top of the Bitcoin cryptocurrency. It is a decentralized network of payment channels first conceptualized in 2014 and its first implementation was released in 2017. Being a fairly new technology, it may have security issues that we do not know of and the goal of this report is to analyse the Lightning Network to further investigate its security properties. The focus of this analysis is on answering whether the confidential data is kept secret and whether the user authenticity holds in the protocol. In the analysis we use the process algebra to formally describe cryptographic protocols that form the Lightning Network and an automatic cryptographic protocol analyser called ProVerif for their analysis.

Baeten, Bergstra, and Klop (and later Caucal) have proved the remarkable result that bisimulation equivalence is decidable for irredundant context-free grammars. In this paper we provide a much simpler and much more direct proof of this result using a tableau decision method involving goal-directed rules. The decision procedure also provides the essential part of the bisimulation relation between two processes which underlies their equivalence. We also show how to obtain a sound and complete sequent-based equational theory for such processes from the tableau system and how one can extract what Caucal calls a fundamental relation from a successful tableau.

J.C.M. Baeten et al. (Lecture Notes in Computer Science, vol. 259, pp. 93-114, 1987) proved that bisimulation equivalence is decidable for irredundant context-free grammars. A much simpler and much more direct proof of this result is provided now. It uses a tableau decision method involving goal-directed rules. The decision procedure yields an upper bound on a tableau depth. Moreover, it provides the essential part of the bisimulation relation between two processes which underlies their equivalence. A second virtue is that it provides a sound and complete equational theory for such processes.>