The (bi)category of profunctors on groupoids is a categorification of the relational model of linear logic. Its objects are not just sets but rather sets whose elements are equipped with groups encoding their symmetries, and its morphisms carry actions by these symmetries. While detailed information on such symmetries helps with, e.g., adequacy proofs of profunctorial models, it makes operations such as composition more difficult to compute. A way to ease the computation is to transform a profunctor into a matrix. Although the matrix representation is not functorial in general, it is known to behave well for certain subclasses, such as the class of profunctors definable by λ-terms. The mathematical reason behind this phenomenon, however, was not understood. This paper shows that the key is stability. Stability is a classical concept in domain theory, and has been extended to profunctors in Taylor’s work and further developed by Fiore et al. All λ-definable profunctors are known to be stabilized, and we show that the matrix representation behaves well for stabilized profunctors. We prove that the matrix representation defines a functor from stabilized profunctors to matrices that preserves the linear logic structures.

In this paper, we establish the foundations of a novel logical framework for the π-calculus, based on the deduction-as-computation paradigm. Following the standard proof-theoretic interpretation of logic programming, we represent processes as formulas, and we interpret proofs as computations. For this purpose, we define a cut-free sequent calculus for an extension of first-order multiplicative and additive linear logic. This extension includes a non-commutative and non-associative connective to faithfully model the prefix operator, and nominal quantifiers to represent name restriction. Finally, we design proof nets providing canonical representatives of derivations up to local rule permutations.

Quantum Separation Logic (QSL) has been proposed as an effective tool to improve the scalability of deductive reasoning for quantum programs. In QSL, separation is interpreted as disentanglement , and the frame rule brings a notion of entanglement-local specification (one that only talks about the qubits entangled with those acted upon by the program). In this paper, we identify two notions of locality unique to the quantum domain, and we construct a novel quantum separation logic, RapunSL , which is able to soundly reduce reasoning about superposition states to reasoning about pure states ( basis-locality ), and reasoning about mixed states arising from measurement to reasoning about pure states ( outcome-locality ). To do so, we introduce two connectives, linear combination and mixing, which together with separation provide a dramatic improvement in the scalability of reasoning, as we demonstrate on a series of challenging case studies.

Uncomputation is a feature in quantum programming that allows the programmer to discard a value without losing quantum information, and that allows the compiler to reuse resources. Whereas quantum information has to be treated linearly by the type system, automatic uncomputation enables the programmer to treat it affinely to some extent. Automatic uncomputation requires a substructural type system between linear and affine, a subtlety that has only been captured by existing languages in an ad hoc way. We extend the Rust type system to the quantum setting to give a uniform framework for automatic uncomputation called Qurts (pronounced quartz). Specifically, we parameterise types by lifetimes, permitting them to be affine during their lifetime, while being restricted to linear use outside their lifetime. We also provide two operational semantics: one based on classical simulation, and one that does not depend on any specific uncomputation strategy.