### Preuves, programmes et systèmes

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

** Responsables :** Claudia Faggian, Jean Krivine et Alexis Saurin

Jeudi 15 juin 2017 · 10h30 · Salle 3052

Samuele Giraudo (Paris-Est Marne-la-Vallée) · Découpage d'associativité généralisé

Mardi 09 mai 2017 · 14h00 · Salle 3052

Valentin Blot (Queen Mary University, London) · An interpretation of system F through bar recursion

Jeudi 27 avril 2017 · 10h30 · Salle 3052

Bérénice Delcroix-Oger (Institut de Mathématiques de Toulouse) · Des arbres sans ambiguités

Jeudi 27 avril 2017 · 14h00 · Salle 3052

Jeremy Siek (Indiana University) · The state of the art in gradual typing

Jeudi 20 avril 2017 · 10h30 · Salle 3052

Jamie Vicary (Univ. of Oxford) · Formalizing Compositional Proofs

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

Jeudi 30 mars 2017 · 10h00 · Salle 3052

Giovanni Bernardi (IRIF) · Un, personne et cent mille: a meta theory for testing equivalences?

Jeudi 30 mars 2017 · 11h15 · Salle 3052

Daniela Petrisan (IRIF) · Hybrid set-vector automata from a category-theoretic perspective

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.

Jeudi 23 mars 2017 · 10h30 · Salle 3052

Thomas Leventis (Institut de Mathématiques de Marseille) · Full Abstraction of the Probabilistic Böhm Trees

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.

Jeudi 16 mars 2017 · 10h30 · Salle 3052

Charles Grellois (INRIA - Univ. Bologna (Italie)) · Verifying properties of functional programs: from the deterministic to the probabilistic case

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

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

[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

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

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

Jeudi 06 octobre 2016 · 10h30 · Salle 3052

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

Jeudi 29 septembre 2016 · 10h30 · Salle 3052

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

Jeudi 02 juin 2016 · 10h30 · Salle 3052

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

Jeudi 21 avril 2016 · 10h30 · Salle 3052

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

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

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

- 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*