F* is a programming language providing proof-assistant features such as dependent types, a rich logic with universes and tactics. Its primary goal is to implement security critical program e.g. cryptographic primitives (HACL*) or protocols (HTTPS in MiTLS), prove gradually their correction and extract to performant effectful low-level code. In order to achieve gradual proof of effectful code, F* relies on weakest-precondition indexed monads called Dijkstra monads. In this presentation we will explain why and how Dijkstra monads are used in F*, as well as how they are often derived from usual presentations of monads as can be found in more mainstream language such as Haskell.

n-fold categories are obtained by n-iterations of the internal category construction, starting from the category Cat. N-Fold categories satisfying the globularity condition correspond to strict n-categories. One can ask if there is an intermediate structure between n-fold categories and strict n-categories which is a model of weak n-categories. We answer this question positively with the introduction of the category of weakly globular n-fold categories. This category is based on a new paradigm to weaken higher categorical structures, and offers several advantages in terms of applications. We will illustrate how this model is part of a wider class of Segal-type models, and its equivalence with the Tamsamani-Simpson model of weak n-categories.

To describe systems composed of interacting parts, scientists and engineers draw diagrams of networks: flow charts, Petri nets, electrical circuit diagrams, signal-flow graphs, chemical reaction networks, Feynman diagrams and the like. In principle all these different diagrams fit into a common framework: the mathematics of symmetric monoidal categories. This has been known for some time. However, the details are more challenging, and ultimately more rewarding, than this basic insight. Two complementary approaches are presentations of symmetric monoidal categories using generators and relations (which are more algebraic in flavor) and decorated cospan categories (which are more geometrical). In this talk we focus on the latter.

The talk presents the theorems of Myhill-Nerode and Chomsky-Schützenberger using rewriting diagrams of semi-Thue systems as paradigm example of planar acyclic circuit diagrams (PLACIDs)—the “graphical syntax” of monoidal categories. The talk will focus on the proposal of a definition of recognizable language in a monoidal category, namely sets of arrows that coincide with the inverse image of their direct image under a monoidal functor to a finite monoidal category. For the case of PLACIDs, this class of languages is shown to coincide with the languages of automata in the sense of Bossut, under modest assumptions on gates of circuit diagrams; moreover, the usual notion of recognizable tree language is recovered. The talk presents the Myhill-Nerode theorem as a tool for solving Bossut's open problem of automata complementation. The remainder of the talk describes work in progress and future work, in particular the Chomsky-Schützenberger theorem for PLACIDs.

Contrary to traditional formulations of rewriting, which tend to rely on ideas such as category-theoretic double pushout constructions, the novel rule algebra framework is based upon the idea of interpreting rewriting rules as generators of certain diagrammatic algebras. In this whiteboard talk, I will present the core mathematical ideas and results, including the deep link between certain types of combinatorial Hopf algebras and rewriting theories. Some illustrative examples for the cases of discrete and graph rewriting will be provided.

Following the pattern of the Frobenius structure usually assigned to the 1-dimensional sphere, we investigate the Frobenius structures of spheres in all other dimensions. Starting from dimension $d=1$, all the spheres are commutative Frobenius objects in categories whose arrows are ${(d+1)}$-dimensional cobordisms. With respect to the language of Frobenius objects, there is no distinction between these spheres—they are all free of additional equations formulated in this language. The corresponding structure makes out of the 0-dimensional sphere not a commutative but a symmetric Frobenius object.

The talk is based on the paper “Spheres as Frobenius objects”, co-authored with Djordje Baralic and Sonja Telebakovic, which is available at arxiv.

