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.