Display calculi and nominal string diagrams

This thesis is divided into two sections, encompassing two main topics: display calculi and nominal string diagrams. In the first section of the thesis, we introduce display calculi and present their advantages and drawbacks compared to sequent calculi. The rest of the section presents the calculus toolbox, a meta-tool for formalising display calculi. The tool includes a tree editor and a type-checker, which aid the user in exploring display calculi more efficiently. Section two grew out of an attempt to build a calculus of simultaneous substitutions for a display version of first order logic. This section explores the topic of string diagrams, in particular, we present two categorical formalisations of nominal string diagrams, along with a formal translation of ordinary string diagrams into nominal string diagrams (and vice versa).