It turns out that enumeration of graphs embedded on surfaces (an active area of combinatorics since Bill Tutte's pioneering work in the 1960s) has a variety of surprising links to the combinatorics of lambda calculus. In the talk, I will give a brief survey of these enumerative connections, then focus on the 1-to-1 correspondence (originally described in work by Bodini, Gardy, and Jacquot) between linear lambda terms and rooted trivalent maps. The key to understanding this bijection will be combining an interpretation of lambda terms as string diagrams with a Tutte-style decomposition of rooted trivalent maps with boundary. Finally, if time permits, I will discuss a suggestive analogy between typing and edge-coloring, and use this to motivate a deeper study of the surprisingly subtle typing properties of linear lambda terms.

We investigate monads of partiality in Martin-Löf type theory, following Moggi’s general monad-based method for modelling effectful computations. These monads are often called lifting monads and appear in category theory with different but related definitions. In this talk, we unveil the relation between containers and lifting monads. We show that the lifting monads usually employed in type theory can be specified in terms of containers. Moreover, we give a precise characterization of containers whose interpretations carry a lifting monad structure. We show that these conditions are tightly connected with Rosolini’s notion of dominance. We provide several examples, putting particular emphasis on Capretta’s delay monad and its quotiented variant, the non-termination monad.

It is well known that context dependent logical rules can be problematic both to implement and reason about. This is one of the factors driving the quest for better behaved, i.e., local, logical systems. In this talk we will present such a local system for linear logic (LL) based on linear nested sequents (LNS). Relying on that system, we propose a general framework for modularly describing systems combining, coherently, substructural behaviors inherited from \LL with simply dependent multimodalities. This class of systems includes linear, elementary, affine, bounded and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them. The resulting LNS systems can be adequately encoded into (plain) linear logic, supporting the idea that LL is, in fact, a ``universal framework'' for the specification of logical systems. From the theoretical point of view, we give a uniform presentation of LL featuring different axioms for its modal operators. From the practical point of view, our results lead to a generic way of constructing theorem provers for different logics, all of them based on the same grounds. This opens the possibility of using the same logical framework for reasoning about all such logical systems.

This is a joint work with Carlos Olarte and Björn Lellmann

There is a growing interest in programs proofs checked by computer. Proofs about programs are often very long and have to face a huge amount of cases due to the multiplicity of programs variables and the precise details of the programs. This is very frustrating since we would like to explain the proofs of correctness and publish them in scientific articles. However if one considers simple algorithms, we would expect to explain their proofs of correctness in the same way as we explain a mathematical proof for a non too complex theorem.

We present a human readable and rather intuitive formal proof for the classical Tarjan-1972 algorithms for finding strongly connected components in directed graphs. Tarjan’s algorithm consists in an efficient one-pass depth-first search traversal in graphs which traces the bases of strongly connected components. We describe the algorithm in a functional programming style with abstract values for vertices in graphs, with functions between vertices and their successors, and with data types such that lists (for representing immutable stacks) and sets. We use the Why3 system and the Why3-logic to express these proofs and fully check them by computer.

Type systems based on linear logic and their friends have proved that they are both capable of expressing a wealth of interesting abstractions. Among these the ability to mix garbage-collected and explicitly managed data in the same language. This is of prime interest for distributed computations that need to reduce latency induced by GC pauses: a smaller GC heap is a happier GC heap.

I had always had the belief that to add linear types to a language was a rather intrusive procedure and that a language with linear types would basically be an entirely new language. The Rust language is a case in point: it has a linear-like type system, but it's a very different language from your run-of-the-mill functional language.

This turns out not to be the case: this talk presents a way to extend a functional programming language. We are targeting Haskell but there is little specific to Haskell in this presentation. I will focus mostly on the type system and how it can be generalised: among other things the type system extends to dependent types.

Interaction morphisms

Tarmo Uustalu, Tallinn U of Technology

I will propose interaction morphisms as a means to specify how an effectful computation is to be run, provided a state in a context. An interaction morphism of a monad T and a comonad D is a family of maps T X x D Y → X x Y natural in X and Y and subject to some equations. Interaction morphisms turn out to be a natural concept with a number of neat properties. In particular, interaction morphisms are the same as monoids in a certain monoidal category; interaction morphisms of T and D are in a bijective correspondence with carrier-preserving functors between the categories of coalgebras of D and stateful runners of T (monad morphisms from T to state monads); they are also in a bijective correspondence with monad morphisms from T to a monad induced in a certain way by D.

This is joint work with Shin-ya Katsumata (University of Kyoto).

The lambda-calculus studies the dynamics of computation, but the complexity of one computation path cannot be forecast, neither in time nor in space, and there is no direct control on the execution environment.

One approach for the former is to gain more control over duplication and deletion of terms, by introducing sharings of common subterms inside a lambda-term, similarly to optimal reduction graphs. This has been done by Gundersen, Heijltjes and Parigot, via the atomic lambda-calculus, a calculus extending the lambda-calculus with explicit sharings, and allowing duplications on individual constructors. It enjoys full-laziness, avoiding unnecessary duplications of constant expressions.

For the latter, an extension of the lambda-calculus linking classical formulas to control flow constructs via Curry-Howard correspondence, the lambda-mu-calculus, was developed by Parigot. New operators in the lambda-mu-calculus correspond to continuations, representing the remaining work in a program.

Can we combine sharing with control operators and thus obtain another extension of the lambda-calculus satisfying full-laziness and featuring control operators? A first challenge is to combine explicit sharings or substitutions with mu-reduction and substitution, and we introduce a right-associative application as in Saurin-Gaboardi's lambda-mu-calculus with streams to overcome this challenge. Another difficulty is to adapt the type system for lambda-mu with multiple conclusions, distinguishing one main conclusion (with a meta-disjunction connective), to a type system in which each rule can be applied to atoms (which corresponds to duplications on individual term constructors), and where no distinction is made between object and meta-level. I will present how to combine these two type systems in the simplest possible way.

I will present the atomic lambda-mu-calculus, which aims to naturally extend the two calculi presented above, giving the simplest type system combining and preserving their properties.