ABSTRACT. The nominal approach to the specification of languages with binding operators, introduced by Gabbay and Pitts, has its roots in nominal set theory. With a user-friendly first-order syntax, nominal logic provides a formal framework to reason about binding operators similar to conventional, on-paper reasoning. Indeed, nominal logic uses the well-understood concept of permutation groups acting on sets to provide a rigorous first-order treatment for the common informal practice of fresh and bound names.

In this talk, I will present our current work towards incorporating nominal techniques into two widely-used rule-based first-order verification environments: the K specification framework and the Maude programming environment.

ABSTRACT. We consider an extension of multiplicative linear logic which encompasses bayesian networks and expresses samples sharing and marginalisation with the polarised rules of contraction and weakening. We introduce the necessary formalism to import exact inference algorithms from bayesian networks, giving the sum-product algorithm as an example calculating the weighted relational semantics of a multiplicative proof-net in a quite efficient way.

ABSTRACT. Linear Logic refines Intuitionnistic Logic by taking into account the resources used during the proof and program computation. In the past decades, it has been extended to various frameworks. The most famous are indexed linear logics which can describe the resource management or the complexity analysis of a program. From an other perspective, Differential Linear Logic is an extension which allows the linearization of proofs. In this article, we merge these two directions by first defining a differential version of Graded linear logic: this is made by indexing exponential connectives with a monoid of differential operators. We prove that it is equivalent to a graded version of previously defined extension of finitary differential linear logic. We give a denotational model of our logic, based on distribution theory and linear partial differential operators with constant coefficients.

ABSTRACT. We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus for *-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo. This yields a much richer equational theory involving distributivity and annihilation laws. The unit-free case is given by relying on the proof-net syntax introduced by Hughes and Van Glabbeek. We then use the sequent calculus to extend our results to full MALL (including all units).

ABSTRACT. This work aims at exploring the algebraic structure of concurrent processes and their behaviour independently of a particular formalism used to define them. We propose a new algebraic structure, which we name conjunctive linear algebras, as a basis for an algebraic presentation of concurrent realizability, following ideas of the algebrization program already developed in he realm of classical and intuitionistic realizability. In particular, we show how any conjunctive linear algebra provides a sound interpretation of multiplicative linear logic. This new structure involves, in addition to the tensor and the orthogonal map, a parallel composition. We define the canonical model of this structure as induced by a variant of the π-calculus with global fusions. Using a model of terms, we prove that the parallel composition cannot be defined from the conjunctive structure alone.

ABSTRACT. In this paper we adapt previous work on rewriting string diagrams using hypergraphs to the case where the underlying category has a traced comonoid structure, in which wires can be forked and the outputs of a morphism can be connected to its input. Such a structure is particularly interesting because any traced Cartesian (dataflow) category has an underlying traced comonoid structure. We show that certain subclasses of hypergraphs are fully complete for traced comonoid categories: that is to say, every term in such a category has a unique corresponding hypergraph up to isomorphism, and from every hypergraph with the desired properties, a unique term in the category can be retrieved up to the axioms of traced comonoid categories. We also show how the framework of double pushout rewriting (DPO) can be adapted for traced comonoid categories by characterising the valid pushout complements for rewriting in our setting.

We conclude by presenting a case study in the form of recent work on an equational theory for sequential circuits: circuits built from primitive logic gates with delay and feedback. The graph rewriting framework allows for the definition of an operational semantics for sequential circuits.

ABSTRACT. The celebrated Squier theorem allows to prove coherence properties of algebraic structures, such as MacLane's coherence theorem for monoidal categories, based on rewriting techniques. We are interested here in extending the theory and associated tools simultaneously in two directions. Firstly, we want to take in account situations where coherence is partial, in the sense that it only applies for a subset of structural morphisms (for instance, in the case of the coherence theorem for symmetric monoidal categories, we do not want to strictify the symmetry). Secondly, we are interested in structures where variables can be duplicated or erased. We develop theorems and rewriting techniques in order to achieve this, first in the setting of abstract rewriting systems, and then extend them to term rewriting systems, suitably generalized in order to take coherence in account. As an illustration of our results, we explain how to recover the coherence theorems for monoidal categories and symmetric monoidal categories.

ABSTRACT. We show that certain diagrams of $\infty$-logoses are reconstructed in internal languages of their oplax limits via lex, accessible modalities, which enables us to use plain homotopy type theory to reason about not only a single $\infty$-logos but also a diagram of $\infty$-logoses. This also provides a higher dimensional version of Sterling's synthetic Tait computability---a type theory for higher dimensional logical relations.

ABSTRACT. In the process of designing a computer system $S$ and checking whether an abstract model $\mathcal{M}$ of $S$ verifies a given specification property $\eta$, one might have only a partial knowledge of the model, either because $\mathcal{M}$ has not yet been completely defined (constructed) by the designer, or because it is not completely observable by the verifier. This leads to new verification problems, subsuming satisfiability and model checking as special cases. We state and discuss these problems in the case of LTL specifications, and develop a uniform tableau-based approach for their solutions.

ABSTRACT. In this paper, we define a temporal extension of Bunched Implication Logic (BI), called LTBI, that combines the LTL temporal connectives with BI connectives. After studying its semantics and illustrating its expressiveness, we design a tableau calculus with labels and constraints for this new logic. We prove its soundness w.r.t. the Kripke-style semantics of LTBI before discussing the issues that make the completeness of the calculus not trivial in the general case of an unbounded timeline.