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.

Traditionally, computability theory is based on a notion of computable functions induced by concrete models like Turing machines, lambda calculus, or general recursion. While these models are well-studied, they only provide a somewhat secondary explanation of computability, at times obscuring the simple computational essence of abstract constructions and constituting a notorious burden for mechanisation in a proof assistant. In this talk, I will give an overview of synthetic computability theory as introduced by Richman and Bauer, offering an elegant alternative: at the price of giving up on some principles of classical reasoning, computability becomes a primitive notion, even internalisable by the axiom that every function is computable. After discussing this general framework in the context of constructive mathematics, I will describe some recent work on Gödel’s incompleteness theorem and Post’s problem both developed synthetically in constructive type theory and mechanized in the Coq proof assistant.

Categories with families (CwF) are perhaps the most widely used notion of models for dependent types. They can be described by an algebraic signature with dependent sorts for contexts, substitutions, types and terms, as well as a plethora of constants and equations. Unfortunately, this mix of dependent sorts and equations is particularly prone to transport hell, and in practice it is nearly impossible to prove non-trivial results using CwFs in a proof assistant. In this talk, I will present a method based on Pédrot's “prefascist sets” to strictify (nearly) all the equations of a CwF, so that they hold by definition. I will then discuss applications of this method to proofs of canonicity and normalisation by Gluing. This is joint work with Ambrus Kaposi.

Voir https://www.irif.fr/rencontres/rentree_pps2024/index

The fastest JavaScript production implementations use just-in-time (JIT) compilation and the vast majority of academic publications about implementations of dynamic languages published during the last two decades focus on JIT compilation. This does not imply that static compilers (AoT) cannot be competitive; as comparatively little effort has been spent creating fast AoT JavaScript compilers, a scientific comparison is lacking. This paper presents the design and implementation of an AoT JavaScript compiler, focusing on a performance analysis. The paper reports on two experiments, one based on standard JavaScript benchmark suites and one based on 31 new benchmarks chosen for their diversity of styles, authors, sizes, provenance, and coverage of the language. The first experiment shows an advantage to JIT compilers, which is expected after the decades of effort that these compilers have paid to these very tests. The second shows more balanced results, as the AoT compiler generates programs that reach competitive speeds and that consume significantly less memory. The paper presents and evaluates techniques that we have either invented or adapted from other systems, to improve AoT JavaScript compilation.

Redexes have residuals and can create new redexes in the (typed or untyped) lamda-calculus. We will review these basic notions which are at the heart of strong normalization and reduction strategies. This talk deals with permutation equivalence, residuals modulo permutations, redex families, the labeled lambda-calculus, general finite developments and optimal reductions.

The talk is a revised version of an article published in the book “The French School of Programming”, Springer, 2024.

Gabriel-Ulmer duality is a contravariant biequivalence between small finite-limit categories and locally finitely presentable categories, which in the spirit of Lawvere's functorial semantics can be viewed as a *theory-model duality*: small finite-limit categories C are viewed as theories, and the lfp category FL(C, Set) of finite-limit preserving Set-valued functors is viewed as category of models of of C. The opposite of C can be reconstructed up to equivalence from Lex(C,Set) as full subcategory of *compact* objects.

The talk presents a *refinement* of Gabriel-Ulmer duality which is motivated by dependent type theory: finite-limit categories are replaced by *clans*, ie categories with a terminal object and a pullback-stable class of maps which is closed under composition, reflecting the structure of syntactic categories of *generalized algebraic theories* (GATs). The category of models of every GAT/clan is lfp, and to be able to reconstruct the clan we equip it with a *weak factorization system*, which in the classical case of ordinary algebraic theories (groups, rings, …) consists of projective extensions on the left, and regular epimorphisms on the right.

Details can be found in the following preprint:

https://arxiv.org/abs/2308.11967

Initially introduced by Renoylds for the Forsythe language, the merge operator increases the expressiveness of terms within intersection polymorphism. It generalizes record concatenation to any term, enabling function overloading and expressive forms of object composition, and offers the promise of a compositional style of statically typed programming in which solutions to the expression problem arise naturally.

However, the operational semantics of an unconstrained merge lacks both determinism and subject reduction. So disjointness relations have been introduced to forbid merging values from overlapping type. In this talk, we will present calculi with disjoint intersection types with type-directed operational semantics (TDOS), which ensures determinism and type soundness, and supports features such as recursion and impredicative polymorphism. Additionally, a novel algorithm for the subtyping of intersection types with distributive laws is introduced, allowing for a simple proof of transitivity and the modular addition of distributivity rules without preprocessing on types. All the results are formalized in Coq.

Please see https://chocola.ens-lyon.fr/events/meeting-2024-09-19/ for the talk abstracts.

https://www.irif.fr/rencontres/pps2024/index

To be debated: same philosophical questions as the preceding day.

https://www.irif.fr/rencontres/pps2024/index

We will address two typical philosophical questions: What are we doing ? Where are we going ?

Most code is executed more than once. If not entire programs then libraries remain unchanged from one run to the next. Just-in-time compilers expend considerable effort gathering insights about code they compiled many times, and often end up generating the same binary over and over again. We explore how to reuse compiled code across runs of different programs to reduce warm-up costs of dynamic languages. We propose to use speculative contextual dispatch to select versions of functions from an off-line curated code repository. That repository is a persistent database of previously compiled functions indexed by the context under which they were compiled. The repository is curated to remove redundant code and to optimize dispatch. We assess practicality by extending Ř, a compiler for the R language, and evaluating its performance. Our results suggest that the approach improves warmup times while preserving peak performance.

There are well-known dualities of computation in both functional and concurrent programming: input/output, expression/context, strict/lazy, sender/receiver, forward/backwards, and several others. When viewed through an algebraic lens, these can be understood as metaphysical interpretations of rigorous mathematical dualities.

