### Preuves, programmes et systèmes

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

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

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*