Je rappelle, pour fixer les notations, que si S est une catégorie, et F: S° —> CAT est un lax foncteur, cette construction fournit une catégorie Gr(F) munie d’une préfibration Pr(F): Gr(F)—>S qui est une fibration ssi F est un pseudo-foncteur. Questions: Par quel type de bi, ou 2, catégorie K peut on remplacer CAT ? Quelles propriété a la correspondance F —> Gr(F) Peut-on internaliser cette construction i.e. si E est, par exemple, un topos, peut-on remplacer S par une catégorie interne à E et CAT par la 2-catégorie CAT(E) des catégories internes à E. La liste ci-dessus est loin d’être exhaustive. Je tâcherai, sans lasser l’auditoire, de montrer la grande variété des questions…, et des réponses.

Many complex generative systems use languages to create structured objects. We consider a model of random languages, defined by weighted context-free grammars. As the distribution of grammar weights broadens, a transition is found from a random phase, in which sentences are indistinguishable from noise, to an organized phase in which nontrivial information is carried. This marks the emergence of deep structure in the language, and can be understood by a competition between energy and entropy.

We provide syntactic (expression-level) language derivative operations, both in the styles of Brzozowski and Antimirov, for trace closures of regular word languages wrt. an independence relation on the alphabet. The Brzozowski and Antimirov style derivatives essentially define functional resp. relational small-step operational semantics of an (abstracted) sequential programming language where some instructions, given by the independence relation, can be reordered without any observable consequences. Our development is motivated by the fact that some aspects of relaxed memories can be explained by allowing the threads of a concurrent program to be reordered in this manner.

We consider Ribenboim’s construction of rings of generalized power series. Ribenboim’s construction makes use of a special class of partially ordered monoids and a special class of their subsets. While the restrictions he imposes might seem conceptually unclear, we demonstrate that they are precisely the appropriate conditions to represent such monoids as internal monoids in an appropriate category of Ehrhard’s finiteness spaces. Ehrhard introduced finiteness spaces as the objects of a categorical model of classical linear logic, where a set is equipped with a class of subsets to be thought of as finitary. Morphisms are relations preserving the finitary structure.

In the present work, we take morphisms to be partial functions preserving the finitary structure rather than relations. The resulting category is symmetric monoidal closed, complete and cocomplete. Any pair of an internal monoid in this category and a ring induces a ring of generalized power series by an extension of the Ribenboim construction based on Ehrhard’s notion of linearization of a finiteness space. We thus further generalize Ribenboim’s constructions. We give several examples of rings which arise from this construction, including the ring of Puiseux series and the ring of formal power series generated by a free monoid. This is joint work with Cockett, Jacqmin and Scott.

We'll also present some results of Beauvais-Fiesthauer, Dewan and Drummond on the embedding of topological spaces into finiteness spaces and discuss how this might be of use in the analysis of etale groupoids and their C*-algebras.

