The theory of decomposition spaces arose out of a need for a more flexbible framework for incidence (co)algebras and Möbius inversion than the classical setting of locally finite posets. As the name suggests, it is a theory of decomposition rather than composiition (as in categories), and it appears that all combinatorial coalgebras are incidence coalgebras of a decomposition space (whereas many of them cannot be realised directly as the incidence coalgebra of any poset). The lectures will be an introduction to decomposition spaces from the viewpoint of combinatorics, but the tools come from category theory and simplicial homotopy theory.

The first lecture will start with a brief review of the classical Möbius functioin in number theory, and Rota's theory for locally finite posets. Here the notion of reduction is important: often it has the flavour of cooking up an auxiliary poset in order to apply the classical theory, and then impose an equivalence relation so as to arrive at the coalgebra actually needed. With this motivation, we then move on to Möbius categories and decomposition spaces, and go through some examples beyond posets, such as the chromatic Hopf algebra of graphs and the Butcher-Connes-Kreimer Hopf algebra of rooted trees.

The second lecture will be a bit more categorical, including an introduction to objective algebraic combinatorics using objective linear algebra: this is linear algebra with coefficients in sets and groupoids instead of number coefficients. Slice categories play the role of vector spaces, and linear functors (given by spans) play the role of linear maps. By working at this level, the theory of decomposition spaces can be seen as a systematic way of lifting coalgebraic identities to 'bijective proofs'. I'll spend some time explaining the need for groupoids and homotopy theory, exemplified with the Faà di Bruno bialgebra.

The third lecture focuses on functorialities, explaining how certain simplicial maps called CULF and IKEO induce coalgebra homomorphisms. Especially important is the simplicial notion of decalage, which underlies many of the reductions in classical theory. CULF maps also enter in the definition of monoidal decomposition spaces, in turn inducing bialgebras and Hopf algebras (rather than just coalgebras). I hope to be able to finish with some potential applications to process calculi and quantum logic. Sometimes processes cannot be composed, or can be composed in many ways. Often this means there is instead a well-defined decomposition operation, and likely a decomposition space. Similarly, effect algebras and effect algebroids describe situations where composition is only partially defined, with axioms ensuring that they are in fact examples of decomposition spaces.

Zoom meeting link

For applications of logic it is often desirable to have a common umbrella encompassing both classical discrete two-valued and quantitative continuous many-valued reasoning.  What are principled ways to extend 2-valued modal logic to many-valued modal logic? What is a suitable generalization of Kripke semantics to this setting? We will explain how category theory allows us to build a general framework to answer these questions. The key observation is that 2 is not only the familiar Boolean algebra but also an instance of a more general structure known as a quantale. A quantale is simply a complete lattice with a little extra structure. As observed by Lawvere in 1973, this extra structure allows us to extend ordinary 2-valued logic to a generalized logic that takes truth values in an arbitrary quantale. The models of such generalized logics encompass a variety of structures including (generalized partial) metric spaces. In this talk, we will give an introduction to this area of logic and also sketch some novel results about canonical extensions of fuzzy-algebras obtained in collaboration with Apostolos Tzimoulis.

Static resource analysis is dedicated to finding methods to determine the quantity of resources (time, energy, memory, …) required to run a program, together with the variables this quantity depends on. The cornerstone of this endeavor is finding invariants/variants between program states: an analyser must automatically understand the algorithms encoded into the program without programmer input.

We focus on resource analyses through type systems for functional languages. To this aim, we introduce AutoBill, an abstract machine used as intermediate representation for resource analysis, based on the lambda-mu-mutilde calculus. We compile to this machine, amongst others, an ML-style language with data-structures (ADT), recursion (fixpoints), and some further extensions.

AutoBill uses Call-by-Push-Value operational semantics, which mixes call-by-value and call-by-name, to encode the runtime semantics of functional languages. The use of an abstract machine furthermore allows continuations to be encoded as explicit call stacks. This in turns enables the re-use of data structures analyses to analyse control flow within programs.

On top of our machine, a linear type system explicits the resource flow that accompanies jumping in and out of computations. Those types are enriched with integer parameters, that are controlled during type-checking through the addition of equations and constraints to data-type definitions. This enables the approximating sizes, costs, combinatorial invariant, etc. in a first-order constraint, and provides a link between those quantities and the largest resource usage occurring at runtime. This is done during type-inference, and the constraint is then sent to an SMT solver for validation, or to a linear programming optimizer to generate resource bounds.

We implement the “Automated Amortized Resource Analysis” method in AutoBill. It assigns, to each data-structure, a count of the amount of sub-structures with some relevant shape. This is then used to bound the iteration counts of an algorithm and obtain polynomial worst-case complexities. Our implementation consists of a specialized compilation scheme from a source language to the abstract machine. The typing-and-analysis engine is then independent of both the source language and the chosen analysis method.

