Preface

By calling into question the implicit structural rules that are taken for granted in classical logic, substructural logics have brought to the fore new forms of reasoning with applications in many interdisciplinary areas of interest. Modalities, in the substructural setting, provide the tools to control and finetune the logical resource management.

The workshop 'Modalities in substructural logics: applications at the interfaces of logic, language and computation' aimed to explore the uses of substructural modalities in areas where logic meets linguistics and computer science. The workshop, endorsed by the Horizon 2020 project MOSAIC, was held on 7 and 8 August 2023 in Ljubljana, Slovenia, as part of the 34th European Summer School in Logic, Language and Information (ESSLLI 2023). The present volume collects the contributed papers and the abstracts of the invited talks.

The Programme Committee of the workshop had the following composition.

• Nick Bezhanishvili (U of Amsterdam)

• Sabine Fritella (INSA)

• Rajeev Goré (ANU Canberra)

• Giuseppe Greco (Vrije Universiteit Amsterdam)

• Rosalie Iemhoff (Utrecht University)

• Michael Moortgat (Utrecht University, co-chair)

• Richard Moot (LIRMM Montpellier)

• Valeria de Paiva (Topos Institute, Berkeley)

• Mehrnoosh Sadrzadeh (UCL, co-chair)

• Andre Scedrov (UPenn)

• Sonja Smets (U of Amsterdam)

We thank the members of the Programme Committee for their efforts.

Michael Moortgat and Mehrnoosh Sadrzadeh
Utrecht and London

Modalities in the Type Theory of Quantum Programming

Quantum computing takes advantage of quantum resources and processes by controlling them classically. The integration of the classical and the quantum, as well as the non-classical features of quantum physics, poses an array of challenges to quantum programming languages and their type theory. The most salient of those challenges may be the one arising from the 'no cloning' property of quantum physics. This property dictates that quantum resources cannot generally be copied or duplicated, and therefore makes it desirable that a quantum programming language has a linear type theory in which a given quantum data can only be used once. Not everything in quantum computing is linear, however, since classical control involves classical data that can be used multiple times. A desirable language of quantum programming should be sensitive to duplicability and unduplicability of data, so that it permits duplication of the duplicable and prohibits duplication of the unduplicable. Its type theory should therefore not only be linear but also have a way of capturing the modality of duplicability, such as the ! ('bang') operator in linear logic.

Indeed, one will find many more modalities when they reflect on the features of quantum computing that quantum programming languages need to accommodate. Quantum computing typically proceeds by compiling or generating a quantum circuit on a classical device and running or executing the circuit on a quantum device. A quantum programming language should be able to not only compile circuits by appending gates one by one, but also apply meta-level operations to circuits such as reversing, controlling, iterating, etc. The language should then be sensitive to the modalities of reversibility and controllability, since not every circuit is reversible or controllable. This talk explores various modalities of this sort.

Particular emphasis will be given to the following two modalities. Firstly, the two-runtime structure of quantum computing means that, while some values are known at circuit-generation time, other values can only be known, if at all, at circuit-execution time. The distinction between these two sorts of values is closely tied to duplicability and unduplicability, but is a separate modality. Secondly, many quantum algorithms require that circuit-execution time be followed by another circuit-generation time at which different circuits be generated depending on the result of the previous circuit execution. This means that, while evaluation of some terms results in circuits within a single circuit-generation time, evaluation of other terms does not but instead results in 'thunks' that represent suspended computations. This fact gives rise to the modality called 'boxability', distinguishing circuits as actual data structures - to which meta-level operations can be applied as well as that can be fed to a quantum device - from mere thunks. I will illustrate the type theory and semantics of these modalities.

This talk is based on joint work with Frank Fu, N. Julien Ross, and Peter Selinger [1,2].

Multi-type Calculi and Structural Control

In recent years, the multi-type approach to the automatic generation of analytic calculi for classes of logics has emerged, initially motivated by the goal of extending the reach of proper display calculi [16] (characterizations of those logics amenable to be captured by proper display calculi have been given in [5,13]) as a proof-theoretic format. This approach draws on semantic insights to obtain proof-theoretic results. Specifically, it hinges on the possibility of equivalently reformulating the algebraic semantics of a given logic in terms of a suitable variety of heterogeneous algebras [3], algebraic structures as in universal algebra in which more than one domain is allowed. Well-known logical frameworks to which the multi-type methodology has been successfully applied include first-order logic [1], dynamic epistemic logic , linear logic [11], monotone modal logic [4], semi-De Morgan logic [12], the logic of lattices [14], of bilattices [10], of rough algebras [9], and inquisitive logic [7,8].

Although these logical frameworks are very different from one another, both technically and conceptually, a common core to their being not properly displayable was precisely identified in the encoding of key interactions between different types, displaying different behaviour. For instance, for dynamic epistemic logic the difficulties lay in the interaction between (epistemic) actions, agents' beliefs, and facts of the world; for propositional dynamic logic, in the interaction between general and iterative actions; for linear logic, between general resources and reusable resources; for inquisitive logic, between general formulas (having both a sentential and an inquisitive content) and flat formulas (having only a sentential content). In each case, precisely the formal encoding of these interactions gave rise to non-analytic axioms in the original formulations of the logics. In each case, the multi-type approach allowed us to redesign the logics, so as to encode the key interactions into analytic multi-type rules, and define a multi-type analytic calculus for each of them. Metaphorically, adding types is analogous to adding dimensions to the analysis of the interactions, thereby making it possible to unravel these interactions, by reformulating them in analytic terms within a richer language.

Besides being used to solve technical problems of existing logics, the multi-type methodology can be also used for different purposes; for instance, as a design framework for new logics that serve to analyze specific interactions, as done in [2]. Precisely in this context, in [11], it is illustrated by a toy example how the multi-type framework can usefully be applied as a formal environment for accounting for various forms of grammatical exceptions in formal linguistics, and on this basis, it is argued that this methodology can be a useful tool for further developing structural control in type logical theory [15]. In this talk, I will discuss these ideas and propose some research directions.