In this talk, I will explore the duality of values and continuations (Filinski'89) through the lens of cartesian closure/co-cartesian co-closure. The main observation is that, just as higher-order functions give exponentials, higher-order continuations give co-exponentials. Using this semantic duality, I will present a λλ~ (lambda-lambda-bar or tilde) calculus, which exhibits a duality of abstraction/co-abstraction. I will develop the syntax and semantics of this language, which gives a computational interpretation in terms of speculative execution and backtracking.

Using this language, I will show how to recover classical control operators, the computational interpretation of classical logic, and a complete axiomatisation of control effects. Finally, I will show how this dualises Lambek's functional completeness, thereby dualising Hasegawa's decomposition of λ-calculus into first-order κ/ζ-calculi.

A classical result in concurrency theory shows that an algebraic interpretation of Petri nets in terms of commutative monoids can be used to provide a characterisation of the deterministic computations of a net via monoidal categories, accounting for their sequential and parallel composition. In turn, this characterisation leads to the interpretation of such computations as sequents of the multiplicative fragment of linear logic. The talk presents a survey of the topic, including recent results concerning non-deterministic computations and their characterisation in terms of dioidal categories, the categorical equivalent of tropical semirings, as well as suggesting a possible connection with the multiplicative additive fragment of linear logic.

I will give an introduction to directed algebraic topology and its application in concurrency theory, covering directed spaces, directed paths, and directed homotopies. Then I will touch upon the combinatorial side of things, precubical sets and higher-dimensional automata (HDAs), which will bring us to the second part of the talk: the language theory of HDAs. This makes the connection back to the initial motivation, concurrency theory, and also gives new inspiration and tools to directed topology.

Software sciences have a role to play in the description, the organization, the execution, and the analysis of the molecular interaction systems such as biological signaling pathways. These systems involve a huge diversity of bio-molecular entities whereas their dynamics may be driven by races for shared resources, interactions at different time- and concentration-scales, and non-linear feedback loops. Understanding how the behavior of the populations of proteins orchestrates itself from their individual interactions, which is the holy grail on systems biology, requires dedicated languages offering adapted levels of abstraction and efficient analysis tools.

In this talk we describe the design of formal tools for Kappa, a site-graph rewriting language inspired by bio-chemistry. In particular, we introduce a static analysis to compute some properties on the biological entities that may arise in models, so as to increase our confidence in them. We also present a model reduction approach based on a study of the flow of information between the different regions of the biological entities and the potential symmetries. This approach is applied both in the differential and in the stochastic semantics.

To better understand Barendregt's genericity for the untyped call-by-value lambda-calculus, we start by first revisiting it in call-by-name, adopting a lighter statement and establishing a connection with contextual equivalence. Then, we use it to give a new, lighter proof of maximality of head contextual equivalence, i.e. that H* is a maximal consistent equational theory. We move on to call-by-value, where we adapt these results and also introduce a new notion dual to light genericity, that we dub co-genericity. We present light (co-)genericity as robust properties rather than just lemmas and provide different proofs based on applicative bisimilarity, semantic models and direct rewriting techniques.

CompCert is the only formally-verified C compiler, and one of the very few formally verified compilers altogether. It is intended for use for safety-critical applications. I will discuss some improvements we implemented over CompCert: new VLIW target, new optimizations, and security features. A lot of our development uses untrusted oracles implemented in OCaml plus a formally verified checker. I will discuss typing issues regarding this interface and some questions we have about them.

Over the past 5 to 10 years, machine learning has revolutionised program synthesis. In this talk we'll present ProgSynth, a general purpose program synthesis tool based on neurosymbolic methods. We'll discuss some challenges: combinatorial search, semantic program synthesis, and reinforcement learning.

A first such link appeared in the context of previous work, in which we provided an algebraic formalisation of categorical coherence theorems in higher dimensional analogs of Kleene algebras. I will briefly recall our definition of the latter and the associated coherence theorems. However, this link between categorical and algebraic structures has since led us to a Jónsson-Tarski correspondance between (higher) catoids, generalizations of (higher) categories, and (higher) quantales. The latter were introduced as a non-commutative extension of locales, and have since also been studied in the context of categorical logic. The first part of this talk will focus on this correspondance and its extension to the associated convolution algebras. These results, as well as the coherence theorem described above, have been formalized in the proof assistant Isabelle.

In the second part of this talk, I will describe ongoing work relating rewriting, quantales, and (directed) topological methods. The goal of this work is to describe the congruences of multinomial lattices and their continuous analogs, in particular the quantale Qv(I) of sup-continuous endomorphisms of the ordered unit interval. The former, generalizing the permutohedra, provide a description of the rewriting system associated to commutativity on finite words, while the latter are studied in the context of categorical linear logic. These structures all have an interpretation as directed spaces, the homotopy types of which are closely related to their congruences. I will describe this correspondance, and briefly discuss the use of topological duality in our ongoing study of these structures.

An “element-free” probability distribution is what remains of a probability distribution after we forget the elements to which the probabilities were assigned. These objects naturally arise in Bayesian statistics, in situations where the specific identity of elements is not important. This talk is about the theory of element-free distributions in the category of measurable spaces. I will explain the basic concepts, and then present two new results which demonstrate that element-free distributions are a canonical notion. The first result is a categorical version of a representation theorem for random partitions, originally due to Kingman, which characterises the space of element-free distributions as a limit in the Kleisli category for the Giry monad G. The second result establishes a correspondence between random element-free distributions and natural transformations of type G → GG. I will sketch the relevance of this theory to nonparametric Bayesian clustering.

This is joint work with Victor Blanchi.

Proof assistant kernels are a natural target for program certification: they are small, critical, and well-specified. Still, despite the maturity of the field of software certification, we are yet to see a certified Agda, Coq or Lean. In this talk, I will try and explain why this is not such an easy task, and present two complementary projects going in that direction. The first, MetaCoq, is a large scale project, broadly aiming at giving tools to manipulate Coq terms and derivations inside of Coq, in particular developing an important body of formalized proofs around Coq's typing. The second is a more recent endeavour, aimed at tackling the mother of all properties: normalisation.

The game comonads research programme, started by Samson Abramsky and Anuj Dawar in 2017, provides categorical accounts of key constructions in finite model theory, and has led to an axiomatic approach to various notions of logical resources central to this field.

I will outline some preliminary ideas on how to bring the tools of homotopy theory to the research area of game comonads, with the aim of tackling open questions concerning e.g. expressive completeness and preservation results.

Joint session with the CHOCOLA seminar. See details at:

https://chocola.ens-lyon.fr/events/meeting-2023-11-16/

Certain properties of (type) dependencies in typed programming languages can be established syntactically by observing non-violation, shortcutting the need of a manual proof. Examples of such properties are variance, irrelevance, parametricity, or causality as in guarded type theory. A type system where function types are annotated with a *modality* expressing the function's behaviour, can account for this syntactic check as part of type-checking. From the need to type basic function operations, we find that these modalities should have the structure of an ordered monoid, or more generally they can be the morphisms of a 2-category whose objects are called *modes*. The purpose of multi[mode/modal] type theory (MTT) is to provide a type system, parametrized by a 2-category called the *mode theory* which abstractly achieves this result.

After introducing MTT and its models, depending on the timing and the interests and background of the audience, we can either look at questions arising during the implementation of MTT, or at applications. Some applications that I have worked on, or am working on, are Degrees of Relatedness (for parametricity & irrelevance), naturality type theory (naturality & variance), and the modal transpension system (for internalizing aspects of presheaf models). J. Ceulemans' Sikkel library for Agda explores how MTT can help to use the many extensions of type theory found in the literature *locally and modularly*.

L'Internet est un réseau consistant de plusieurs dizaines de milliards de nœuds. Le *routage* est le problème d'acheminer un paquet à travers un réseau. Le paradigme de routage utilisé dans l'Internet s'appelle le *routage next-hop*.

Dans cet exposé, je ferai une introduction au routage next-hop, puis je décrirai comment il est traditionnellement réalisé dans l'Internet. Je décrirai les faiblesses des techniques traditionnelles de routage, et je montrerai comment le protocole de routage Babel vise à les contourner.

Titles and abstracts available at: https://chocola.ens-lyon.fr/events/meeting-2023-09-28/

Metaprogramming is the art of writing programs that produce or manipulate other programs. This opens the possibility to eliminate boilerplate code and exploit domain-specific knowledge to build high-performance programs. While this widely used concept is almost as old as programming itself, it has been surprisingly challenging to extend to logical frameworks and type-theory in general.

In this talk, I present a layered modal type theory that provides a logical foundation to meta-programming with intensional code analysis. At its core (layer 0), has a pure (simply-typed) calculus with no modality. Layer 1 is obtained by extending the core with one layer of contextual box types which describes open code at layer 0 and supports pattern matching on open code from layer 0. Although both layers fundamentally share the same language and the same typing judgment, we only allow computation at layer 1. As a consequence, layer 0 accurately captures the syntactic representation of code in contrast to the computational behaviors at layer 1. The system is justified by normalization by evaluation (NbE) using a presheaf model. The normalization algorithm extracted from the model is sound and complete and is implemented in Agda.

We see this work as a stepping stone towards developing a dependent type theory that supports intensional code analysis in meta-programming.

This is joint work with Jason Z. Hu.

Barendregt's book “The Lambda Calculus, its syntax and semantics” (1981/84) has become a `classic' in Theoretical Computer Science because it presents the state of the art in lambda calculus in a comprehensive way, and proposes a number of open problems and conjectures. In 2022, Barendregt and Manzonetto published a `sequel' of this book, presenting the solutions of several of these problems, and more. In this talk, we will present a selection of these problems and the key ingredients that were employed to solve them.

Topology-based geometric modeling deals with the representation of nD objects, which splits the topological description, i.e., the representation of the objects' topological cells (vertices, edges, faces, volumes, …), and the geometric information, i.e., the addition of data to the topological cells. We study the combinatorial models of generalized and oriented maps represented as attributed typed graphs subject to consistency conditions. This representation allows the study of modeling operations as graph rewriting rules. The motivation is twofold. First, we study the preservation of the model consistency through syntactic conditions statically checked on the rules. Second, we extend rules into rule schemes to abstract over the underlying topology. This formalization of modeling operations also offers guidelines for inferring operations from a representative example consisting of an initial and a target object. The inference mechanism is implemented in Jerboa, a platform for designing geometric modelers exploiting graph transformation rules.

Milner's work on functions as processes shows how the evaluation strategies of the lambda-calculus can be faithfully mimicked in the pi-calculus, allowing a dynamic representation of functional programs. Milner namely studies the call-by-name and call-by-value evaluation strategies, and raises the problem of full abstraction for these encodings, i.e., what are the equivalences induced by these encodings. The theory of call-by-name is well-studied and understood, and the problem of full abstraction for call-by-name was solved shortly after. On the other hand, the theory of call-by-value on open terms is complex, and we present the solution of the full abstraction problem for call-by-value, which was left open until quite recently.

Algebraic operations, as defined by Plotkin and Power, are well-studied and powerful tools to provide denotational semantics for computational lambda-calculus and it is especially useful in design for abstraction of effectful computations, allowing a high degree of modularity by separating effect signatures from their interpretations. The practical counterpart of this is obtained by the use of handlers, a popular tool in functional programming that can actually provide concrete implementations of effect signatures while preserving modularity.

In this talk, I will present a joint work with Ugo Dal Lago and Francesco Gavazzo on how algebraic operations, and handlers, can support decision-making abstractions in functional programs: a user can invoke an operation to resolve choices without implementing the underlying selection mechanism, and can give feedback by way of rewards. We differ from some recently proposed approach to the problem based on the selection monad, by Abadi and Plotkin, as we express the underlying selection mechanism with efficient algorithms implemented by a set of handlers. I will first introduce algebraic effects and handlers, then present the selection monad approach for choices, and our approach, based on stateful computations (or equivalently comodels). Both the theoretical and practical aspects will be examined, and I will show the practical efficiency of our approach compared to the selection monad. Finally, I will focus on how our work can actually be implemented in a modular way on a concrete language with handlers and how we can use expressive type systems to obtain safety properties, especially ensuring a high-degree of modularity and a sound usage of algebraic operations.

Program execution rarely happens in isolation. Indeed, during its evaluation a program may modify the memory of the machine, interact with external processes, change the flow of the computation, etc. All these phenomena are known as computational effects, and they can be informally described as those side effects happening during the evaluation process of the program. Computational effects are of paramount importance to understand program behaviour, and indeed they are one of the main research topics in programming language semantics since the very birth of the discipline. Starting with the seminal work by Eugenio Moggi, computational effects have been successfully understood relying on the language of algebra and category theory, with notions such as monad, algebraic (and Lawvere) theory, and distributive law being nowadays well-accepted idioms in the programming language community. Although the categorical perspective on computational effects has been particularly effective to model the denotational semantics of effectful programs it does not work so well when it comes to accounting for their operational behaviour. In this talk, I will introduce the theory of computational effects by first reviewing the categorical approach to effectful programs, focusing in particular on Plotkin and Power's theory of algebraic effects, and then moving to computational effects in (some subfields of) operational reasoning. In particular, I will give evidence that by extending the aforementioned categorical notions from a categorical (functional) to an allegorical (relational) setting, it is possible to obtain an elegant operational theory of computational effects having the same level of generality as its denotational counterpart. To maintain the talk as accessible as possible, I will give a first introductory part on computational effects and then move to the more technical relational development. The latter will consist of a general high-level outline of the results achieved in the context of operational reasoning and of a more in-depth case study.

In this talk, we introduce two complete equational theories: one for linear optical circuits and one for quantum circuits. More precisely, in both cases we introduce a set of circuit equations that we prove to be sound and complete: two circuits represent the same quantum evolution if and only if they can be transformed one into the other using the equations.

We shall first present our proposed equational theory for linear optical circuits. We shall then discuss how the semantics of both kind of circuits differ, and how to relate them using controlled-gates. The discussion will drive is to the completeness result for quantum circuits, based on the one for linear optical circuits.

ML modules are offer large-scale notions of composition and modularity. Provided as an additional layer on top of the core language, they have proven both vital to the working OCaml and SML programmers, and inspiring to other use-cases and languages. Unfortunately, their meta-theory remains difficult to comprehend, and more recent extensions (abstract signatures, module aliases) lack a complete formalization. Building on a previous translation from ML modules to Fω, we propose a new comprehensive description of a significant subset of OCaml modules, including both applicative and generative functors and the proposed feature of transparent ascription. By exploring the translations both to and from Fω, we provide a complete description of the signature avoidance issue, as well as insights on the limitations and benefits of the path-based approach of OCaml type-sharing.

(Joint work with Almudena Colacito, Nikolaos Galatos, and Simon Santschi)

This talk will be about deciding equations in various classes of ordered groups and ordered monoids, and how this relates to deciding if there exist orders on free groups and monoids satisfying finitely many inequalities.

Removing the inverse operation from any lattice-ordered group (l-group) yields a distributive lattice-ordered monoid (l-monoid), but not every distributive l-monoid admits a group structure. Indeed, every distributive l-monoid is a (possibly finite) pointwise-ordered monoid of order-preserving maps on a chain, whereas every l-group is a pointwise-ordered group of order-preserving permutations on a chain and must be either trivial or infinite.

We will see that the equational theory of distributive l-monoids is decidable and coincides with the equational theory of l-groups without inverses, and hence, by eliminating inverses, that the equational theory of l-groups is also decidable. This contrasts with the fact that there are inverse-free equations that are satisfied by all totally ordered abelian groups but not all totally ordered commutative monoids, and the decidability of the equational theory of the latter is open.

Ehrhard and Regnier’s Taylor expansion of λ-terms has been broadly used as an approximation theory for several variants of the λ-calculus. Many results arise from a Commutation theorem relating the normal form of the Taylor expansion of a term to its Böhm tree. We extend this framework to the (001-)infinitary λ-calculus, where terms and reductions may be infinite, and where the normal forms are precisely the Böhm trees. This enables us to give a unified presentation of the Commutation theorem, thanks to the simulation of the infinitary reduction by the (finitary, confluent and terminating) reduction of the Taylor expansion. Finally we deduce new, simple proofs of confluence and genericity for the infinitary λ-calculus, as well as approximation-based characterisations of head- and β-reductions.

Corresponding paper (submitted to LMCS): https://arxiv.org/abs/2211.05608. This is joint work with my supervisor Lionel Vaux Auclair (I2M, AMU).

In the last years, there has been a growing interest in the notion of “distances/errors” between programs. A natural question is that of the relation between this point of view and the one provided by Ehrhrard and Regnier's Taylor expansion of lambda-terms, in which the role played by polynomials in analysis is played by so-called resource terms. One of the main motivations of this still very in progress work – joint with Paolo Pistone – is precisely to explore how can we relate these two worlds. For instance, a notable notion from the “metric perspective” is that of a program being K-Lipschitz; from the “differential perspective”, one may want resource terms to be Lipschitz, but then there is a mismatch with respect to analysis, because polynomials are not. Now, the well known “tropicalisation”, precisely transforms polynomials into Lipschitz functions. Tropical mathematics is a well-established field, in tight relation with algebraic geometry and optimisation; we explore some of its relations with lambda-calculus. In particular, we consider the category of sets and matrices with coefficients in the so-called tropical semifield. Endowed with certain bang and differential operators, it gives rise to a model of the differential lambda-calculus in which morphisms can be Taylor expanded and, seen as “infinite” tropical polynomials, satisfy certain continuity and Lipschitz properties. I will mention some possible applications in relation with probabilities and extracting quantitative information from programs. If time allows, I will mention how we are recognising that, actually, all this relates to some general research in quantales-enriched categories, and probably has an interesting relation with Ehrhard's finiteness spaces.

In this talk, I will start by discussing the lack of a reasonable time cost model for linear logic. Then, inspired by recent advances in the sister field of lambda calculus, I will introduce a new term-based presentation of cut elimination for IMELL admitting a reasonable strategy (that is, a strategy of which the number of step is a reasonable time cost model). The focus will be on the principles behind the new presentation of cut elimination.

The computationally complete symbolic attacker (CCSA) is a logically-based approach proposed by Bana and Comon to verify cryptographic protocols in the computational model, i.e. in the model of cryptographers where messages are probabilistic bitstrings and attackers are arbitrary probabilistic PTIME machines. The original formulation of CCSA was based on first-order logic and only supported the verification of protocols with bounded traces. With several co-authors, we have proposed in 2020 to build a meta-logic on top of this “base” first-order logic, to obtain a methodology that supports verifying unbounded protocols. This meta-logic forms the basis of the Squirrel proof assistant.

The study of computational complexity is based on computational models, traditionally Turing machines. Space complexity is defined as the maximum number of cells used during a computation. How could we measure the space complexity of functional programs? The notion of space is not clear as there is not a fixed evaluation schema. However, the cost model should be reasonable, i.e. linearly related with the one of Turing machines. In this talk, I will go through the journey that led to the definition of the first reasonable space cost model for the lambda-calculus, accounting for logarithmic space complexity.

This talks presents the Functional Machine Calculus (FMC) as a simple model of higher-order computation with effects, including higher-order mutable store, input and output, and probabilistic and non-deterministic computation as special cases of input. It consists of two independent generalizations of the lambda-calculus, derived from the standard opera- tional perspective of a call–by–name stack machine and supported by domain-theoretic considerations. One generalization, “locations”, enables effect operators to be encoded into the constructs of the calculus. The second, “sequencing”, is known from kappa-calculus and concate- native languages, and introduces the imperative notions of “skip” and “sequence”. This enables the encoding of reduction strategies, including call–by–value lambda-calculus and monadic constructs. Reduction in the FMC is confluent, which is possible be- cause encoded effect operations reduce algebraically, rather than operationally. It can be simply typed to confer strong normalization, and semantically forms a Cartesian closed category.

https://www.irif.fr/rencontres/rentree2022

Recent years have seen tremendous growth in the amount of verified software. Proofs for complex properties can now be achieved using higher-order theories and calculi. Complex properties lead to an ever-growing number of definitions and associated lemmas, which constitute an integral part of proof construction. Following this – whether automatic or semi-automatic – methods for computer-aided lemma discovery have emerged. In this work, we introduce a new symbolic technique for bottom-up lemma discovery, that is, the generation of a library of lemmas from a base set of inductive data types and recursive definitions. This is known as the theory exploration problem, and so far, solutions have been proposed based either on counter-example generation or the more prevalent random testing combined with first-order solvers. Our new approach, being purely deductive, eliminates the need for random testing as a filtering phase and for SMT solvers. Therefore it is amenable compositional reasoning and for the treatment of user-defined higher-order functions. Our implementation, TheSy, has shown to find more lemmas than prior art, while avoiding redundancy and without having to run the programs once.

In this talk, I will present results published in CAV 2021, and ongoing work on extending TheSy to richer theories. In the first work, we used e-graphs on top of egg (Willsey et al). In the follow-up, we extend egg to be able to handle conditional equalities, which are pervasive in many theories; notably, Separation Logic with inductive definitions. We hope that this will allow synthesizing a richer set of lemmas.

The Mathematical Foundations of Programming Semantics takes place in Ithaca, New York, with a local event hosted at IRIF. The talks of Daniela Petrisan, Alexandre Goy, Nicolas Munnich, Chris Barrett, and Willem Heijltjes will take place in room 3052. The talks from speakers in Ithaca will be broadcast in the same room.

See https://www.cs.cornell.edu/mfps-2022/paris.md.html for additional information.

The Mathematical Foundations of Programming Semantics takes place in Ithaca, New York, with a local event hosted at IRIF. The talk of Nicolas Wu will take place in room 3052 at 18:20. The talks from speakers in Ithaca will be broadcast in the same room.

See https://www.cs.cornell.edu/mfps-2022/paris.md.html for additional information.

The Mathematical Foundations of Programming Semantics takes place in Ithaca, New York, with a local event hosted at IRIF. The talks of Barbara König, Ayberk Tosun, and Frank Pfenning will take place in room 3052. The talks from speakers in Ithaca will be broadcast in the same room.

See https://www.cs.cornell.edu/mfps-2022/paris.md.html for additional information.

In asynchronous games, Melliès proved that innocent strategies are positional: their behaviour only depends on the position, not the temporal order used to reach it. This insightful result shaped our understanding of the link between dynamic (i.e. game) and static (i.e. relational) semantics. Here, we investigate the positionality of innocent strategies in the traditional setting of Hyland-Ong-Nickau-Coquand pointer games. Although innocent strategies are not positional, total finite innocent strategies still enjoy a key consequence of positionality, namely positional injectivity: they are entirely determined by their positions.

This talk is based on a article written with Pierre Clairambault (https://drops.dagstuhl.de/opus/volltexte/2021/14255).

One of the key aspects of mathematical logic and semantical techniques in theoretical computer science is to test the validity of a formula in structure. This can be a complex task, e.g. if the formula or the structure is complicated. In this talk, I will present a method for testing the validity of a statement of dependent type theory in categories of variable sets (presheaves). This involves a generalisation of the well-known Kripke semantics for intuitionistic logic and of the Kripke-Joyal semantics for higher-order intuitionistic logic. As an application, I will outline how this method can be used to relate type-theoretic and category-theoretic characterisations of so-called uniform fibrations, which have been used in Homotopy Type Theory. I will not assume prior knowledge of type theory or category theory. This is joint work with Steve Awodey (Carnegie Mellon University) and Sina Hazratpour (Johns Hopkins University), see https://arxiv.org/abs/2110.14576.

Logical relations are the main tool for proving positive properties of logics, type theories, and programming languages: canonicity, normalization, decidability, conservativity, computational adequacy, and more. Logical relations combine pure syntax with non-syntactic objects that are parameterized in syntax in a somewhat complex way; the sophistication of possible parameterizations makes logical relations a tool that is primarily accessible to specialists. In the spirit of Halmos' book Naïve Set Theory, I advocate for a new viewpoint on logical relations based on synthetic Tait computability, the internal language of categories of logical relations. In synthetic Tait computability, logical relations are manipulated as if they were sets, making the essence of many complex logical relations arguments accessible to non-specialists.

In this talk I will discuss the recent progress in learning methods for theorem proving. In many domains, representations that are able to abstract over unimportant transformations, such as abstraction over translations and rotations in vision are becoming more common. Standard methods of interpreting formulas for learning theorem proving are however yet unable to handle many important transformations. In particular, embedding previously unseen labels, that often arise in definitional encodings and in Skolemization, has been very weak so far. Similar problems appear when transferring knowledge between known symbols. I will discuss encoding of formulas based on graph models, that represents symbols only by nodes in the graph, without any knowledge of the original labels. I will discuss this in multiple theorem proving tasks, including lemma selection, reasoning, and interaction with an ITP.

The talk bridges between two major paradigms in computation, the functional, at basis computation from input to output, and the interactive, where computation reacts to its environment while underway. Central to any compositional theory of interaction is the dichotomy between a system and its environment. Concurrent games and strategies address the dichotomy in fine detail, very locally, in a distributed fashion, through distinctions between Player moves (events of the system) and Opponent moves (those of the environment). A functional approach has to handle the dichotomy much more ingeniously, through its blunter distinction between input and output. This has led to a variety of functional approaches, specialised to particular interactive demands. Through concurrent games we can more clearly see what separates and connects the differing paradigms, and show how:

- several paradigms of functional programming and logic arise naturally as subcategories of concurrent games, including stable domain theory; nondeterministic dataflow; geometry of interaction; the dialectica interpretation; lenses and optics; and their extensions to containers in dependent lenses and optics.

- to transfer enrichments of strategies (such as to probabilistic, quantum or real-number computation) to functional settings.

“Program sensitivity” measures the distance between the outputs of a program when it is run on two related inputs. This notion, which plays an important role in areas such as differential privacy and optimization, has been the focus of several program analysis techniques introduced in recent years. One approach that has proved particularly fruitful for this domain is the use of type systems inspired by linear logic, as pioneered by Reed and Pierce in the Fuzz programming language. In Fuzz, each type is equipped with its own notion of distance, and the typing rules explain how those distances can be treated soundly when analyzing the sensitivity of a program. In particular, Fuzz features two products types, corresponding to two different sensitivity analyses: the “tensor product” combines the distances of each component by adding them, while the “with product” takes their maximum. In this talk we will show how products in Fuzz can be generalized to arbitrary Lp distances, metrics that are often used in privacy and optimization. The original Fuzz products, tensor and with, correspond to the special cases L1 and L∞. To handle the generalized products, we extend the Fuzz type system with bunches – as in the logic of bunched implications – where the distances of different groups of variables can be combined using different Lp distances. We show that our extension, Bunched Fuzz, can be used to reason about important examples of metrics between probability distributions in a natural way.

This is joint work with june wunder, Arthur Azevedo de Amorim, and Marco Gaboardi.

I will present a further step in my ongoing research programme on Algebraic Type Theory, the overall aim of which is to develop a mathematical theory understanding type theories algebraically while supporting practical foundations. The talk will centre on Second-Order Algebraic Theories, which are equational presentations in languages with (first-order) algebraic type structure and (second-order) term structure with variable-binding operators and parametrised metavariables. Examples include: first-order logic, simply-typed computational calculi, and the calculus of partial differentiation.

Specifically, I will present a new categorical model for Second-Order Algebraic Theories: it is based on indexed families and founded upon the initial-algebra approach. A main motivation for and crucial aspect of the mathematical theory is that it is directly programmable in languages supporting inductive families; and, indeed, was developed in unison with building a formally-verified computer implementation for second-order semantics, computation, and deduction. As such, the work resulted in a framework within the Agda proof assistant for the automatic generation of generic second-order abstract syntax and provably-correct metaoperations for manipulating it; to wit, algebraic models together with compositional interpretations, capture-avoiding and metavariable substitution operations, and equational and/or rewriting reasoning. This is joint work with Dmitrij Szamozvancev; a paper, source code, documentation, and case studies are available at the project page <tinyurl.com/agda-soas>.

Clones are sets of finitary operations on a fixed carrier set that contain all projection operations and are closed under composition. They play an important role in universal algebra (the term clone of an algebra), in the study of first-order structures (the polymorphism clone of a structure), and in theoretical computer science (the polymorphism clone of a constraint satisfaction problem). In this talk we introduce a new general framework for algebras and clones, called universal clone algebra. Algebras and clones of finitary operations are to universal algebra what t-algebras and clone algebras are to universal clone algebra. Clone algebras found a one-sorted, purely algebraic theory of clones, while t-algebras are a slight generalisation of algebras to cope with infinite arities. We present a method to codify algebras and clones into t-algebras and clone algebras, respectively. We provide concrete examples showing that general results in universal clone algebra, when translated in terms of algebras and clones, give new versions of known theorems in universal algebra. We apply this methodology to Birkhoff's HSP theorem and to the recent topological versions of Birkhoff's theorem.

Realizability aims at extracting the computational content of mathematical proofs. Introduced in 1945 by Kleene as part of a broader program in constructive mathematics, realizability has later evolved to include classical logic and even set theory. Krivine's work led to define realizability models for the theory ZF following a technique that generalizes the method of Forcing. After a brief presentation of this technique, we will discuss the problem of representing ordinals in realizability models for set theory, thus we will present the solution proposed in a joint work with Guillaume Geoffroy that led to realize uncountable versions of the Axiom of Dependent Choice.

In this talk, I will introduce a multi-token machine for Idealized Parallel Algol (IPA), a higher-order concurrent programming language with shared state and semaphores. For the purely functional fragment, the machine is conceptually close to Geometry of Interaction token machines, originating from Linear Logic and presenting higher-order computation as the low-level process of a token walking through a graph (a proof net) representing the term. However, our methodology is somewhat different: instead of representing terms as proof nets, the machine takes the shape of a compositional interpretation of terms as “Petri structures”, certain coloured Petri nets. Formalizing the token machine as a Petri net allows us to pair GoI with folklore ideas on the representation of first-order imperative concurrent programs as coloured Petri nets.

To prove our machine correct, we follow game semantics and represent types as certain games specifying dependencies and conflict between computational events. We define Petri strategies as those Petri structures obeying the rules of the game. In turn, we show how Petri strategies unfold to concurrent strategies in the sense of concurrent games on event structures. This not only entails correctness and adequacy of our machine, but also lets us generate operationally a causal description of the behaviour of programs at higher-order types.

This is joint work with Simon Castellan. The Geometry of Causality machine is implemented, and available at: https://ipatopetrinets.github.io/

http://chocola.ens-lyon.fr/events/

In this talk we define logical systems where graphs play the role of formulas. We recall the well-known correspondence between propositional formulas and cographs, a specific family of graphs satisfying simple topological conditions, and we introduce a proof system for a logic generalising this correspondence to general undirected graphs. We show that the proof system satisfies some basic requirements, most notably analyticity. We conclude by outlining the novelty in this approach and the research directions which it opens.

In call-by-value languages, some mutually-recursive value definitions can be safely evaluated to build recursive functions or cyclic data structures, but some definitions (`let rec x = x + 1`) contain vicious circles and their evaluation fails at runtime. We propose a new static analysis to check the absence of such runtime failures.

Our analysis is described by a set of declarative inference rules that can be “directed” into an algorithmic check. Our implementation of this check replaced the existing check used by the OCaml programming language, a fragile syntactic/grammatical criterion which let several subtle bugs slip through as the language kept evolving.

http://chocola.ens-lyon.fr/events/

This talk is about an exploration of a mathematical logician into a taboo in modern mathematics : the veracity of our proofs. It is not a formal proof talk and not even a foundations of mathematics one, but it rather gives a perspective of where we stand in mathematics with respect to how much we can trust our own doing, and how we could perhaps improve it. Or if it is really possible to improve. The talk is an adaptation of an invited address I gave at the conference « 90 years after Gödel’s Incompleteness Theorem » (July 202, Tübingen, Germany).

Rust is a fairly recent programming language for system programming, bringing static guarantees of memory safety through a strong ownership policy. This feature opens promising advances for deductive verification, which aims at proving the conformity of Rust code with respect to a specification of its intended behavior.

We present Creusot, a tool for the formal specification and deductive verification of Rust. Creusot's specification language features a notion of prophecies to reason about memory mutation. Rust provides advanced abstraction features based on a notion of traits, extensively used in the standard library and in user code. The support for traits is at the heart of Creusot's approach of verification and specification of programs.

In the same way we have streams of bits and stream transformer, we can define streams of qubits and qubit stream transformers. I will present an extension of quantum circuits with quantum memories to represent stream tranfsormers. We provide a set of rewriting rule and a coinduction principle that can extend any complete set of rules for cirucits to a complete set of rule for stream transformer. Thus, any two observationaly equivalent stream transformers can be proven equivalent using our rewriting rules. I will also expose ongoing works on the denotational semantics of stream transformers and extension to the post selectioned case.

Functional interpretations are maps of formulas from the language of one theory into the language of another theory, in such a way that provability is preserved. These interpretations typically replace logical relations by functional relations. Functional interpretations have many uses, such as relative consistency results, conservation results, and extraction of computational content from proofs as is the case in the so-called proof mining program.

I will present several recent functional interpretations and some results that come from these interpretations. I will also give examples of application of functional interpretations, in the spirit of the proof mining program.

Probabilistic programming is the idea of writing models from statistics and machine learning using program notations and reasoning about these models using generic inference engines. Recently its combination with deep learning has been explored intensely, which led to the development of so called deep probabilistic programming languages, such as Pyro, Edward and ProbTorch. At the core of this development lie inference engines based on stochastic variational inference algorithms. When asked to find information about the posterior distribution of a model written in such a language, these algorithms convert this posterior-inference query into an optimisation problem and solve it approximately by a form of gradient ascent or descent.

In this talk, we analyse one of the most fundamental and versatile variational inference algorithms, called score estimator or REINFORCE, using tools from denotational semantics and program analysis. We formally express what this algorithm does on models denoted by programs, and expose implicit assumptions made by the algorithm on the models. The violation of these assumptions may lead to an undefined optimisation objective or the loss of convergence guarantee of the optimisation process. We then describe rules for proving these assumptions, which can be automated by static program analyses. Some of our rules use nontrivial facts from continuous mathematics, and let us replace requirements about integrals in the assumptions, such as integrability of functions defined in terms of programs' denotations, by conditions involving differentiation or boundedness, which are much easier to prove automatically (and manually). Following our general methodology, we have developed a static program analysis for the Pyro programming language that aims at discharging the assumption about what we call model-guide support match. Our analysis is applied to eight representative model-guide pairs from the Pyro webpage, which include sophisticated neural network models such as AIR. It finds a bug in one of these cases, reveals a non-standard use of an inference engine in another, and shows that the assumptions are met in the remaining six cases.

(Joint work with Wonyeol Lee, Hangyeol Yu, and Hongseok Yang, KAIST)

Contextual equivalence is a relation over program expressions which guarantees that related expressions are interchangeable in any program context. It encompasses verification properties like safety and termination, has attracted considerable attention from the semantics community, and has found its main applications in the verification of cryptographic protocols, compiler correctness and regression verification.

In this talk we present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations similar to symbolic game semantics, up-to techniques, and lightweight state invariant annotations. This yields an equivalence verification technique with no false positives or negatives. The technique is bounded-complete, in that all inequivalences are automatically detected given large enough bounds. Moreover, several hard equivalences are proved automatically or after being annotated with state invariants. We have realised the technique in a tool prototype called Hobbit and benchmarked it with an extensive set of new and existing examples. Hobbit can prove many classical equivalences including all Meyer and Sieber examples.

Epistemic Logic is the modal logic of knowledge. It allows to reason about a finite set of agents who can know facts about the world, and about what the other agents know. The traditional Kripke-style semantics for epistemic logic is based on graphs whose vertices represent the possible worlds, and whose edges indicate the agents that cannot distinguish between two worlds. In this talk, I will present an alternative semantics for epistemic logic, based on combinatorial topology. The idea is to replace the Kripke graph by a simplicial complex, allowing for higher-dimensional connectivity between the possible worlds. In fact, every Kripke model can be turned into an equivalent simplicial model, thus uncovering its underlying topological information.

This is joint work with Éric Goubault and Sergio Rajsbaum

Necula (PLDI'2000) and Tristan, Gouvereau, Morrisett (PLDI'2011) established that symbolic execution combined with rewriting is effective in validating the code produced by state-of-the-art compilers applying various optimizations. In the meantime, Tristan and Leroy (POPL'2008) used formally-verified symbolic execution to certify the schedules produced by untrusted oracles – optimizing pipeline usage – within the CompCert compiler. Alas, their formally-verified checker had exponential complexity and was thus never integrated into mainline CompCert.

With Cyril Six and David Monniaux, we solved this performance issue with formally verified hash-consing within the symbolic execution. And we successfully applied this technique to implement within CompCert effective optimizations targeting superscalar (or VLIW) in-order processors.

The talk will actually start by briefly introducing a sound Foreign Function Interface for embedding OCaml oracles within Coq. Hence, it will explain how we used it in this application.

Law at large underpins modern society, codifying and governing many aspects of citizens' daily lives. Oftentimes, law is subject to interpretation, debate and challenges throughout various courts and jurisdictions. But in some other areas, law leaves little room for interpretation, and essentially aims to rigorously describe a computation, a decision procedure or, simply said, an algorithm. Unfortunately, prose remains a woefully inadequate tool for the job. The lack of formalism leaves room for ambiguities; the structure of legal statutes, with many paragraphs and sub-sections spread across multiple pages, makes it hard to compute the intended outcome of the algorithm underlying a given text; and, as with any other piece of poorly-specified critical software, the use of informal language leaves corner cases unaddressed. We introduce Catala, a new programming language that we specifically designed to allow a straightforward and systematic translation of statutory law into an executable implementation. Catala aims to bring together lawyers and programmers through a shared medium, which together they can understand, edit and evolve, bridging a gap that often results in dramatically incorrect implementations of the law. We have implemented a compiler for Catala, and have proven the correctness of its core compilation steps using the F* proof assistant. We evaluate Catala on several legal texts that are algorithms in disguise, notably section 121 of the US federal income tax and the byzantine French family benefits; in doing so, we uncover a bug in the official implementation. We observe as a consequence of the formalization process that using Catala enables rich interactions between lawyers and programmers, leading to a greater understanding of the original legislative intent, while producing a correct-by-construction executable specification reusable by the greater software ecosystem.

Modern software increasingly exploits parallelism to reach new heights of performance. Unfortunately, concurrent programming is error-prone, and developers often make incorrect assumptions about how their programs will behave, raising concerns about its use in critical systems. Using formal methods to provide strong correctness guarantees is appealing, but challenging; verification frameworks either lack the expressivity required to model every advanced low-level pattern found in real-world implementations, or they do not retain the level of automation needed to ensure the scalability of verification. To address this issue, we present Steel, a new verification framework to develop and prove concurrent programs embedded in F*, a dependently typed programming language and proof assistant.

In this talk, we give an overview of Steel from the ground up. To reason about programs, Steel provides a higher-order, impredicative concurrent separation logic with support for dynamically-allocated invariants and partial commutative monoids (PCMs). To automate verification, Steel separates verification conditions between separation logic predicates and first-order logic encodeable predicates; we develop a (partial) decision procedure using efficient, reflective tactics that focuses on the former, while the latter can be encoded efficiently to SMT by F*. We will conclude by presenting several verified Steel libraries, including mutable, self-balancing trees as well as a novel PCM-based encoding of 2-party dependently typed sessions, that illustrate the expressiveness and programmability of Steel.

The chef kicks them out: “I'm sorry, in my kitchen we only use induction”

This talk will start from Morris' PhD thesis in 1968 and present 50 years of theoretical computer science, through PCF, CCS, Alternating transition systems, contexts and strategies, ending up at the footsteps of the monumental Palace of Justice in Créteil.

Informally, “constructivism” is a programme of mathematics aiming to ensure that anything asserted to exist must be explicitly constructed. It is generally practiced using intuitionistic logic, which achieves this by rejecting the law of excluded middle. However, the same result is also achieved by Girard's linear logic, which instead restricts the number of times each hypothesis can be used in a proof; but essentially no practicing constructivists today use linear logic.

I will show that intuitionistic and linear approaches to constructive mathematics are intimately connected, through an interpretation of linear logic (or more precisely, affine logic) into intuitionistic logic based on a categorical Chu/Dialectica construction called the “antithesis translation”. In particular, many odd features of intuitionistic mathematics, such as inequality relations, anti-subgroups, and apartness spaces, arise automatically and unavoidably by translating natural definitions from affine logic across this interpretation. Thus, affine logic can be used as a “high-level tool” for intuitionistic mathematics, helping to find the right definitions and manage the bookkeeping of formally dual properties in proofs.

Focusing is a general technique for syntactically compartmentalising the non-deterministic choices in a proof system, which not only improves proof search but also has the representational benefit of distilling sequent proofs into synthetic normal forms. However, since focusing was traditionally specified as a restriction of the sequent calculus, the technique had not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some modal or substructural logics.

With K. Chaudhuri and L. Straßburger, we extended the focusing technique to nested sequents, a generalisation of ordinary sequents which allows us to capture all the logics of the classical and intuitionistic S5 cube in a modular fashion. This relied, following the method introduced by O. Laurent, on an adequate polarisation of the syntax and an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.

Recently, with A. Gheorghiu, we applied a similar method to the logic of Bunched Implications (BI), a logic that freely combines intuitionistic logic and multiplicative linear logic. For this we had first to reformulate the traditional bunched calculus for BI using nested sequents, followed by a polarised and focused variant that (again) we show is sound and complete via a cut-elimination argument.

Game semantics is the art of interpreting formulas (or types) as games and proofs (or programs) as strategies. In order to reflect the interactive behaviour of programs, strategies are required to follow specific scheduling policies. Typically, in the case of a sequential programming language, the program (Player) and its environment (Opponent) play one after the other, in a strictly alternating way. On the other hand, in the case of a concurrent language, Player and Opponent are allowed to play several moves in a row, in a non alternating way. In the two cases, the scheduling policy is designed very carefully in order to ensure that the strategies synchronise properly and compose well when plugged together. A longstanding conceptual problem has been to understand when and why a given scheduling policy works and is compositional in that sense. In this talk, I will introduce the notion of template game and exhibit a number of simple and fundamental combinatorial properties which ensure that a given scheduling policy defines (indeed) a monoidal closed bicategory of games, strategies and simulations. The notion of template game will be illustrated by constructing two game models of linear logic with different flavours (alternating and asynchronous) using the same categorical combinatorics, performed in the category of small 2-categories.

The interested reader will find more material here https://www.irif.fr/~mellies/template-games.html https://www.youtube.com/watch?v=ZC2jtq2R3cw and in the companion papers [1,2,3].

[1] PAM. Categorical combinatorics of scheduling and synchronization in game semantics. Proceedings of POPL 2019. https://www.irif.fr/~mellies/papers/Mellies19popl.pdf https://www.irif.fr/~mellies/slides/popl-slides-january-2019.pdf

[2] PAM. Template games and differential linear logic. Proceedings of LICS 2019. https://www.irif.fr/~mellies/template-games/2-template-games-and-differential-linear-logic.pdf

[3] PAM. Asynchronous template games and the Gray tensor product of 2-categories. Proceedings of LICS 2021. https://www.irif.fr/~mellies/papers/asynchronous-template-games.pdf

[4] PAM. Une étude micrologique de la négation https://www.irif.fr/~mellies/hdr-mellies.pdf

In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. In the dependently-typed setting, however, we would like to appeal to such invariance results within a language itself, in order to transfer theorems from simple to complex implementations. Homotopy type theorists have noted that Voevodsky's univalence principle equates isomorphic structures, but unfortunately many instances of representation independence are not isomorphisms.

In this talk, we describe a technique for establishing internal relational representation independence results in Cubical Agda by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. Joint work with Evan Cavallo, Anders Mörtberg, and Max Zeuner. Available at https://dl.acm.org/doi/10.1145/3434293.

Static analysis aims at discovering semantic properties of software prior to execution. Examples of emantic properties of interest include the absence of some classes of errors, the invariance of certain classes of numerical properties, or the preservation of the shape of unbounded data-structures. While many static analyses proceed by computing an over-approximation of the set of reachable states of a program, it is also possible to seek for an abstraction of the input/output relation of programs. The former is often sufficient to answer questions such as “may my program crash ?”, but the former opens up several interesting roads. First it allows to prove certain classes of functional correctness properties. Second, it makes it possible to reuse the analysis for a given program fragment (typically a function), and to speed up the overall analysis process. We call such analyses relational. However, relational analyses need to manipulate abstractions of state relations. Tables of pairs or abstract pre- and post-conditions are often used. In this talk, we present an abstraction that is based on logical connectors that are designed specifically to capture relations. We present the abstrction, analysis algorithms and examples.

(Joint work with Hugo Illous and Matthieu Lemerre.)

Monads and their presentations via equational theories provide a tool for reasoning about programs with computational effects. In recent works, we have studied monads resulting from the combination of nondeterminism, probabilities, and termination, as well as their extensions to the category of metric spaces. In this talk, we'll introduce this framework and show applications to proving equivalences and distances of nondeterministic and probabilistic systems.

Bibliography:

Bonchi, Sokolova, Vignudelli. The theory of traces for systems with nondeterminism and probabilities. LICS 2019. Available at: https://arxiv.org/abs/1808.00923

Mio, Vignudelli. Monads and quantitative equational theories for nondeterminism and probabilities. CONCUR 2020. Available at: https://arxiv.org/abs/2005.07509

Mio, Sarkis, Vignudelli. Combining nondeterminism, probability, and termination: equational and metric reasoning. LICS 2021. Available at: https://arxiv.org/abs/2012.00382

Knaster-Tarski's theorem, characterising the greatest fixpoint of a monotone function over a complete lattice as the largest post-fixpoint, naturally leads to the so-called coinduction proof principle for showing that some element is below the greatest fixpoint (e.g., for providing bisimilarity witnesses). The dual principle, used for showing that an element is above the least fixpoint, is related to inductive invariants. This talks considers proof rules which are similar in spirit but for showing that an element is above the greatest fixpoint or, dually, below the least fixpoint.

The theory is developed for non-expansive monotone functions on suitable lattices of the form M^Y, where Y is a finite set and M an MV-algebra, and it is based on the construction of (finitary) approximations of the original functions. We show that our theory applies to a wide range of examples, including termination probabilities, behavioural distances for probabilistic automata and bisimilarity. Moreover it allows us to determine original algorithms for solving simple stochastic games.

The work to be presented is in collaboration with Pierre-Évariste Dagand and Lionel Rieg. It studies the computational content of the Fundamental Lemma of classical realizability for the simply-typed lambda-calculus with sums.

(If you are unfamiliar with classical realizability, it might help to think of it as a unary logical relation with an elegant symmetric setup – it originates in studies of classical logic. The talk will gently introduce classical realizability.)

Two salient points of our presentation correspond to folklore ideas that we present as opinionated recommandations, to ourselves and others, of how to give a “modern” presentation of these questions (classical realizability, and in general studying the computational content of a proof device):

1. We present classical realizablity as compilation to Curien-Herbelin style symmetric abstract machine calculi, instead of the Krivine Abstract Machine, to represent realizers. Experts will recognize the polarized reduction rules of Munch-Maccagnoni.

2. To present computation content, we are *not* using extraction of a program from a mathematical-style proof in a proof assistant. That beautiful approach rarely works and it generates ugly code. Instead we *write* the logical argument directly as a program in a dependently-typed (meta)language, and we think about the code we are writing.

Girard's Geometry of Interaction (GOI) can be made concrete by considering it as an implementation technique for functional programs, in particular the lambda calculus. Our work is about the complexity analysis of the abstract machine based on the GOI, the interaction abstract machine (IAM). We have adapted in a non trivial way de Carvalho's non idempotent intersection types so that type derivations completely characterize the time and space complexity of the IAM, thus providing a logical account of the IAM resource usage. Moreover, by the way of the type systems we have introduced, we are able to state some negative results about time and space cost models for the lambda calculus based on the IAM. This is joint work with Beniamino Accattoli and Ugo Dal Lago.

Transiently-powered systems featuring non-volatile memory as well as external peripherals enable the development of new low-power sensor applications. However, as programmers, we are ill-equipped to reason about systems where power failures are the norm rather than the exception. A first challenge consists in being able to capture all the volatile state of the application –external peripherals included– to ensure progress. A second, more fundamental, challenge consists in specifying how power failures may interact with peripheral operations. In a joint work with Rémi Oudin, Delphine Demange, Gautier Berthou and Tanguy Risset, we have proposed a formal specification of intermittent computing with peripherals, an axiomatic model of interrupt-based checkpointing as well as its proof of correctness, machine-checked in the Coq proof assistant. However, this result assumes that the system is able to maintain a shadow copy of the external devices it interacts with. Perhaps surprisingly, this could be an opportunity to adopt an algebraic treatment of external peripherals.

https://www.irif.fr/rencontres/pps2021/index

https://www.irif.fr/rencontres/pps2021/index

The subject of the SMTCoq project is to significantly enhance automation in the Coq proof assistant. At the heart of SMTCoq is a Coq plugin that offers a way to use automatic provers with the same degree of trust as Coq itself. On top of it, we define a framework to progressively encode Coq's logic into first-order logic, through modular and fine-grained logical transformations that can be composed. Our objective is to obtain automatic while expressive tactics for Coq.

In this talk, I will concisely introduce the communication between Coq and external provers, before presenting the new framework of logical transformations. I will report on work in progress of examples of transformations in this framework.

This is joint work with Valentin Blot, Louise Dubois de Prisque and Pierre Vial.

https://www.irif.fr/rencontres/pps2021/index

https://www.irif.fr/rencontres/pps2021/index

Ce travail est un travail commun avec Sylvie Boldo, François Clément Florian Faissole et Vincent Martin dans le cadre du projet DIM-RFSI MILC. La résolution des équations aux dérivées partielles (EDP) est au cœur de nombreux programmes de simulation dans l'industrie et la méthode des éléments finis (MEF) est un outil très utilisé pour leur résolution numérique.

Je présenterai le but à long terme dans lequel s'inscrit ce travail, domaine de la sécurité, de la fiabilité et de la sûreté. Il s'agit de poser les fondements qui nous permettront de prouver la correction d'une bibliothèque implantant la MEF en C++, telle que FELiScE (Finite Elements for Life Sciences and Engineering). Sa vérification formelle augmentera la confiance dans tous les codes qui l'utilisent. Ces travaux sont interdisciplinaires (logique/preuve de programmes/analyse numérique). Ces preuves reposent entre autres sur les bases mathématiques telles que la théorie de la mesure, l'intégrale de Lebesgue, les distributions, les espaces de Sobolev jusqu'à la construction de l'espace fonctionnel L2. Dans cet exposé je m'attarderai sur la formalisation de l'intégrale de Lebesgue pour les fonctions positives.

Monitorability underpins the technique of Runtime Verification because it delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the operational guarantees provided by monitors, i.e., the computational entities carrying out the verification. This work views monitorability as a spectrum, where the fewer guarantees that are required of monitors, the more properties become monitorable. Accordingly, I present a monitorability hierarchy based on this trade-off. For regular specifications, I give syntactic characterisations in Hennessy–Milner logic with recursion for its levels. Finally, I map existing monitorability definitions into our hierarchy. This gives a unified framework that makes the operational assumptions and guarantees of each definition explicit and provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools.

This is joint work with Luca Aceto, Antonis Achilleos, Anna Ingolfsdottir and Karoliina Lehtinen

We start by presenting a local system for linear logic (LL) based on linear nested sequents. 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.

We then move to the question of giving an interpretation to subexponentials. We will show a game interpretation of affine linear logic with subexponentials, viewing the game as a playground for illuminating semantic intuitions underlying resource conscious reasoning. Interestingly enough, this led to the proposal of new sequent systems for capturing the notions of costs and budget in a fragment of linear logic with subexponentials, thus opening new possibilities for analysing the problem of comparing proofs.

We finish the talk by showing a computational interpretation of subexponentials in the process-as-formula fashion, where process constructors are mapped to logical connectives and computational steps are related to proof steps. In particular, we will show in detail the role of pre-orders in subexponentials for the adequate specification of different modalities in concurrent systems, such as time, space, epistemic and preferences. We end with a discussion about which new models of computation should arise from the extension of the concept of modality in linear logic.

Some interactions between combinatorics and universal algebra through rewrite systems and clone theory are presented. Given a variety $V$ of algebras (presented by generating operations and relations between some of their compositions), a natural question consists in building a combinatorial realization of $V$. This consists in encoding the operations of $V$ in such a way that two equivalent ones have the same representation, and in providing an algorithm to compute the representation of the functional composition of several operations. In particular, we present a class of clones obtained from monoids. This gives rise among other to realizations of varieties of various classes of semigroups (commutative, left/right-regular bands, semilattices, etc.).

Les omega-catégories faibles, comme toutes les structures supérieures, sont délicates a définir et a manipuler. La raison est qu'elles ont de la structure dans toutes les dimensions, et que cette structure est cohérente: pour chaque dimension, les bonnes propriétés vérifiées par la structure dans cette dimension sont encodées par des éléments de dimension supérieure. La conséquence est qu'au fur et à mesure que l'on monte en dimension, les éléments présents deviennent de plus en plus riches et complexes a décrire. Ainsi, les définitions possibles de ces structures s'appuient sur des schémas d'axiomes, permettant de générer l'infinité d'opérations et de cohérences en toute dimensions, et ces schémas d'axiomes sont eux-mêmes encodés dans des structures algébriques adéquates, comme une opérade globulaire (définition due a Batanin et Leinster) ou une catégorie avec certaines colimites (définition due a Grothendieck et Maltsiniotis). Plus récemment, Finster et Mimram ont proposé une définition des omega-catégories faibles en encodant ces schémas d'axiomes dans une théorie des types, CaTT. Dans cet exposé, je vais présenter la theorie CaTT et m'appuyer sur cette formulation pour présenter formellement les omega-categories faibles. Je vais ensuite faire une démonstration d'un assistant de preuve pour les oméga-categories faibles que j'ai implementé en m'appuyant sur cette théorie des types et discuter des possibilités de cet outil, ainsi que des améliorations que j'y ai apportées. Je vais finalement esquisser une comparaison entre CaTT et la définition de Grothendieck-Maltsiniotis des omega-catégories faibles.

We introduce probabilistic analysis techniques for the testing of programs based on concurrent models. During this talk we study the notion of process synchronization from the point of view of combinatorics. As a first step, we address the quantitative problem of counting the number of executions of simple processes interacting with synchronization barriers. We elaborate a systematic decomposition of processes that produces a symbolic integral formula to solve the problem. Based on this procedure, we develop a generic algorithm to generate process executions uniformly at random. For some interesting sub-classes of processes we propose very efficient counting and random sampling algorithms. All these algorithms have one important characteristic in common: they work on the control graph of processes and thus do not require the explicit construction of the state-space. By consequence, we thus completely avoid the classical combinatorial explosion induced by such processes.

We provide an overview of the techniques developed and results obtained in the field of Implicit Computational Complexity, which aims at providing machine-independent or PL-based characterizations of complexity classes. After discussing some related results on “infinite data” (streams, real numbers, functions, …), we present a new tractable characterization of the class of Basic Feasible Functionals (BFF), known to be the class of second order functions computable in polynomial time. The corresponding programs consist of simply-typed terms that can call strongly normalizing imperative procedures following a tier-based type discipline.

We propose a systematic approach to approximate the behavior of models of polymers with synthesis and degradation. Our technique consists in discovering time-dependent lower and upper bounds for the concentration of some quantities of interest. These bounds are obtained by approximating the state of the system by a hyper-box,. The evolution of the position of each hyper-face is defined by the means of differential equations which are obtained by pessimistically bounding the derivative with respect to the corresponding coordinate on this hyper-face.

The over-approximation of each derivative relies on symbolic reasoning. We use Kappa to describe our models. Kappa is a site-graph rewriting languages which is popular to describe protein-protein interaction networks. The main ingredients of Kappa, graph patterns, can be interpreted in two ways. Intensionally by the means of embeddings between graphs, or extensionally as the (potentially infinite) multi-sets of the complete graphs they occur in. This second interpretation leads to the definition of positive series of concentration of species. Interestingly, it can be proven that some universal constructions between graphs induce generic methods to prove the well-posedness of some numerical series, and some equality and inequality among them, hence providing a convenient tool-kit for symbolic reasoning

One of the differences between Brouwerian intuitionistic logic and classical logic is their treatment of time. In classical logic truth is atemporal, whereas in intuitionistic logic it is time-relative. Thus, in intuitionistic logic it is possible to acquire new knowledge as time progresses, whereas the classical Law of Excluded Middle (LEM) is essentially flattening the notion of time stating that it is possible to decide whether or not some knowledge will ever be acquired. This paper demonstrates that, nonetheless, the two approaches are not necessarily incompatible by introducing an intuitionistic type theory along with a Beth-like model for it that provide some middle ground. On one hand they incorporate a notion of progressing time and include evolving mathematical entities in the form of choice sequences, and on the other hand they are consistent with a variant of the classical LEM. Accordingly, this new type theory provides the basis for a more classically inclined Brouwerian intuitionistic type theory.

Proving the absence of bugs in a given piece of software (a problem which has been known to be intrinsically hard since Turing and Cook) is not the only challenge in software development. Indeed, the ever growing complexity of software increases the need for more trustable optimisations. Solving these two problems (reliability, optimisation) implies the development of safe (without false negative answers) and efficient (wrt memory and time) analyses, yet precise enough (with few false positive answers).

In this talk I will present two experiences in the design of static analyses dedicated to array properties and explore the intrinsic difficulties we, together with my coauthors, faced while developing them. I will also show some experimental evidence of the impact of this work on real-world compilers, as well as future perspective for this area of research.

Research in the field of programming languages traditionally relies on a definition of syntax modulo renaming of bound variables, with its associated operational semantics. We are interested in mathematical tools allowing us to automatically generate syntax and semantics from basic data. We pay particular attention to the notion of substitution, using the categorical notions of monads and modules over them. Languages with variable binding, such as the pure lambda calculus, are monads on the category of sets. We provide a further notion of transition monads which takes into account the operational semantics. We give examples of specifications for transition monads, in the spirit of Initial Semantics, where an object is characterized by some initiality property in a suitable category of models.

From a programmer's perspective, quantum algorithms are simply classical algorithms having access a special kind of memory featuring particular operations: quantum operations. They therefore feature two kinds of control flow. One is purely conventional and is concerned in the classical part of the algorithm. The other – dubbed quantum control – is more elusive and still subject to debate: if the notion of quantum test is reasonably consensual, the quantum counterpart of loops is still not believed to be meaningful.

In this talk, we argue that, under the right circumstances, a reasonable notion of quantum loop is possible. To this aim, we propose a typed, reversible language with lists and fixpoints, extensible to linear combinations of terms. The language admits a reduction strategy in the spirit of algebraic lambda-calculi. Under the restriction of structurally recursive fixpoints, it is shown to capture unitary operations. It is expressive enough to represent several of the unitaries one might be interested in expressing.

As quantum programming is leaving the domain of fiction to join reality, we need to generalise previous work on denotational semantics to the quantum realm. In this talk, we will focus on the semantics for higher order quantum programming languages, namely the pre-existing static model from Pagani, Selinger and Valiron relying on relational semantics, and our dynamic model relying on concurrent game semantics.

In this talk I will present a fully diagrammatic approach to the theory of finite-state automata, based on reinterpreting their usual state-transition graphs as string diagrams. Moreover, I will give an equational theory that completely axiomatises language equivalence in this new setting. The proposed axiomatisation is finitary— a result which is provably impossible to obtain for the usual one-dimensional syntax of regular expressions. This is joint work with Fabio Zanasi.

In a recent article, my students and I have introduced a type-based analysis for deriving upper bounds on the expected execution cost of functional probabilistic programs. The analysis is naturally compositional, parametric in the cost model, and supports higher-order functions and inductive data types. The derived bounds are multivariate polynomials that are functions of data structures. Bound inference is enabled by local type rules that reduce type inference to linear constraint solving. The type system is based on the potential method of amortized analysis and extends automatic amortized resource analysis (AARA) for deterministic programs.

In this talk, I will first give an overview of AARA for deterministic programs and some of the innovations that have been introduced over the past decade. I will then describe our novel results on expected bound analysis for probabilistic programs, highlight the challenges of adopting AARA to a probabilistic language, present experimental results, and discuss some open problems.

Using finite domains to interpret semantically the simply typed lambda-calculus extends naturally the theory of finite state automata to simple programs. In this talk we are going to survey several applications of this approach ranging from equations solving, parsing and model checking.

- Nicolas Behr: Rewriting Theory for the Life Sciences - Camille Combe: Combinatoire des permutations généralisées, des objets Fuss-Catalan et structures algébriques associées. - Hugo Moeneclaey: tba - Sylvain Douteau: Stratified homotopy theory

Au programme de cette deuxième session en ligne des journées de rentrée du pôle PPS:

- Hugo Herbelin: présentation des axes scientifiques du pôle PPS.

- Vincent Blazy: Structure fine du Sous-Typage d’Univers en CCI et applications à la certification de programmes et aux Fondements des Mathématiques.

- Zeinab Galal: A Profonctorial Finiteness Semantics;

- Farzad Jafar-Rahmani: Denotational semantics of logic with fixed points.

- Ada Vienot: tba

Au programme de cette première session en ligne des journées de rentrée de PPS:

- Kostia Chardonnet: Towards a Curry-Howard Correspondence for Quantum Computation

- El-Mehdi Cherradi: Preuves, programmes et homotopie

- Simon Forest: Des constructions génériques pour les catégories supérieures

- Mickael Laurent: Intégration d'outils de programmation avancés dans un langage avec types ensemblistes

The benefits of modularity in programming — abstraction barriers, which allows hiding implementation details behind an opaque interface, and genericity, which allows specializing a single implementation to a variety of underlying data types — apply just as well to deductive program verification, with the additional advantage of helping the automated proof search procedures by reducing the size and complexity of the premises and by instantiating and reusing once-proved properties in a variety of contexts.

This talk presents the modularity features of WhyML, the language of the program verification tool Why3. Instead of separating abstract interfaces and fully elaborated implementations, WhyML uses a single concept of “module”, a collection of abstract and concrete declarations, and a basic operation of “cloning” which instantiates a module with respect to a given partial substitution, while verifying its soundness. This mechanism brings into WhyML both abstraction and genericity, as illustrated by a small verified Bloom filter implementation, translated into executable idiomatic C code.

We introduce a lambda-calculus decorated with types, enhanced with intersection types, union types, and dependent types. Intersection and union types are a way to express ad hoc polymorphism and are an alternative to the parametric polymorphism of Girard. Dependent types were introduced as a way to formalize intuitionistic logic using the “proofs-as-lambda-terms / formulae-as-types” Curry-Howard principle. The resulting type system can be enriched with a decidable subtyping relation. We then discuss the design decisions which have led us to the formulation of these calculi, and provide some examples of applications; and we finally present a software implementation of the Delta-framework, with a description of the type checker, the refinement algorithm, the subtyping algorithm, the evaluation algorithm and the command-line interface. This work can be understood as a little step toward an alternative type theory to defining polymorphic programming languages and interactive proof assistants.

We will present the design and implementation of _Interaction Trees_ (ITrees), a general-purpose data-structure for representing in Coq potentially divergent, effectful, programs. ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from event handlers, which give meaning to events by defining their semantics as monadic actions. They are expressive enough to represent impure and potentially nonterminating, mutually recursive computations in Coq. Finally, they give rise to a theory enabling equational reasoning, up to weak bisimulation, about ITrees and monadic computations built from them. In contrast to other approaches, ITrees are executable via code extraction.

ITrees are expressive enough to serve as a language of specification for many projects of the DeepSpec ecosystem, making them a convenient Franca Lingua for formal specification, and helping in connecting projects together. Furthermore, their ability to be extracted make them compatible with ambitions of liveness and two-sidedness.

In this talk, we will particularly focus on how ITrees can be used in the context of verified compilation. To this end, we will first introduce the core concepts over a toy language, before sketching how we have been scaling the approach to LLVM IR as part of the Vellvm DeepSpec project.

Concurrent Kleene algebra (CKA) is an algebraic framework to reason about concurrent programs. In recent years, we have studied several ways of enhancing CKA with extra features, to carry out more sophisticated verification tasks.

In this talk, I will start by recalling the basic definitions of CKA, and its decidability and completeness theorems. We will then take an overview of some of its extensions, considering aspects such as control-flow, memory consistency and mutual exclusion.

This talk is the result of collaborations with Tobias Kappé, Jana Wagemaker, Simon Docherty, Fabio Zanasi, Jurriaan Rot, Alexandra Silva, David Pym, Damien Pous, and Georg Struth.

Separation logic has proven an effective way of reasoning about functional correctness of imperative programs. In the last decade, tools brought its expressiveness to interactive program verification (for example, CFML applies to a meaningful fragment of the OCaml language).

There is now a call for reasoning principles for shared-memory concurrency. In real-world applications, shared memory typically exhibits counter-intuitive behaviors, and “weak” memory models are required to describe them. This poses specific challenges for program verification.

After introducing the weak memory model of Multicore OCaml, I will derive a program logic for this language, and demonstrate its usage on simple examples.

I will show how, in our logic, the invariants of these concurrent data structures extend from the naive model of memory to the weaker model enforced by Multicore OCaml. This model is simpler than that of C11, and we argue that our logic exhibits primitive reasoning principles that are easier to deal with than what was possible for C11.

This work builds on the Iris concurrent separation logic framework and is fully mechanized in Coq.

The security of communications heavily relies on cryptography. For decades, mathematicians have invested an immense effort in providing cryptography that is built on firm mathematical foundations. This has lead to a collection of cryptographic primitives whose correctness can be proved by drawing on results from branches of mathematics such as complex analysis, algebraic geometry, representation theory and number theory. A stated goal of recent competitions for cryptographic standards is to gain trust from the broad cryptography community through open and transparent processes. These processes generally involve open-source reference and optimized implementations for performance evaluation, rigorous security analyses for provable security evaluation and, often, informal evaluation of security against side-channel attacks. These artefacts contribute to building trust in candidates, and ultimately in the new standard. However, the disconnect between implementations and security analyses is a major cause for concern.

In this talk, I will present the Jasmin-EasyCrypt project that explores how formal approaches could eliminate this disconnect and bring together implementations (most importantly, efficient implementations) and software artefacts, in particular machine-checked proofs, supporting security analyses.

Suite de l'exposé de la semaine précédente, cf. son résumé.

Nous donnerons un panorama « généraliste » des différentes variantes de la théorie des types de Martin-Löf et de leurs implémentations dans des assistants de preuve (Agda, Coq, Lean, Arend, …). En particulier, nous essaierons d'articuler certaines questions autour des questions d'égalité définitionnelle/propositionnelle, conversion judgementale/non-typée, univers à la Tarski/Russell, syntaxe intrinsèque/extrinsèque.

Nous donnerons les principes de base de la manière de pensée « HoTT » : principle d'univalence (= extensionalité des types), inductifs supérieurs (généralisation des pushouts), niveaux d'homotopie (h-niveaux), correspondance entre preuves d'égalité et chemins, correspondance propositions/types/espaces/∞-groupoïdes, description « synthétique » d'espaces géométriques (par exemple, cercle = pure donnée algébrique d'un point et d'un chemin autour de ce point), construction de Grothendieck reliant ΣB.(B→A) et A→Type.

Nous pourrions aussi aborder la théorie des types cubiques vue comme style direct pour la paramétricité itérée délimitée. Nous pourrions aussi essayer d'ébaucher le dictionnaire permettant de connecter les vocabulaires informatique/logique/géométrique/catégorique.

À noter que l'exposé essaiera en premier lieu de répondre à la curiosité de l'auditoire et le plan donné pourra évoluer en fonction des questions posées.

To verify properties of functional programs, such as termination, one can use for instance type theory or model-checking. I will present some results for the verification of functional programs, both in the deterministic and in the probabilistic case. In the deterministic case, model-checking of formulas of monadic second-order logic (MSO) is decidable over higher-order recursion schemes (HORS), a candidate model for functional programs. I will present this result, and then turn to the probabilistic case, for which we will explore two approaches for verifying termination: one based on type theory, the other one on model-checking.

Very short abstract: What is an existentially closed Heyting algebra and what does it have to do with automata theory?

Slightly longer abstract: Logical systems of deduction often resemble algebraic systems of equation resolution. The simplest instance of this resemblance is the fact that classical propositional logic essentially boils down to studying algebras over the two-element field. When one changes the logical deduction system, the algebraic structures become less simple, and more interesting; this is where one enters the world of Heyting algebras, modal algebras, and generalizations of such.

The aim of our work here is to gain a better understanding of such logical-algebraic structures by studying them from the perspective of model theory. In the model-theoretic study of usual algebra, the concept of model completeness plays a central role: it provides the correct abstraction of the concept of an algebraically closed field. We show that model completeness also has an important role to play in logical algebra.

In particular, we will discuss two cases of model completeness: intuitionistic logic, and linear temporal logic. In the former, model completeness can be seen to be closely related to a certain interpolation property of the logic, originally established by Pitts. In the latter, automata on infinite words are the technical ingredient that leads to model completeness.

On introduit les systèmes de réécriture topologiques comme généralisation des systèmes de réécriture abstraits, où l'on considère un espace topologique au lieu d'un ensemble de termes. Les systèmes de réécriture abstraits sont les systèmes de réécriture topologiques pour la topologie discrète. On introduit la confluence topologique comme étant une propriété de confluence par passage à la limite, et on caractérise les bases standards par cette propriété. On caractérise également la confluence topologique par des opérations de treillis grâce à une représentation des systèmes de réécriture par des opérateurs de réduction continus. Enfin, on relie les représentations des séries formelles non commutatives à la dualité des opérateurs de réduction, et on déduit un critère pour qu'une algèbre soit syntaxique.

I will talk about a system that combines Dependent Types and Linear Types. As an application of this system, I will show how to transport Martin Hofmann's LFPL and Amortised Resource analysis systems for resource constrained computing to full dependent types. This results in a theory where unconstrained computations are allowed at the type level, but only polynomial time computations at the term level. The combined system now allows one to explore the world of propositions whose proofs are not only constructive, but also of restricted complexity.

Systems programming often requires the manipulation of resources like file handles, network connections, or dynamically allocated memory. Programmers need to follow certain protocols to handle these resources correctly. Violating these protocols causes bugs ranging from type mismatches over data races to use-after-free errors and memory leaks. These bugs often lead to security vulnerabilities.

While statically typed programming languages guarantee type soundness and memory safety by design, most of them do not address issues arising from improper resource handling. Linear and affine types guarantee single-threaded resource usage, but they are rarely deployed as they are too restrictive for real-world applications.

We present Affe, an extension of ML with constrained types that manages linearity and affinity properties through kinds. In addition Affe supports the exclusive and unrestricted borrowing of affine resources, inspired by features of Rust. Moreover, Affe retains the defining features of the ML family: an impure, strict functional expression language with complete principal type inference and type abstraction through modules. Our language does not require any linearity annotations in expressions and supports common functional programming idioms.

Draft: https://arxiv.org/abs/1908.09681

Despite continued progress in program verification, many fundamental data structures and algorithms remain difficult to verify. Challenges arise when programs use concurrency or randomization because these effects lead to non-deterministic behavior. Although many specialized logics have been developed to reason about programs that use either concurrency or randomization, most can only handle the use of one of these features in isolation. However, many common concurrent data structures are randomized, making it important to consider the combination.

This talk will describe Polaris, a logic for reasoning about programs that are both concurrent and randomized. Polaris combines ideas from three separate lines of work: (1) Varacca and Winskel's denotational model of non-determinism and probability, (2) Barthe et al.'s approach to probabilistic relational reasoning via couplings, and (3) higher-order concurrent separation logic, as realized in the Iris verification framework.

http://chocola.ens-lyon.fr/events/

We study trace-based equivalences for labelled transition systems combining nondeterministic and probabilistic choices. We do so via a coalgebraic construction known as the generalized powerset construction, which consists in first determinizing a system and then recovering trace equivalence as bisimulation equivalence on the determinized system. The generalized powerset construction allows us to apply these two steps, inspired by the standard powerset construction for nondeterministic automata, to a variety of systems, such as labelled transition systems with different computational effects captured by monads (e.g., systems with probabilistic choices). We show how trace semantics for labelled transition systems combining nondeterministic and probabilistic choices can be recovered by instantiating the generalized powerset construction, and we characterise and compare the resulting semantics to known definitions of trace equivalences appearing in the literature. Most of our results are based on the exciting interplay between monads and their presentations via algebraic theories.

The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential lambda-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in lambda-calculus that are usually demonstrated by exploiting Scott's continuity, Berry's stability or Kahn and Plotkin's sequentiality theory.

A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.

http://chocola.ens-lyon.fr/events/

http://chocola.ens-lyon.fr/events/

In this talk, I will explain the fundamental ideas of stochastic mechanics which led me to investigate the dynamics of graph-like structures, using a new perspective on rewriting systems. My talk is designed to be accessible to a wide audience, and I will thus illustrate my approach on a very simple voter model, expressed in the language of stochastic rewriting. The discussion of this elementary example will clarify the reasons why I am currently working on a general theory of tracelets, mixing ideas from rewriting theory, category theory and concurrency theory, in order to extend the traditional realm of stochastic mechanics, and to implement analysis tools for sophisticated and currently intractable stochastic phenomena on graph-like structures.

http://chocola.ens-lyon.fr/events/

Rencontres de rentrée du pôle PPS de l'IRIF, du lundi 2 au mardi 3 septembre 2019. Accueil à 9h, exposés de 9h30 à 17h30.

Programme détaillé disponible sur la page https://www.irif.fr/rencontres/pps2019/index.

We give a geometry of interaction model for a typed lambda-calculus endowed with operators for sampling from a continuous uniform distribution and soft conditioning, namely a paradigmatic calculus for higher-order Bayesian programming. The model is based on the category of measurable spaces and partial measurable functions, and is proved adequate with respect to both a distribution-based and a sampling based operational semantics.

Joint work with Naohiko Hoshino

(This is a joint seminar between the CompSys, PPS, and Verification seminar series.)

Processing large amounts of data used to be an affair of specialists: specialized hardware, specialized software, specialized programming model, specialized engineers. MapReduce was the first widely adopted high-level API for large-scale data processing. It helped democratize big data processing by providing a clear abstraction that was supported by several efficient systems. In this talk, I will present how the programming APIs (and underlying systems) for large-scale data processing evolved in the past 20 years, both within Google and in the open source world. I will start from MapReduce and Millwheel and finish with Apache Beam and where we're headed next.

We propose a new core calculus for programming languages with effects, interpreted using a hypergraph-rewriting abstract machine inspired by the Geometry of Interaction. The intrinsic calculus syntax and semantics only deals with the basic structural aspects of programming languages: variable binding, name binding, and thunking. Everything else, including function abstraction and application, must be provided as extrinsic operations with associated rewrite rules. The graph representation yields natural concepts of locality and robustness for equational properties and reduction rules, which enable a novel flexible and powerful reasoning methodology about (type-free) languages with effects. We illustrate and motivate the technique with challenging examples from the literature.

Joint work with Koko Muroya and Todd Waugh Ambridge.

A vast amount of individuals’ data is collected, stored and accessed every day. These data are valuable for scientific and medical research, for decision making, etc. However, use or release of these data may be restricted by concerns for the privacy of the individuals contributing them. Differential Privacy has been conceived to offer ways to answer statistical queries about sensitive data while providing strong provable privacy guarantees ensuring that the presence or absence of a single individual in the data has a negligible statistical effect on the query's result. In this talk I will introduce differential privacy and present some formal verification techniques we developed to help programmers to certify their programs differentially private and to guarantee that their programs provide accurate answers. These techniques combine approaches based on type systems and program logics with ideas for reasoning about differential privacy using composition, sensitivity and probabilistic coupling. This combination permits fine-grained formal analyses of several basic mechanisms that are fundamental for designing practical differential privacy applications. In addition, I will present some of our results showing how to answer a large number of queries on high dimensional datasets preserving privacy, and how to perform differentially private chi-squared hypothesis testing with the same asymptotic guarantees as the traditional tests.

There is no known way of giving a domain-theoretic semantics to higher-order probabilistic languages, in such a way that the involved domains are continuous or quasi-continuous - the latter is required to do any serious mathematics. We argue that the problem naturally disappears for languages with two kinds of types, where one kind is interpreted in a Cartesian-closed category of continuous dcpos, and the other is interpreted in a category that is closed under the probabilistic powerdomain functor. Such a setting is provided by Paul B. Levy's call-by-push-value paradigm. Following this insight, we define a call-by-push-value language, with probabilistic choice sitting inside the value types, and where conversion from a value type to a computation type involves demonic non-determinism. We give both a domain-theoretic semantics and an operational semantics for the resulting language, and we show that they are sound and adequate. With the addition of statistical termination testers and parallel if, we show that the language is even fully abstract - and those two primitives are required for that.

We examine some combinatorial properties of parallel cut elimination in multiplicative linear logic (MLL) proof nets. We show that, provided we impose a constraint on some paths, we can bound the size of all the nets satisfying this constraint and reducing to a fixed resultant net. This result gives a sufficient condition for an infinite weighted sum of nets to reduce into another sum of nets, while keeping coefficients finite. We moreover show that our constraints are stable under reduction.

Our approach is motivated by the quantitative semantics of linear logic: many models have been proposed, whose structure reflect the Taylor expansion of multiplicative expo- nential linear logic (MELL) proof nets into infinite sums of differential nets. In order to simulate one cut elimination step in MELL, it is necessary to reduce an arbitrary number of cuts in the differential nets of its Taylor expansion. It turns out our results apply to differential nets, because their cut elimination is essentially multiplicative. We moreover show that the set of differential nets that occur in the Taylor expansion of an MELL net automatically satisfies our constraints.

(Joint work with Jules Chouquet.)

Alors que de nombreux modèles de calcul nous permettent de manipuler des données issues de domaines non dénombrables (fonctions d'ordre supérieur, nombres réels, objets définis par co-induction), les différentes notions de complexité ne permettent de s'intéresser qu'à des fonctions d'ordre 1 (i.e. traitant des données finies) voire des fonctions d'ordre 2 (i.e. traitant des fonctions d'ordre 1). Dû à la difficulté de définir une notion pertinente de taille pour des données d'ordre quelconque, les notions de complexité pour des fonctions d'ordre 3 ou plus sont à la fois incomplètes et imparfaites.

En nous appuyant sur la sémantique des jeux nous proposons ici une définition de taille et de complexité pour les fonctions d'ordre supérieur de PCF, et plus généralement pour tout processus calculatoire assimilable à une certaine classe de jeux séquentiels.

There are different categorical approaches to variations of transition systems and their bisimulations. One is coalgebras, another one is open maps. In this talk, I will describe these two approaches, illustrated by the case of labelled transition systems (almost no knowledge in category theory is needed for this part). I will then describe how it is possible to translate one into the other in some cases. From open maps to coalgebras, this was done by Lasota, using multi-sorted transition systems. From coalgebras to open maps, this was done in my joint work with Thorsten Wißmann, Shin-ya Katsumata and Ichiro Hasuo, where we derived path-categories and trace semantics for free for different flavors of categories of coalgebras with non-deterministic branching. I will illustrate those constructions on various concrete examples (tree automata, regular nominal automata, …).

Taylor expansions have been introduced by Ehrhard and Regnier as a computational interpretation of Girard's quantitative semantics. Lambda-terms are expanded into linear combinations of their n-linear approximants, such approximants being defined as resource lambda-terms. This construction is well-suited to interpret quantitative calculi, such as the probabilistic lambda-calculus: Taylor expansions are linear combinations and the resource lambda-calculus is linear so interpreting probability distributions over terms is straightforward. Yet paradoxically the proof technique used by Ehrhard and Regnier to study Taylor expansions heavily rely on the particular structure of the expansions of ordinary lambda terms, and they are not suited to work on a quantitative setting. In this talk we will show how to indirectly extend their result to probabilistic Taylor expansions. First we will introduce explicit Taylor expansions, which uses “inert” probabilistic choices to interpret probabilistic terms while preserving the necessary properties to apply Ehrhard and Regnier's proof techniques. Then we will show how to extract interesting results on probabilistic Taylor expansions from these explicit Taylor expansions.

Les réseaux de preuves donnent une représentation canonique des démonstrations dans la logique linéaire multiplicative : l'équivalence dénotationnelle des preuves coïncide avec l'équivalence des réseaux. Par contre, la canonicité des réseaux ne s'étend pas au second ordre. Ce problème est du à la présence des témoins des règles existentielles. En fait, dans plusieurs sémantiques dénotationnelles l'information portée par les preuves est compressée, et notamment les témoins existentiels sont effacés.

Font partie de ces sémantiques “effaçantes” les sémantiques cohérente et rélationnelle, ainsi que la sémantique dinaturelle et la sémantique observationnelle. On présente des résultats sur l'équivalence des preuves dans ces sémantiques et on discute des applications en complexité dues à la possibilité de compresser les preuves. Une partie de ces travaux est issue d'une collaboration avec L. Tortora de Falco, T. Seiller et L.T.D. Nguyễn.

Species of Structures, introduced almost 40 years ago, give a natural conceptu l framework for the notion of ``combinatorial construction on sets’’. Fundamental operations between species allow the specification of new species in terms of known ones, giving a systematic context for the solution of classical enumeration questions, including both labelled and unlabelled enumeration (a.k.a. Pólya Theory). In this talk, we will give an accessible introduction to the Theory of Species, with many illustrations. If time allows, we will also survey some of many areas (computer science, theoretical physics, chemistry, etc.) where they are currently useful.

The naive translation of set-theoretic definitions of algebraic structures (such as monoids, categories and groups) into Martin-Lof type theory is often incomplete: without additional hypotheses such as truncation or a decidable equality, these translations fail to specify the behavior of the structure with respect to higher equalities. On the other hand, a complete description of such structures is quite difficult, as it typically requires the specification of an infinite number of equations. I will present recent progress on this problem by giving a definition of a “coherent polynomial monad” internal to type theory.

We introduce a type system for the $\pi$-calculus which is designed to guarantee that typable processes are well-behaved, namely they never produce a run-time error and, even if they may diverge, there is always a chance for them to “finish their work”, i.e. to reduce to an idle process. The introduced type system is based on non-idempotent intersections, and is thus very powerful as for the class of processes it can capture. Indeed, despite the fact that the underlying property is $\Pi^0_2$-complete, there is a way to show that the system is complete, i.e., that any well-behaved process is typable, although for obvious reasons infinitely many derivations need to be considered.

Joint work with Ugo Dal Lago, Marc De Visme, Akira Yoshimizu

The notion of linearisation of the lambda-calculus has been explored in different settings: Damas and Florido used information given by intersection types, to define a notion of expansion of terms in the lambda-calculus into linear terms; Kfoury embedded the lambda-calculus into a new linear calculus, with a new notion of “linear” reduction, and linearization was defined indirectly by means of a notion of contraction of expanded terms in the new calculus into standard lambda-terms; Alves and Florido defined a notion of linearisation from standard lambda-terms into a linear subset, called the weak linear lambda-calculus, by using the notion of computation as paths, deriving from Lévy’s labelled lambda-calculus.

In this talk we will explore these previous works, discuss their relation and present some open problems regarding the termination of linearisation methods.

Herbrand's theorem exposes some of the constructive content of classical logic. In its simplest form, it reduces the validity of a first-order purely existential formula to that of a finite disjunction. More generally, it reduces first-order validity to propositional validity, by understanding the structure of the assignment of first-order terms to existential quantifiers, and the causal dependency between quantifiers.

In this talk, we show that Herbrand's theorem in its general form can be elegantly stated and proved as a theorem in the framework of concurrent games, a denotational semantics designed to faithfully represent causality and independence in concurrent systems. Closely related to expansion trees, the causal structure of concurrent strategies, paired with annotations by first-order terms, is used to specify the dependency between quantifiers. As furthermore these strategies can be composed we are able to interpret classical sequent proofs, yielding a compositional proof of Herbrand's theorem.

http://chocola.ens-lyon.fr/events/meeting-2018-12-13/

Implicative Algebras were recently introduced as a unified framework for forcing and realisability, whose particularity is to interpret terms and formulæ uniformly.

In this ongoing work with Alexandre Miquel, we show how linear logic fits in this picture: we present a family of models, where certain computational principles are distinguished, and argue thata it provides a satisfactory meaning explanation of the connectives of (perfective) linear logic.

In this talk I will review G4ip, a simple calculus for intuitionistic propositional logic (IPL) that provides a decision procedure for provability. Its basic mechanisms can be traced back to Vorob'ev in the 50s, and were found again by Hudelmaier (88), Dyckhoff (90), Paulson (91), and (with a linear logic flavour) Lincoln-Scedrov-Shankar (91). In 2015, Claessen and Rosén presented the fastest decision procedure for IPL, based on SMT-solving techniques. We describe their algorithm and show how it can be seen as a variant of the aforementioned calculus, albeit with key variations that provide increased performance. Their algorithm relies on a SAT-solver used as a black box and treats intuitionistic entailment as a theory. We show how the recent framework of model-constructing satisfiability for SMT-solving could further integrate intuitionistic reasoning within the main SAT-solving loop. This would constitute an intuitionistic variant of the main algorithm of SAT-solvers, where Kripke models are built instead of Boolean models.

11:00 – 12:30 Éric Tanter (Universidad de Chile & Inria Paris) - Invited talk: Abstracting Gradual Typing: Principles and Application to Gradual Parametricity

  Gradual typing enables programming languages to seamlessly combine dynamic and static checking. Language researchers and designers have extended a wide variety of type systems to support gradual typing. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs. Based on an understanding of gradual types as abstractions of static types, we have developed systematic foundations for gradual typing based on abstract interpretation, called Abstracting Gradual Typing (AGT for short). Gradual languages designed with the AGT approach satisfy, by construction, the established criteria for gradually-typed languages. In this talk, I will give a brief introduction to AGT in a simply-typed setting, and will then discuss recent work on a gradual counterpart of System F that enforces relational parametricity, even in the presence of imprecise types.

14:00 – 15:00 Flavien Breuvart (Université Paris 13) - Invited talk: Graded Types Parametricity : Principles and Application to Abstract Interpretation

  In this talk, we will briefly present the yet-to-start project CoGITARe, which aims at developing further graded types expressivity and inference in order to use them to perform abstract interpretations.
  In a second time, we give an historic on graded type systems and their expressivity. Then, we will see that this expressivity is limited by a lake of dependency/parametricity. We will thus explore two ongoing research directions that adds two very different kind of parametricity to graded types.
  (The provocative title should only be taken as a joke. Despite their apparent similitudes, this work and Éric Tanter's have vastly different objectives and involved different issues and techniques. In particular, notice that gradual and graded types are fundamentally different.)

15:30 – 16:30 Shane Mansfield (Univ. of Oxford) - Invited talk: An overview of empirical models

  Empirical models are a way of formalising data that arises in physical experiments. They were first proposed by Abramsky and Brandenburger as part of a framework to analyse fundamentally non-classical phenomena in quantum systems. Conveniently from a computer science perspective, they abstract away from the mathematical baggage of quantum theory and instead allow the key phenomena to be characterised purely as features of empirical data. After introducing the basic framework I will discuss some more recent results and developments, drawing on joint work with a number of collaborators. In particular: quantum computations can simply be modelled as classical computations with the additional ability to interact with a resource empirical model; quantitative measures of non-classicality can be shown to relate directly to some basic quantum-over-classical computational advantages; and the beginnings of a category-theoretic approach to reasoning about empirical models have emerged.

18:00 – 19:00 Xavier Leroy - Lecture: Leçon inaugurale au Collège de France

  This is not part of the CHoCoLa day, but you might be interested in attending! See https://www.college-de-france.fr/site/xavier-leroy/inaugural-lecture-2018-11-15-18h00.htm

  The meeting will take place in Bâtiment Sophie Germain, here.
  We will first gather at the 3rd floor of the building, for a breakfast.
  We will then move for the talk of the morning (11.00-12.30) to Amphi Turing.
  We will have lunch in room 3052
  In the afternoon (14h-16h30), we will be in room 1016

Journées PPS 2018

Journées PPS 2018

We propose a type-based analysis to infer the session protocols of channels in an ML-like concurrent functional language. Combining and extending well-known techniques, we develop a type-checking system that separates the underlying ML type system from the typing of sessions. Without using linearity, our system guarantees communication safety and partial lock freedom. It also supports provably complete session inference with no programmer annotations. We exhibit the usefulness of our system with interesting examples, including one which is not typable in substructural type systems.

Guarded recursion has emerged as a natural paradigm for programming with infinite data structures in type theory and high-assurance functional languages. In the first part of this talk, I will present some intuitions behind guarded recursion, using programming examples. In a second part, I will discuss ongoing work on a typed lambda-calculus equipped with rich facilities for defining and manipulating guarded recursive types.

(joint work with J. Weinberger)

Abstract: Voevodsky's model of the Univalence Axion in simplicial sets is not constructive as shown by Coquand et al. To avoid this problem Cohen, Coquand, Huber, Moertberg have constructed in Cubical Sets a model of a Cubical Type Theory which has computational meaning.

We show that simplicial sets form a subtopos of cubical sets which allows one to contructively reason in the latter about the former.

I will give a new definition of partial Higher Dimension Automata – a geometric model for true concurrency – using lax functors. This definition is simpler than the original, and more natural from a categorical point of view, but also matches more clearly the intuition that pHDA are Higher Dimensional Automata with some missing faces. I will then focus on trees. Originally, for example in transition systems, trees are defined as those systems that have a unique path property. To understand what kind of unique path property is needed in pHDA, I will start by looking at trees as colimits of paths. From this, I will deduce that trees are exactly the pHDA with the unique path property modulo a notion of homotopy, and without any shortcuts. This property will allow me to prove two interesting characterisations of trees: trees are exactly those pHDA that are the unfolding of another pHDA; trees are exactly the cofibrant objects, much as in the language of Quillen’s model structures. In particular, this last characterisation gives the premisses of a new understanding of concurrency theory using homotopy theory.

In a 2012 paper, Richard Statman exhibited an inference system, based on second order monadic logic and non-terminating rewrite rules, that exactly types all strongly normalizable lambda-terms. We show that this system can be simplified to first-order minimal logic with rewrite rules, along the Deduction Modulo Theory lines.

We show that our rewrite system is terminating and that the conversion rule respects weak versions of invertibility of the arrow and of quantifiers. This requires additional care, in particular in the treatment of the latter. Then we study proof reduction, and show that every typable proof term is strongly normalizable and vice-versa.

On discutera différentes manières de relier syntaxiquement la logique linéaire classique (LL) et sa version intuitionniste (ILL) : d'une part à travers la question de la conservativité de LL sur ILL (contre-exemples et conditions suffisantes), et d'autre part via l'étude de non-non traductions de LL dans ILL. On montrera que ces traductions permettent de représenter des extensions de LL dans ILL, mais aussi qu'elles peuvent être utilisées comme outil pour prouver des propriétés de LL : élimination des coupures et focalisation par exemple. Ces différents résultats ont été formalisés en Coq à l'aide de la bibliothèque Yalla, que nous présenterons brièvement.

There exists a large spectrum of techniques for proving correctness of computer programs. At one end is the Curry-Howard isomorphism, in which a typing procedure automatically checks the correctness of a program, and at the other end are techniques à la Hoare, in which non-trivial reasonning is performed in a logic adapted to the programming language. Realizability can be seen as a mixture of these two approaches: proving that a program realizes a specification is done via a combination of automatic techniques in a Curry-Howard fashion, and manual proofs of correctness of subprograms with respect to some axioms. In my talk I will present some realizability models where the realizability relation is defined semantically: a program realizes a specification if its denotation satisfies a property in the model. The denotational models involved include game semantics, continuation models and Scott domains.

This talk will present SyTeCi, the first general automated tool to check contextual equivalence for programs written in a typed higher-order language with references (i.e. local mutable states), corresponding to a fragment of OCaml.

After introducing the notion of contextual equivalence, we will see on some examples why it is hard to prove such equivalences (reentrant calls, private states). As we will see, such examples can be found in many different programming languages.

Then, we will introduce SyTeCi, a tool to automatically check such equivalences. This tool is based on a reduction of the problem of contextual equivalence of two programs to the problem of reachability of “error states” in transition systems of memory configurations.

Contextual equivalence being undecidable (even in a finitary setting), so does the non-reachability problem for such transition systems. However, one can apply model-checking techniques (predicate abstraction, summarization of pushdown systems) to check non-reachability via some approximations. This allows us to prove automatically many non-trivial examples of the literature, that could only be proved by hand before. We will end this talk by the presentation of a prototype implementing this work.

No one is without knowing the famous Shadok principle « the more it fails, the more likely it will eventually succeed. » Taking inspiration from this unfathomable wisdom, we came up with a dependent type theory which allows failure, so that we could succeed more in proving things. Such a Shadok theory is justified by translating it away into vanilla dependent theory, just as a mundane compiler would, where failing can be interpreted as a call-by-name exception mechanism. En passant, this gives the first full syntactical model of the Calculus of Inductive Constructions introducing effects.

Alas! The right to fail succeeds a tad too much, insofar as the resulting Shadock type theory is logically inconsistent. Not being impressed in any way, we put order into this madness by requiring that no exception should ever reach toplevel, thanks to a clever use of a variant of Bernardy-Lasson syntactic parametricity. While the former model can be thought of as Friedman A-translation applied to CIC, the latter is no more than a principled variant of Kreisel's modified realizability that scales to dependent types. In particular, it readily gives a model of CIC that still has canonicity, strong normalization and decidable type-checking, while featuring new principles typical of modified realizability such as the independence of premises and unprovability of Markov's principle.

https://www.pédrot.fr/articles/exceptional.pdf

The causal structure of spacetime defines a (pair of) natural order structures on the underlying set of events. Much of the analysis of cauasl structure involves a delicate interplay between order, topology and geometry. In view of the fundamental role of the causal order in certain approaches to quantum gravity as well as its fundamental role in concurrency theory one can ask whether the topology can be derived from pure order theoretic considerations.

In a remarkable example of serendipity, order theory has been developed by computer scientists and mathematicians in order to capture computability concepts. Dana Scott developed a notion of a continuous lattice or continuous poset with a view to capturing computability as continuity with a suitable topology that has come to be known as the Scott topology. This subject has acquired the name of ``domain theory.''

We applied domain theory to the problem of reconstructing the spacetime topology from the order and came up with a number of results about reconstruction of spacetime structure from just a countable dense set.

We prove that a globally hyperbolic spacetime with its causality relation is a bicontinuous poset whose interval topology is the manifold topology. From this one can show that from only a countable dense set of events and the causality relation, it is possible to reconstruct a globally hyperbolic spacetime in a purely order theoretic manner. The ultimate reason for this is that globally hyperbolic spacetimes belong to a category that is equivalent to a special category of domains called interval domains.

This was joint work with Keye Martin of Naval Research Laboratories.

Software-based countermeasures provide effective mitigation against side-channel attacks, often with minimal efficiency and deployment overheads. Their effectiveness is often amenable to rigorous analysis: specifically, several popular countermeasures can be formalized as information flow policies, and correct implementation of the countermeasures can be verified with state-of-the-art analysis and verification techniques. However, in absence of further justification, the guarantees only hold for the language (source, target, or intermediate representation) on which the analysis is performed.

We consider the problem of preserving side-channel countermeasures by compilation for cryptographic “constant-time”, a popular countermeasure against cache-based timing attacks. We present a general method, based on the notion of 2-simulation, for proving that a compilation pass preserves the constant-time countermeasure. Using the Coq proof assistant, we verify the correctness of our method and of several representative instantiations.

http://chocola.ens-lyon.fr/events/meeting-2018-02-08

10:30 – 12:00

  Prakash Panangaden (Mc Gill University, Canada)
  Quantitative Equational Logic 

14:00 – 15:00

  Justin Hsu (University College London, UK)
  From Couplings to Probabilistic Relational Program Logics 

15:30 – 16:30

  Thomas Ehrhard (IRIF, Univ. Paris Diderot)
  Stable and measurable functions on positive cones: a model of probabilistic functional languages with continuous types

Many program properties are relational, comparing the behavior of a program (or even two different programs) on two different inputs. While researchers have developed various techniques for verifying such properties for standard, deterministic programs, relational properties for probabilistic programs have been more challenging. In this talk, I will survey recent developments targeting a range of probabilistic relational properties, with motivations from privacy, cryptography, machine learning. The key idea is to meld relational program logics with an idea from probability theory, called a probabilistic coupling. The logics allow a highly compositional and surprisingly general style of analysis, supporting clean proofs for a broad array of probabilistic relational properties.

Bio: Justin Hsu is a post-doctoral researcher at the University College of London. He obtained his graduate degree from the University of Pennsylvania. His research interests span formal verification and theoretical computer science, including verification of randomized algorithms, differential privacy, and game theory.

Depuis plusieurs années, je participe au groupe de travail Homenet de l'IETF, l'organisme qui définit les normes qui régissent l'Internet. Dans cet exposé, sur l'exemple de Homenet et de mes aventures à l'IETF, j'essaierai de donner une idée de ce qu'est le processus de normalisation, pourquoi il est important pour l'Informatique et pour l'Internet.

Cet exposé est une version étendue et légèrement censurée de l'exposé que j'ai donné aux Journées PPS le 12 octobre 2017.

In higher-order model-checking (HOMC), functional programs are represented as higher-order recursion schemes (HORS), a kind of grammar with parameters which can be functions. These grammars generate infinite trees, over which we want to check formulas of monadic second-order logic (MSO). This problem is decidable, as proved first by Ong in 2006, and then by many others including Kobayashi and Ong (2009) whose approach use intersection types. It turns out that linear logic is a powerful and enlightening tool to reason about HOMC, as shown by Grellois and Melliès in the last years.

In general, the complexity of the HOMC problem is n-EXPTIME, where n is the order of the HORS of interest. In this talk, we explain that we can refine this complexity measure: motivated by linear logic, we introduce *linear* HORS and a linear-nonlinear model of automaton checking fragments of MSO. We then show that HOMC is in fact n-EXPTIME complete for n the *linear* order of the linear HORS generating the tree of interest. We believe that this explains why HOMC, in spite of its huge theoretical complexity, has been successfully used in practice by Kobayashi's team.

This linear framework allows to reprove in a much simpler way three existing results extending the usual HOMC problem, and notably to deal with call-by-value programs in a smooth way (the usual HOMC approach considering call-by-name).

This is joint work with Pierre Clairambault and Andrzej Murawski.

In this talk, we introduce a new game semantics framework for concurrency based on event structures, extending the work of Rideau and Winskel. In this framework, we can extend the notions of innocence and well-bracketing to the concurrent (and non-deterministic) case, generalizing the so-called “Abramsky cube”.

This talk focuses on the deterministic case. I will first introduce the concurrent strategies and their composition, in the existing linear setting. I will then present our extension to nonlinearity using copy indices and symmetry to represent uniformity. I will then present our notions of concurrent innocence & well-bracketing, to finish on our result of intensional full abstraction for PCF. Time permitting, I will discuss extensions of this result to non-angelic nondeterminism and probabilities.

Les algèbres dendriformes sont des structures algébriques introduites par Loday. Elle offrent un moyen de découper un produit associatif en deux produits non nécessairement associatifs. L'étude de ces algèbres, réalisée avec le point de vue fourni par la théorie des opérades, fait apparaître la combinatoire des arbres binaires et des mélanges d'arbres. Nous définissons ici une opérade à un paramètre entier généralisant l'opérade diassociative. Par dualité de Koszul, nous obtenons des généralisations de l'opérade dendriforme. Les algèbres sur ces opérades permettent de découper un produit associatif en plusieurs parties, avec certaines relations de compatibilité. Les propriétés combinatoires et algébriques de ces structures sont passées en revue.

There are two possible computational interpretations of second-order arithmetic: Girard's system F or Spector's bar recursion and its variants. While the logic is the same, the programs obtained from these two interpretations have a fundamentally different computational behavior and their relationship is not well understood. We make a step towards a comparison by defining the first translation of system F into a simply-typed total language with a variant of bar recursion. This translation relies on a realizability interpretation of second-order arithmetic. Due to Gödel's incompleteness theorem there is no proof of termination of system F within second-order arithmetic. However, for each individual term of system F there is a proof in second-order arithmetic that it terminates, with its realizability interpretation providing a bound on the number of reduction steps to reach a normal form. Using this bound, we compute the normal form through primitive recursion. Moreover, since the normalization proof of system F proceeds by induction on typing derivations, the translation is compositional. The flexibility of our method opens the possibility of getting a more direct translation that will provide an alternative approach to the study of polymorphism, namely through bar recursion.

Les tableaux boisés sont des objets combinatoires intervenant notamment dans l'étude de certains modèles de mécanique statistique. Cet exposé porte sur les arbres non ambigus, qui sont un cas particulier de tableaux boisés reliés aux permutations ayant leurs excédences (w(i)>i) en début de mot. Nous avons obtenu, lors d'un travail commun avec J.-C. Aval, A. Boussicault, F. Hivert et P. Laborde-Zubieta, des résultats énumératifs et bijectifs sur ces objets, que je présenterai ici après avoir introduit le cadre de cette étude.

Gradual typing is an approach for designing programming languages that integrate static and dynamic type checking. Gradual typing gives the programmer fine-grained control over which regions of a program are statically checked and which regions are dynamically checked. Over the last decade, there has been renewed interest in such an integration partly due to the rise in popularity of dynamic languages. But as small programs grow into large programs, so does the need for early error detection and modularity, which is provided by static type checking. Gradual typing provides a practical migration path for dynamically typed programs to become more statically typed. This talk will give a glimpse at the state of the art in gradual typing. It will describe a) the major challenges in the design and implementation of gradually typed languages, b) the research that has addressed many of of these challenges, and c) the open problems that need to be solved. The research in gradual typing spans both theoretical and practical questions, from mechanized metatheory to efficient compilation.

I will present a new proof assistant, Globular, which allows the formalization of compositional proofs in higher category theory. The interface is geometrical, with proofs depicted as string diagrams, and allowing direct click-and-drag manipulation of proofs in a simple and intuitive way, up to the level of 4-categories. I will show how to build a simple proof from scratch, and present some sophisticated formalized proofs from topology and algebra. I will also give some details of the theoretical basis, which gives a new and simple way to understand higher category theory. This talk will be accessible, and will not require any previous knowledge.

Web site: https://ncatlab.org/nlab/show/Globular Paper: https://arxiv.org/abs/1610.06908

Testing theory focuses on contextual equivalences that were proposed in the 80s as an alternative to bisimulation equivalence. During the last decade testing equivalences proved useful in constructing semantic models of session types and in laying the foundations of web-service technologies. As result, testing theory is more useful and richer than ever. In this seminar I will recall the chief ideas behind testing theory, and argue that we lack a general methodology to reason on testing equivalences. I will also outline the evidence that a meta-theory may exist, and some open questions.

The main purpose of this talk is to introduce a new automata model, hybrid set-vector automata, that naturally embed deterministic finite state automata and finite automata weighted over a field.

We take a category-theoretic approach, which provides a neat understanding of minimisation. It is well known that category theory offers a unifying view of some automata theory results. For example, minimisation of deterministic automata (over finite words) and Shützenberger’s automata weighted over fields, arise from the same categorical reasons.

In the first part of the talk, I will discuss about how to model and minimise automata in categories. Traditionally, automata are seen either as algebras for a functor plus a final map, possibly in a monoidal category, or as coalgebras for a functor plus an initial map. We propose yet another view of automata as functors from an input category to an output category.

The new hybrid set-vector automata can be modelled by taking the output category to be a free-colimit completion of the category of finite-dimensional vector spaces under a certain class of colimits.

This is joint work with Thomas Colocombet.

A very natural notion of equivalence of programs is the observational equivalence: two programs are equivalent if they have the same behaviour in any environment. More specifically in the lambda-calculus two terms M and N are equivalent if for every context C, the terms C[M] and C[N] are either both solvable or both unsolvable. Respecting this equivalence is an important property of some models of the lambda-calculus, called the full abstraction. It is well known that the model of infinitely extensional Böhm trees is fully abstract. The question we are interested in is what becomes of these notions when we introduce probabilistic choice in the calculus.

The solvability has a natural extension, which is the convergence probability, hence two terms are observationally equivalent if they have the same convergence probability under any context. There is also a simple way to define probabilistic Bohm trees, as we can associate to any term a subprobability distribution over head normal forms. But it is not obvious that these generalizations of the deterministic notions are still equivalent. In this talk we will show how to prove that probabilistic Böhm trees actually form a model, and how to get a separability result to ensure this model is fully abstract.

In functional programs, also called higher-order programs, functions may take functions themselves as arguments. As a result, their model-checking relies in most approaches on semantic or type-theoretic tools. In this talk, I will explain how an analysis based on linear logic of a model-checking result of 2009 by Kobayashi and Ong led Melliès and I to the construction of a model for model-checking. This model is such that, when interpreting a term with recursion representing the tree of traces of a functional program, its denotation determines whether it satisfies a MSO property of interest. A related and similar model was obtained independently by Salvati and Walukiewicz. In the second part of the talk, I will discuss the verification of termination for functional programs with recursion and probabilistic choice. Dal Lago and I defined recently a type system which is such that typable programs terminate with probability 1. In other terms, their set of diverging executions is negligible. If time allows, I will sketch ideas towards an extension of the model-checking results of the deterministic case to quantitative logics and functional programs with recursion.

The starting point of the talk will be the identification of structure common to tree-like combinatorial objects, exemplifying the situation with abstract syntax trees~(as used in formal languages) and with opetopes (as used in higher-dimensional algebra). The emerging mathematical structure will be then formalized in a categorical setting, unifying the algebraic aspects of the theory of abstract syntax of [2,3] and the theory of opetopes of [5]. This realization conceptually allows one to transport viewpoints between these, now bridged, mathematical theories and I will explore it here in the direction of higher-dimensional algebra, giving an algebraic combinatorial framework for a generalisation of the slice construction of [1] for generating opetopes. The technical work will involve setting up a microcosm principle for near-semirings and subsequently exploiting it in the cartesian closed bicategory of generalised species of structures of [4]. Connections to (cartesian and symmetric monoidal) equational theories, lambda calculus, and algebraic combinatorics will be mentioned in passing.

[1] J.Baez and J.Dolan. Higher-Dimensional Algebra III. n-Categories and the Algebra of Opetopes. Advances in Mathematics 135, pages 145-206, 1998.

[2] M.Fiore, G.Plotkin and D.Turi. Abstract syntax and variable binding. In 14th Logic in Computer Science Conf. (LICS'99), pages 193-202. IEEE, Computer Society Press, 1999.

[3] M.Fiore. Second-order and dependently-sorted abstract syntax. In Logic in Computer Science Conf. (LICS'08), pages 57–68. IEEE, Computer Society Press, 2008.

[4] M.Fiore, N.Gambino, M.Hyland, and G.Winskel. The cartesian closed bicategory of generalised species of structures. In J. London Math. Soc.}, 77:203-220, 2008.

[5] S.Szawiel and M.Zawadowski. The web monoid and opetopic sets. In arXiv:1011.2374 [math.CT], 2010.

Dynamic programming is about exploiting sharing opportunities in recursive call trees of a function. If the pattern of sharing opportunities is known statically, a call dag can be built instead of a tree from the start.

In this talk, we present a generic framework for doing so and demonstrate it in action on two textbook examples of dynamic programming - Fibonacci and edit distance. We describe sharing opportunity patterns with systems of equations between node addresses. A technique from term rewriting systems, namely Knuth-Bendix completion, gives us unique normal forms for node addresses. A dag is represented as a spanning tree whose nodes are defined by addresses in normal form. Mathematically, the function taking an input for our function of interest into a call tree is a comonad coalgebra, node addresses are coterms and equations are coequations.

A Haskell implementation of this framework uses circular programming and a generic implementation of derivatives of functors.

We view this work as a showcase of how basic algorithmics and more advanced category theory can interact in a mutually beneficial way.

This joint work with Nicolas Wu, University of Bristol.

Graphical choreographies, or global graphs, are general multiparty session specifications featuring expressive constructs such as forking, merging, and joining for representing application-level protocols. Global graphs can be directly translated into modelling notations such as BPMN and UML. In the first part of the talk, I will first present an algorithm whereby a global graph can be constructed from asynchronous interactions represented by communicating finite-state machines (CFSMs); and a sound characterisation of a subset of safe CFSMs from which global graphs can be constructed. In the second part, I will outline a few recent applications of this work to communicating timed automata and the Go programming language.

We introduce a fully-abstract intensional model for a polymorphic call-by-value language with higher-order references. As in game semantics, the denotation of a term is represented as a set of plays between the term and its environment. But rather than building it compositionally, by induction over the term, we generate it using a labelled transition system representing all the possible interactions between the term and any environment. Names, and more generally the theory of nominal sets, are crucially used to represent locations (i.e. memory addresses) and functional and polymorphic values. Freshness of such names then control the observational power of environments. Thanks to the presence of references, the observational power of environments is strong enough to avoid the need of performing a quotient of the model to be fully abstract. This gives us new principles to reason on effectul and polymorphic programs. This work has been done in collaboration with Nikos Tzevelekos (QMUL).

We study the theory of contextual equivalence in the untyped lambda-calculus, generated by taking the normal forms as observables. Introduced by Morris in 1968, this is the original extensional lambda theory H+ of observational equivalence. On the syntactic side, we show that this lambda-theory validates the omega-rule, thus settling a long-standing open problem. On the semantic side, we provide sufficient and necessary conditions for relational graph models to be fully abstract for H+. We show that a relational graph model captures Morris's observational pre-order exactly when it is extensional and lambda-König. Intuitively, a model is lambda-König when every lambda-definable tree has an infinite path which is witnessed by some element of the model.

The process of inverting Markov kernels relates to the important subject of Bayesian modelling and learning. In fact, Bayesian update is exactly kernel inversion. ​We investigate how and when Markov kernels (aka stochastic relations, or probabilistic mappings) can be inverted. We address the question both directly on the category of measurable spaces, and indirectly by interpreting kernels as Markov operators: For the direct option, we introduce a typed version of the category of Markov kernels and use the so-called ‘disintegration of measures’. Here, one has to specialise to measurable spaces borne from a simple class of topological spaces -e.g. Polish spaces (other choices are possible). Our method and result greatly simplify a recent development ​by Culbertson and Sturz. For the operator option, we use a cone version of the category of Markov operators (​aka ​kernels seen as predicate transformers). That is to say, our linear operators are not just continuous, but are required to satisfy the stronger condition of being ω-chain-continuous.​ ​Prior work shows that one obtains an adjunction in the form of a pair of contravariant and inverse functors between the categories of L1- and L∞-cones. Inversion, seen through the operator prism, is just adjunction.​ ​No topological assumption is needed. We​ ​show​ ​that​ ​both​ ​categories​ ​(Markov​ ​kernels​ ​and​ ​ω-chain-continuous Markov operators) are related by a family of contravariant functors Tp for 1 ≤ p ≤ ∞. The Tp’s are Kleisli extensions of (duals of) conditional expectation functors introduced ​before. We​ prove​ ​that​ ​both​ ​notions​ ​of​ ​inversion agree when both defined: if f is a kernel, and f† its direct inverse, then T∞(f)† = T1(f†). This is a joint work with Fredrik Dahlqvist UCL, Ohad Kammar Oxford, Ilias Garnier ENS

We introduce a linear infinitary lambda-calculus in which two exponential modalities are available, the first one being the usual, finitary one, the other being the only construct interpreted coinductively. The obtained calculus embeds the infinitary applicative lambda-calculus and is universal for computations over infinite strings. What is particularly interesting about the calculus is that the refinement induced by linear logic allows to restrict both modalities so as to get calculi which are terminating inductively and productive coinductively. We exemplify this idea by isolating a fragment of the calculus around the principles of SLL and 4LL. Interestingly, it enjoys confluence, contrarily to what happens in ordinary infinitary lambda-calculi.

The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: denotational and operational. The former preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected.

We propose a technique for formalising and proving operational preciseness of the subtyping relation in the setting of a concurrent lambda calculus with intersection and union types. The key feature is the link between typings and the operational semantics. We prove then sound- ness and completeness getting that the subtyping relation of this calculus enjoys both denotational and operational preciseness.

This is a joint work with Mariangiola Dezani-Ciancaglini.

(joint work with Marcelo Fiore and Pierre-Louis Curien)

I will present “linear call-by-push-value” enriched-adjunction models refining call-by-push-value models of effects and linear/non-linear models of linear logic, with higher-order functions, sums, and resource modalities, together with a theorem lifting linear models into cartesian ones. I will also present computational interpretations of these models as intuitionistic (linear) logics (LJ/ILL) where the order of evaluation matters, in the form of polarised calculi that satisfy usual properties of Barendregt-style lambda-calculus, and that have sound and coherent interpretations in the previous models. This suggests an approach to modelling proofs and programs with direct models and calculi.

The purpose of this talk is to explain a new approach to complexity theory based on (dynamic) semantics of linear logic, whose aim is to enable techniques and invariants from ergodic theory (e.g. l^2-Betti numbers of a countable Borel equivalence relation) to be used in computational complexity.

The origins of the techniques can be traced to Girard's “geometry of interaction” (GoI) program using von Neumann algebras and the recent GoI-inspired results in complexity. However, this approach reaches its full strength when using the more combinatorial setting of Interaction Graphs models of (fragments of) linear logic. Using techniques akin to game semantics (with a bit of measure theory), we are able to characterise (predicate) complexity classes as the set of programs/proofs interpretations of type Pred[m] := Nat ⇒ Bool. These models are parametrised by a group of measure-preserving maps m (equivalently, by a measurable group action) and provide the first sketches of a conjectured correspondence between measurable group actions and complexity constraints.

The GHZ and W states are two entangled quantum states of three qubits, that are inequivalent in the sense that one cannot be turned into the other by local (single-qubit) operations; this is reflected in their different communicational properties and use in cryptographic protocols. A few years ago, Coecke and Kissinger showed that one can associate, to the two states, two Frobenius algebras in the category of Hilbert spaces - a type of algebra with a well-understood string diagram representation, which could hopefully provide a bridge between algebraic, computational and topological aspects of quantum entanglement. We present a complete graphical axiomatisation of the relations between the GHZ and W states/algebras: the ZW calculus. This calculus refines the pre-existing ZX calculus, while keeping its most desirable characteristics, such as the undirectedness of diagrams; comes with an explicit normalisation procedure; provides an original decomposition of the category of qubits, with a prominent “fermionic” fragment; and hints at a topological explanation of its components and axioms.