Programs in numerical analysis and scientific computing make heavy use of floating-point numbers to approximate ideal real numbers. Operations on floating-point numbers incur roundoff error, and an important practical problem is to bound the overall magnitude of the error for complex computations. Existing work employs a variety of strategies such as interval arithmetic, SMT encodings, and global optimization; however, current methods are not compositional and are limited in scalability, precision, and expressivity.

Today, I'll talk about some of our recent work on NumFuzz, a higher-order language that can bound forward error using a linear, coeffect type system for sensitivity analysis combined with a novel quantitative error type. Our type inference procedure can derive precise relative error bounds for programs that are several orders of magnitude larger than previously possible.

If time permits, I'll briefly discuss a second type system called Bean for bounding backward error. Like NumFuzz, Bean is based on a linear coeffect type system, but it features a semantics based on a novel category of lenses on metric spaces. Bean is the first system to soundly reason about backward error in numerical programs.

Joint work with Ariel Kellison, Laura Zielinski, and David Bindel.

We introduce Coma, a formally defined intermediate verification language. Specification annotations in Coma take the form of assertions mixed with the executable program code. A special programming construct representing the abstraction barrier is used to separate, inside a subroutine, the “interface” part of the code, which is verified at every call site, from the “implementation” part, which is verified only once, at the definition site. In comparison with traditional contract-based specification, this offers us an additional degree of freedom, as we can provide separate specification (or none at all) for different execution paths. For programs where specification is given in a traditional way, with abstraction barriers at the function entries and exits, our verification conditions are similar to the ones produced by a classical weakest-precondition calculus. For programs where abstraction barriers are placed in the middle of a function definition, the user-written specification is seamlessly completed with the verification conditions generated for the exposed part of the code. In the talk, we present the language, the rules of verification condition generation, and the current implementation of Coma.

Automatic Differentiation is the study of the efficient computation of differentials. While the first automatic differentiation algorithms are concomitant with the birth of computer science, the specific backpropagation algorithm has been brought to a modern light by its application to neural networks. This work unveils a surprising connection between backpropagation and Gödel's Dialectica interpretation, a logical translation that realizes semi-classical axioms. This unexpected correspondence is exploited through different logical settings. In particular, we show that the computational interpretation of Dialectica translates to the differential λ-calculus and that Differential Linear Logic subsumes the logical interpretation of Dialectica.

https://chocola.ens-lyon.fr/events/meeting-2025-03-13/

In this talk, we will introduce Owi, a symbolic execution engine for WebAssembly (Wasm). We will begin by detailing how we extended a concrete Wasm interpreter to support symbolic execution. Next, we will show how we used OCaml 5 to parallelize the exploration, allowing multi-core execution. Since Wasm is a compilation target, we will demonstrate how Owi can be applied to perform symbolic execution of programs written in C, C++ and Rust by compiling them to Wasm. Finally, we will give examples of practical applications of symbolic execution, such as bug finding or solver-aided programming.

Voir le site du séminaire CHOCOLA.

https://chocola.ens-lyon.fr/events/meeting-2025-02-06/

The convertibility test, which checks if two λ-terms are equal up to β-reduction, is an essential part of typechecking and proof verification in proofs assistants based on type theory, such as Coq, Agda and Lean. Naturally, the correctness of such a test is necessary to ensure the proofs thus verified are valid; but having an efficient test is also required both for real-time interaction with the user, and for proof search.

In this presentation, we start with an efficient, strong call-by-need, big-step semantics for the λ-calculus, which is the critical building block to implement a convertibility test in a classical manner. We then show how we can improve upon this by considering the convertibility problem in its entirety, viewing it as proof search. To this end, we study what can be considered a (non-)convertibility proof, drawing upon existing work.

This gives rise to a new parallel, heuristic-less algorithm for this test, which does not duplicate computations, and comes with worst-case complexity guarantees. We derived a virtual machine from this algorithm, and made it more efficient by following Grégoire and Leroy, showing that our algorithm is suited to compilation of the input λ-terms for additional efficiency. Both this semantics and this efficient parallel convertibility test have been implemented in OCaml and experimentally validated, significantly outperforming Coq in some cases. They are also both formalised and verified using Coq, building confidence in our work.

This talk will present MARVeLus, a cyber-physical systems language which combines verification, simulation, and implementation. The language is based on Zélus, a modern version of Lustre, where we add refinement types and associated typing rules. Our refinement types can express temporal-logic-based safety properties and prove them using a rich type system in the style of deductive verification. The language comes with an implementation, and a platform enabling execution on physical robots. Although our current implementation is limited to verifying properties about discrete constructs of Zélus, the talk will also present early efforts extending the proof systems to continuous constructs of Zélus, inspired by differential dynamic logic.