On utilise les régularités des morphismes de la catégorie cartésienne fermée des espaces cohérents probabilistes pour majorer une distance naturelle sur les (classes d'équivalence observationnelle) de termes de PCF probabilistes par une distance définissable dans le modèle.

Game semantics is the art of interpreting formulas (types) as games and proofs (programs) as strategies interacting in space and time with their environment. In order to reflect the interactive behaviour of programs, strategies are required to follow specific scheduling policies. Typically, in the case of a purely sequential programming language, the program (Player) and its environment (Opponent) play one after the other, in a strictly alternating way. In the case of a concurrent language, on the other hand, 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 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 flavors (alternating and non alternating) using the same categorical combinatorics, performed in the category of small categories.

Differential categories were introduce to provide a minimal categorical semantics for differential linear logic. However, there exists three approaches to axiomatizing the derivative by deriving transformations, coderelictions, and creation maps - long thought to be distinct notions. Recently, Blute, Cockett, Seely and myself have revisited the axioms of a differential category and showed that for categorical models of differential linear logic the three approaches are equivalent. Thus, there is only one notion of differentiation.

Les catégories différentielles ont été introduites afin de fournir une sémantique catégorique minime pour la logique linéaire différentielle. Cependant, il existe trois approches d'axiomatiser la dérivée par les “deriving transformations”, “coderelictions”, “creation maps” - considérés pendant longtemps comme des notions distinctes. Récemment, avec Blute, Cockett et Seely, nous avons revisité les axiomes d’une catégorie différentielle et démontré que pour les modèles catégoriques de logique linéaire différentielle, les trois approches sont équivalentes. Il y a donc qu’une seule notion de différentielle.

Rauszer's bi-intuitionistic propositional logic (BiInt) is the conservative extension of intuitionistic propositional logic (Int) with a connective dual to implication usually called 'exclusion'. A *standard-style* sequent calculus for BiInt is easily obtained by extending the multiple-conclusion sequent calculus of Int with exclusion rules dual to the implication rules. However, similarly to standard-style sequent calculi for modal logics like S5, this calculus is incomplete without the cut rule. Cut-freeness is achievable for sequent calculi with non-standard sequent forms. The *nested* and *labelled* calculi (Goré, Postniece; Pinto, Uustalu) were motivated by quite different intuitive considerations. Yet they turn out to be very close on the technical level: slightly adjusted towards each other, they can be made isomorphic.

This is joint work with Luís Pinto (Universidade do Minho).

I will introduce a method to lift monads on the base category of a fibration to its total category using codensity monads. This method, called codensity lifting, is applicable to various fibrations which were not supported by the speaker's previous method called categorical TT-lifting. After introducing the codensity lifting, we illustrate some examples of codensity liftings of monads along the fibrations from the category of preorders, topological spaces and extended psuedometric spaces. I will also talk about the liftings of algebraic operations to the codensity-lifted monads. If time permits, I will mention a characterisation of the class of liftings (along posetal fibrations with fibred small limits) as a limit of a certain large diagram.

(Joint work with Tetsuya Sato; presented in CALCO 2015)

Intersection Types are a well-known family of tools that characterise different notions of normalisation. We develop a general framework for building such systems from a notion of approximation, that allows to recover many well-known intersection type systems, as well as new systems, for every calculus that can be translated into linear logic. This construction uses in a crucial way Melliès and Zeilberger’s “type systems as functors” viewpoint, as well as an adapted Grothendieck construction.

Based on a joint work with Damiano Mazza and Pierre Vial.

Universal algebra uniformly captures various algebraic structures, by expressing them as equational theories or (abstract) clones. The ubiquity of algebraic structures in mathematics has also given rise to several variants of universal algebra, such as symmetric and non-symmetric operads, clubs, and monads. In this talk, I will present a unified framework for these cousins of universal algebra, or notions of algebraic theory.

First I will explain how each notion of algebraic theory can be identified with a certain monoidal category, in such a way that theories correspond to monoids. Then I will introduce a categorical structure underlying the definition of models of theories. In specific examples, it often arises in the form of oplax action or enrichment. Finally I will uniformly characterize categories of models for various notions of algebraic theory, by a double-categorical universal property in the pseudo-double category of profunctors.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Interaction morphisms

Tarmo Uustalu, Tallinn U of Technology

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

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

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

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

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

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

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

Les tableaux de Young portent une multiplication associative, décrite par l'algorithme de Schensted. Le monoïde ainsi obtenu est appelé plaxique. Il joue un rôle fondamental dans de nombreuses applications combinatoires et algébriques. On montrera que cette multiplication sur les tableaux est entièrement déterminée par un tressage sur l'ensemble (bien plus simple !) des colonnes. Ici un tressage est une solution ensembliste de l'équation de Yang-Baxter. Notre tressage s'inscrit également dans le cadre de la réécriture. Comme application, on identifiera la cohomologie de Hochschild du monoïde plaxique, qui résiste à toutes les approches classiques, à la cohomologie tressée des tableaux-colonnes, beaucoup plus accessible. Toutes les notions et constructions seront rappelées.

Plusieurs modèles de sémantique de jeux concurrents ont émergé ces dernières années. Dans ce travail, on se concentre sur certaines de ces approches, qui ont donné des modèles de CCS, du pi-calcul et du lambda-calcul non-déterministe. Un point commun informel mais saillant entre ces approches est que les stratégies innocentes sont définies commes les faisceaux pour la topologie de Grothendieck où les parties sont recouvertes par leurs vues. On propose ici de tisser un lien formel entre deux de ces approches au niveau des parties et des stratégies.

Program differences are pervasive in software development, but most of the time they are represented as textual differences with no regards to the syntactic nature of programming languages or their semantics. Thus, they may be hard to read and often fail to convey insight on the changes on semantics. Furthermore, such low-level, unstructured presentations are hard to reason about.

We present a formal framework to characterize differences between deterministic programs in terms of their small-step semantics. This language-agnostic framework defines the notion of /difference languages/ in which /oracles/—programs that relate small-step executions of pairs of program written in a same language—can be written, reasoned about and composed.

We illustrate this framework by instantiating it on a toy imperative language and by presenting several /difference languages/ ranging from trivial equivalence-preserving syntactic transformations to characterized semantic differences. Through those examples, we will present the basis of our framework, show how to use it to relate syntactic changes with their effect on semantics, how one can abstract away from the small-step semantics presentation, and discuss the composability of oracles.

This is joint work with Thibaut Girka (IRIF - MERCE) and David Mentré (MERCE)

Call-by name (CBN) and call-by-value (CBV) have been defined as the dual solutions to a critical pair at the heart of cut-elimination in classical sequent calculus. When one moves to intuitionistic logic, this symmetric picture breaks, but what happens precisely? How are such definitions adapted to the intuitionistic case? How do the resulting calculi relate to the many other proposals for intuitionistic CBV and CBN calculi? And what does that break of duality say about intuitionistic logic? We find that proof-theory alone distills new CBV and CBN lambda-calculi which agree, in a technical sense, with the computational lambda-calculus and the ordinary lambda-calculus, respectively; but the former distilled calculus is contained in the latter - a vindication of Plotkin. This containment, in turn, rests on another asymmetry: a certain permutative/focalization conversion, named T, solves what remains of the classical critical pair in favor of CBN, while the symmetric solution with a certain CBV conversion Q does not exist. In this sense we may say intuitionistic logic enjoys a CBN bias. Full answers to the above questions require us to work simultaneously with sequent calculus and its equivalent bidirectional natural deduction. The former syntax is our starting point, where we track the (lost) symmetries and find the idea of permutative conversions; the latter syntax is the bridge towards more traditional programming notations. For instance, only in bidirectional natural deduction one sees that T eliminates the difference between “let” and explicit substitution, and only there one understands what calling paradigm corresponds to the superimposition of CBN and CBV.

I will present AEON (Atomic Events and Ownership Networks), a programming model for safe and scalable cloud computing. AEON is based on the well-known paradigms of object-orientation and event-driven programming. AEON’s runtime system guarantees a linearizable and deadlock-free semantics for events that span across multiple objects and servers. Moreover, to achieve an economical and scalable solution, our runtime system provides seamless elasticity (the capability to adapt the resources usage to the actual workload), and exploits the object graph — the ownership network — to enhance parallelism. In this talk will concentrate on the safety aspects of the semantics of AEON, and show some experimental scalability results.

We prove a finite family developments theorem (FFD) for the calculus with explicit substitutions Linear Substitution Calculus (LSC). The notion of redex family is obtained by adapting Lévy labels to support the two distinctive features of LSC, namely its use of context rules that allow substitutions to act “at a distance” and also the set of equations modulo which it rewrites. We then apply FFD to prove a number of results for LSC including: an optimal reduction result, an algorithm for standardisation by selection, and normalisation of a linear call-by-need reduction strategy.

For years we have been bothered by a small mistery on categorical models of Linear Logic (star-autonomous categories) and Geometry of Interaction (compact closed categories, typically arising from traced monoidal categories via Int-construction): is there a proper intermediate structure between star-autonomous categories and compact closed categories, that is, a traced star-autonomous category which is not compact closed? We settle this issue by showing that any traced star-autonomous category is actually compact closed.

We also discuss what would happen if we remove symmetry, thus the following question: is there a non-symmetric star-autonomous category with a (suitably generalized) trace which is not pivotal? Our recent attempt suggests that the answer is again no, but the situation is much subtler than the symmetric case.

The result on the symmetric case is a joint work with Tamas Hajgato.

I will begin by presenting a structural description of the kind of empirical data which arises in physical experiments, using the language of sheaf-theory. A potential feature of such data is contextuality (including as a special case non-locality) which can be neatly characterised in this setting. The feature does not arise in classical data, and a number of recent results indicate that it is the key feature in enabling quantum advantages or speedups over classical behaviour in a variety of computational scenarios. The sheaf-theoretic perspective exposes a qualitative hierarchy of strengths of contextuality and I will also mention recent efforts to quantify contextuality via linear programming. Finally I will report on work in progress on developing a resource theory for contextuality, beginning with an algebra of empirical models under whose operations contextuality is monotonically decreasing.

In the usual deterministic lambda-calculus the confluence of the unique computation rule, the beta-reduction, makes it easy to turn the reduction into an equality, the beta-equivalence. This idea to consider not computation but equalities on terms gives rise to the notion of lambda-theory. On the other hand the probabilistic lambda-calculus is usually treated only in terms of computation. In particular we know that we must impose a reduction strategy for the probabilistic choice if we want the calculus to make sense.

In this talk we will recover this notion of presentation through equalities in the probabilistic lambda-calculus. We will show how some usual notions can be translated in the probabilistic world. In particular we will define a notion of probabilistic Böhm tree, and show a separability result. This will implies that just like in the deterministic setting the Böhm tree equality is the same as the observational equivalence.

The Krivine machine is an abstract machine implementing the linear head reduction of $\lambda$-calculus. Ehrhard and Regnier gave a resource sensitive version returning the annotated form of a $\lambda$-term accounting for the resources used by the linear head reduction. These annotations take the form of terms in the resource $\lambda$-calculus.

We generalize this resource-driven Krivine machine to the case of the algebraic $\lambda$-calculus. The latter is an extension of the pure $\lambda$-calculus allowing for the linear combination of $\lambda$-terms with coefficients taken from a semiring. Our machine associates a $\lambda$-term $M$ and a resource annotation $t$ with a scalar $\alpha$ in the semiring describing some quantitative properties of the linear head reduction of $M$.

In the particular case of non-negative real numbers and of algebraic terms $M$ representing probability distributions, the coefficient $\alpha$ gives the probability that the linear head reduction actually uses exactly the resources annotated by $t$. In the general case, we prove that the coefficient $\alpha$ can be recovered from the coefficient of $t$ in the Taylor expansion of $M$ and from the normal form of $t$.

Propositional dynamic logic (PDL) is at the core of reasoning about dynamic systems. We present a syntax directed formalism for PDL, built on coproofs.

Contrary to proofs, which are generated inductively top-down, coproofs are generated coinductively bottom-up, and may have infinite branches. However, our inference rules allow this only via state-changes, and as a result are sound.

We also prove the semantic completeness of our formalism, and apply it to obtain new interpolation theorems for PDL.

Il existe deux formalisations des langages/systèmes probabilistes: l'une est de considérer l'arbre des dérivations (avec branchements probabilistes), l'autre est de considérer des distributions de probabilités. Avoir accès à l'arbre de dérivation est pratique pour les preuves car on a accès à l'historique complet, mais lorsque l'arbre est infini, le formalisme est très lourd et peu explicite. La formulation à base de distributions est plus simple et donne des théorèmes élégants mais engendre des preuves très complexes (où il faut souvent retrouver l'historique du calcul). Dans cet exposé nous verrons qu'il est possible de récupérer le meilleur des deux mondes grâce à un théorème d'encodage probabilistique inspiré de la théorie catégorique des coalgèbres. Nous verrons qu'il s'agit d'un outil systématique qui, à l'instar de l'induction ou la coinduction, permet de structurer des preuves et des définitions complexes. Pour des raisons de temps, nous n'évoquerons que brièvement comment ce schéma de preuve nous permet de redéfinir une version probabiliste de notions usuelles telles que les types intersection probabilistes ou les candidats de réductibilité probabilistes.

Most standard models of the lambda calculus validate the principles of infinitary rewriting (which include identification of meaningless terms). For example, in Scott models, the interpretation of every fixed point combinator is equal to the limit (in the model) of interpretations of

\f.f(Ω), \f.f^2(Ω), \f.f^3(Ω), …, \f.f^n(Ω), ….

The infinite term \f.f(f(f…)) is the limit of the above sequence, and in the infinitary lambda calculus all fpcs reduce to this term, which is an infinitary normal form. It would seem natural to extend the interpretation function to cover infinitary terms as well, however, naive attempts to do this fail. The problem is already present in the first-order case: finite terms over a signature ∑ can be interpreted by means of the initial semantics – where the free algebra of terms admits a canonical homomorphism to any other ∑-algebra. However, the infinite terms are elements of the cofinal coalgebra, which universal property concerns maps INTO the algebra, rather than out of it. We are thus faced with a “koan”:

• What does it mean to interpret infinite terms?*

While we shall not provide a (co)final solution to this koan, we will offer germs of some possible approaches, with the hope of starting a discussion that could follow this short talk.