### Sémantique

** Date et lieu :** le mardi à 11h, salle 3052, Sophie Germain

** Responsable :** Paul-André Melliès et Michele Pagani

Mardi 21 mars 2017 · 14h00 · Salle 3052

Jean-Bernard Stefani (INRIA) · Location graphs

Mardi 28 février 2017 · 11h00 · Salle 3052

Ran Chen ^{1)} · Strongly Connected Components in graphs, formal proof of Tarjan1972 algorithm

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.

Mardi 24 janvier 2017 · 11h00 · Salle 3052

Arnaud Spiwack (Tweag I/O) · Retrofitting linear types

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.

Vendredi 13 janvier 2017 · 14h00 · Salle 3052

Tarmo Uustalu (Tallinn University of Technology) · 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).

Mardi 10 janvier 2017 · 11h00 · Salle 3052

Fanny He (Université de Bath, UK) · The atomic lambda-mu-calculus

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.

Mercredi 21 décembre 2016 · 11h00 · Salle 3052

Victoria Lebed (Trinity College, Dublin) · Que savent les tresses sur les tableaux de Young ?

Mardi 20 décembre 2016 · 11h00 · Salle 3052

Clovis Eberhart (LAMA, Chambéry) · Séquences justifiées et diagrammes de cordes : deux approches de la sémantique de jeux concurrents

Mardi 06 décembre 2016 · 11h00 · Salle 3052

Yann Régis-Gianas (IRIF) · Explaining Program Differences Using Oracles

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)

Mardi 15 novembre 2016 · 11h00 · Salle 3052

José Espírito Santo (University of Minho) · Call-by-name, call-by-value and intuitionistic logic

Mardi 08 novembre 2016 · 11h00 · Salle 3052

Gustavo Petri (IRIF) · Safe and Scalable Cloud Programming

Mardi 18 octobre 2016 · 10h30 · Salle 3052

Pablo Barenbaum (Université de Buenos Aires - CONICET) · Finite Family Developments for the Linear Substitution Calculus

Mardi 18 octobre 2016 · 11h30 · Salle 3052

Masahito Hasegawa (Research Institute in Mathematical Sciences (RIMS)) · Traced star-autonomous categories are 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.

Mardi 05 juillet 2016 · 11h00 · Salle 3052

Shane Mansfield (IRIF) · Empirical Models and Contextuality

Mardi 07 juin 2016 · 11h00 · Salle 3052

Thomas Leventis (I2M Marseille) · Probabilistic lambda-theories

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.

Mardi 07 juin 2016 · 10h00 · Salle 3052

Antoine Allioux (IRIF) · Krivine machine and Taylor expansion in a non-uniform setting

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

Mardi 17 mai 2016 · 11h00 · Salle 3052

Daniel Leivant (Indiana University Bloomington) · Syntax directed coproofs for Propositional Dynamic Logic

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.

Jeudi 07 avril 2016 · 16h00 · Salle 3052

Flavien Breuvart (INRIA Focus (Université de Bologna, IT)) · L'encodage probabiliste: vers une formalisation systématique des langages probabilistes, déterministiques et potentiellement divergents.

Mardi 29 mars 2016 · 10h30 · Salle 3052

Andrew Polonsky (IRIF) · Interpreting infinite terms

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

^{1)}Inria