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)