Preuves, programmes et systèmes

Date et lieu : le jeudi à 10h30, salle 3052, Sophie Germain

Responsables : Claudia Faggian, Jean Krivine et Alexis Saurin

Jeudi 23 février 2017 · 10h30 · Salle 3052

Marcelo Fiore (University of Cambridge) · An Algebraic Combinatorial Approach to the Abstract Syntax of Opetopic Structures

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.

Jeudi 26 janvier 2017 · 10h30 · Salle 3052

Tarmo Uustalu (Tallinn University of Technology) · Dynamic programming and coalgebras with sharing

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.

Mardi 10 janvier 2017 · 11h00 · Salle 3052

Camell Kachour (IRIF) · Sur des modèles algébriques d'infini-n-catégories faibles cubiques

Jeudi 01 décembre 2016 · 10h30 · Salle 3052

Julien Lange (Imperial College) · Building Graphical Choreographies From Communicating Machines: Principles and Applications

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.

Jeudi 24 novembre 2016 · 10h30 · Salle 3052

Thibaut Balabonski (LRI, Université Paris Sud) · Optimisation de programmes C++ concurrents

Jeudi 17 novembre 2016 · 10h30 · Salle 3052

Bruno Barras · Exposé repoussé à début 2017

Jeudi 03 novembre 2016 · 10h30 · Salle 3052

Guilhem Jaber (IRIF) · Operational Nominal Game Semantics

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).

Jeudi 06 octobre 2016 · 10h30 · Salle 3052

Giulio Manzonetto (LIPN) · New Results on Morris's Observational Theory — The Benefits of Separating the Inseparable

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.

Jeudi 29 septembre 2016 · 10h30 · Salle 3052

Vincent Danos (ENS) · Bayesian inversion by ω-complete cone duality

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

Jeudi 02 juin 2016 · 10h30 · Salle 3052

Ugo Dal Lago (Univ. Bologna) · Infinitary Lambda Calculi from a Linear Perspective

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.

Jeudi 21 avril 2016 · 10h30 · Salle 3052

Silvia Ghilezan (Université de Novi Sad) · Preciseness of Subtyping on Intersection and Union Types

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.

Mercredi 30 mars 2016 · 10h30 · Salle 3052

Guillaume Munch-Maccagnoni (Cambridge Computer lab) · Enriched-adjunction models and polarisation for modelling effects and resources

(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.

Jeudi 24 mars 2016 · 10h30 · Salle 3052

Pawel Sobocinski (University of Southampton) · TBA

Jeudi 10 mars 2016 · 10h30 · Salle du Conseil

Thomas Seiller (Department of Computer Science, University of Copenhagen - DIKU) · Complexity Constraints as Group Actions

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.

Jeudi 14 janvier 2016 · 10h30 · Salle 3052

Amar Hadzihasanovic (Oxford University) · String diagrams and the algebra of entanglement

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.

  • Jeudi 17 décembre : Jean-Marie Madiot (Princeton University), Bisimulations up-to: beyond first-order transition systems
  • Jeudi 26 novembre : Fabio Zanasi (Radboud University of Nijmegen, Netherlands), Interacting Hopf Algebras - the theory of linear systems
  • Jeudi 19 novembre : Beniamino Accattoli (INRIA), Proof nets and the lambda-calculus 2.0
  • Jeudi 5 novembre : double séminaire
    • 10h30 : Russell Harmer (ENS Lyon), Executable knowledge
    • 14h00 : Luca Padovani (Torino, Italy), The Chemical Approach to Typestate-Oriented Programming
  • Jeudi 17 septembre : Stéphane Graham-Lengrand (LIX), Non-idempotent intersection types and quantitative information about reduction paths: a survey
  • Jeudi 10 septembre : Christian Schulte (School of ICT, KTH Royal Institute of Technology, and Swedish Institute of Computer Science, Sweden), Modeling and Solving Code Generation for Real