Preuves, programmes et systèmes
Jeudi 14 décembre 2017, 10 heures 30, ENS Lyon
Séminaire Chocola ENS Lyon
Preuves, programmes et systèmes
Jeudi 14 décembre 2017, 10 heures 30, Salle 3052
Juliusz Chroboczek (IRIF, Université Paris Diderot) Homenet, l'IETF, et le processus de normalisation
Depuis plusieurs années, je participe au groupe de travail Homenet de
l'IETF, l'organisme qui définit les normes qui régissent l'Internet. Dans
cet exposé, sur l'exemple de Homenet et de mes aventures à l'IETF,
j'essaierai de donner une idée de ce qu'est le processus de normalisation,
pourquoi il est important pour l'Informatique et pour l'Internet.
Cet exposé est une version étendue et légèrement censurée de l'exposé que
j'ai donné aux Journées PPS le 12 octobre 2017.
Preuves, programmes et systèmes
Jeudi 7 décembre 2017, 10 heures 30, Salle 3052
Charles Grellois (Université Aix-Marseille) Linearity in Higher-Order Recursion Schemes
In higher-order model-checking (HOMC), functional programs are represented as higher-order recursion schemes (HORS), a kind of grammar with parameters which can be functions. These grammars generate infinite trees, over which we want to check formulas of monadic second-order logic (MSO). This problem is decidable, as proved first by Ong in 2006, and then by many others including Kobayashi and Ong (2009) whose approach use intersection types. It turns out that linear logic is a powerful and enlightening tool to reason about HOMC, as shown by Grellois and Melliès in the last years.
In general, the complexity of the HOMC problem is n-EXPTIME, where n is the order of the HORS of interest. In this talk, we explain that we can refine this complexity measure: motivated by linear logic, we introduce *linear* HORS and a linear-nonlinear model of automaton checking fragments of MSO. We then show that HOMC is in fact n-EXPTIME complete for n the *linear* order of the linear HORS generating the tree of interest. We believe that this explains why HOMC, in spite of its huge theoretical complexity, has been successfully used in practice by Kobayashi's team.
This linear framework allows to reprove in a much simpler way three existing results extending the usual HOMC problem, and notably to deal with call-by-value programs in a smooth way (the usual HOMC approach considering call-by-name).
This is joint work with Pierre Clairambault and Andrzej Murawski.
Preuves, programmes et systèmes
Jeudi 23 novembre 2017, 10 heures 30, Salle 3052
Simon Castellan (Imperial College) The parallel intensionally fully abstract model for PCF
In this talk, we introduce a new game semantics framework for
concurrency based on event structures, extending the work of Rideau and
Winskel. In this framework, we can extend the notions of innocence and
well-bracketing to the concurrent (and non-deterministic) case,
generalizing the so-called “Abramsky cube”.
This talk focuses on the deterministic case. I will first introduce the
concurrent strategies and their composition, in the existing linear
setting. I will then present our extension to nonlinearity using copy
indices and symmetry to represent uniformity. I will then present our
notions of concurrent innocence & well-bracketing, to finish on our
result of intensional full abstraction for PCF. Time permitting, I will
discuss extensions of this result to non-angelic nondeterminism and
probabilities.
Preuves, programmes et systèmes
Jeudi 9 novembre 2017, 10 heures 30, ENS Lyon
Séminaire Chocola ENS LYon
Preuves, programmes et systèmes
Jeudi 19 octobre 2017, 10 heures 30, Salle 3052
Martin Hyland (DPMMS, University of Cambridge) Understanding Computation in Game Semantics
Preuves, programmes et systèmes
Jeudi 15 juin 2017, 10 heures 30, Salle 3052
Samuele Giraudo (Paris-Est Marne-la-Vallée) Découpage d'associativité généralisé
Les algèbres dendriformes sont des structures algébriques introduites
par Loday. Elle offrent un moyen de découper un produit associatif en
deux produits non nécessairement associatifs. L'étude de ces algèbres,
réalisée avec le point de vue fourni par la théorie des opérades, fait
apparaître la combinatoire des arbres binaires et des mélanges d'arbres.
Nous définissons ici une opérade à un paramètre entier généralisant
l'opérade diassociative. Par dualité de Koszul, nous obtenons des
généralisations de l'opérade dendriforme. Les algèbres sur ces opérades
permettent de découper un produit associatif en plusieurs parties, avec
certaines relations de compatibilité. Les propriétés combinatoires et
algébriques de ces structures sont passées en revue.
Preuves, programmes et systèmes
Mardi 9 mai 2017, 14 heures, Salle 3052
Valentin Blot (Queen Mary University, London) An interpretation of system F through bar recursion
There are two possible computational interpretations of second-order
arithmetic: Girard's system F or Spector's bar recursion and its
variants. While the logic is the same, the programs obtained from these
two interpretations have a fundamentally different computational
behavior and their relationship is not well understood. We make a step
towards a comparison by defining the first translation of system F into
a simply-typed total language with a variant of bar recursion. This
translation relies on a realizability interpretation of second-order
arithmetic. Due to Gödel's incompleteness theorem there is no proof of
termination of system F within second-order arithmetic. However, for
each individual term of system F there is a proof in second-order
arithmetic that it terminates, with its realizability interpretation
providing a bound on the number of reduction steps to reach a normal
form. Using this bound, we compute the normal form through primitive
recursion. Moreover, since the normalization proof of system F proceeds
by induction on typing derivations, the translation is compositional.
The flexibility of our method opens the possibility of getting a more
direct translation that will provide an alternative approach to the
study of polymorphism, namely through bar recursion.
Preuves, programmes et systèmes
Jeudi 27 avril 2017, 10 heures 30, Salle 3052
Bérénice Delcroix-Oger (Institut de Mathématiques de Toulouse) Des arbres sans ambiguités
Les tableaux boisés sont des objets combinatoires intervenant notamment dans l'étude de certains modèles de mécanique statistique.
Cet exposé porte sur les arbres non ambigus, qui sont un cas particulier de tableaux boisés reliés aux permutations ayant leurs excédences (w(i)>i) en début de mot. Nous avons obtenu, lors d'un travail commun avec J.-C. Aval, A. Boussicault, F. Hivert et P. Laborde-Zubieta, des résultats énumératifs et bijectifs sur ces objets, que je présenterai ici après avoir introduit le cadre de cette étude.
Preuves, programmes et systèmes
Jeudi 27 avril 2017, 14 heures, Salle 3052
Jeremy Siek (Indiana University) The state of the art in gradual typing
Gradual typing is an approach for designing programming languages that
integrate static and dynamic type checking. Gradual typing gives the
programmer fine-grained control over which regions of a program are
statically checked and which regions are dynamically checked. Over
the last decade, there has been renewed interest in such an
integration partly due to the rise in popularity of dynamic languages.
But as small programs grow into large programs, so does the need for
early error detection and modularity, which is provided by static type
checking. Gradual typing provides a practical migration path for
dynamically typed programs to become more statically typed. This talk
will give a glimpse at the state of the art in gradual typing. It will
describe a) the major challenges in the design and implementation of
gradually typed languages, b) the research that has addressed many of
of these challenges, and c) the open problems that need to be solved.
The research in gradual typing spans both theoretical and practical
questions, from mechanized metatheory to efficient compilation.
Jeremy Siek is an Associate Professor at Indiana University
Bloomington. Jeremy's areas of research include programming language
design, type systems, mechanized theorem proving using proof
assistants, and optimizing compilers. Jeremy's Ph.D. thesis explored
foundations for constrained templates, aka the “concepts” proposal for
C++. Prior to that, Jeremy developed the Boost Graph Library, a C++
generic library for graph algorithms and data structures. Jeremy
post-doc'd at Rice University where he developed the idea of gradual
typing: a type system that integrates both dynamic and static typing
in the same programming language. Jeremy is currently working on a
gradually-typed version of Python. Jeremy received the NSF CAREER
award to fund his project: “Bridging the Gap Between Prototyping and
Production”. Jeremy was also twice awarded a Distinguished Visiting
Fellowship from the Scottish Informatics & Computer Science Alliance.
Preuves, programmes et systèmes
Jeudi 20 avril 2017, 10 heures 30, Salle 3052
Jamie Vicary (Univ. of Oxford) Formalizing Compositional Proofs
I will present a new proof assistant, Globular, which allows the
formalization of compositional proofs in higher category theory. The
interface is geometrical, with proofs depicted as string diagrams, and
allowing direct click-and-drag manipulation of proofs in a simple and
intuitive way, up to the level of 4-categories. I will show how to
build a simple proof from scratch, and present some sophisticated
formalized proofs from topology and algebra. I will also give some
details of the theoretical basis, which gives a new and simple way to
understand higher category theory. This talk will be accessible, and
will not require any previous knowledge.
Web site: https://ncatlab.org/nlab/show/Globular
Paper: https://arxiv.org/abs/1610.06908
Preuves, programmes et systèmes
Jeudi 30 mars 2017, 10 heures, Salle 3052
Giovanni Bernardi (IRIF) Un, personne et cent mille: a meta theory for testing equivalences?
Testing theory focuses on contextual equivalences
that were proposed in the 80s as an alternative
to bisimulation equivalence.
During the last decade testing equivalences proved
useful in constructing semantic models
of session types and in laying the foundations of
web-service technologies. As result, testing theory
is more useful and richer than ever.
In this seminar I will recall the chief ideas behind
testing theory, and argue that we lack
a general methodology to reason on testing equivalences.
I will also outline the evidence that a meta-theory
may exist, and some open questions.
Preuves, programmes et systèmes
Jeudi 30 mars 2017, 11 heures 15, Salle 3052
Daniela Petrisan (IRIF) Hybrid set-vector automata from a category-theoretic perspective
The main purpose of this talk is to introduce a new automata
model, hybrid set-vector automata, that naturally embed deterministic
finite state automata and finite automata weighted over a field.
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.
Preuves, programmes et systèmes
Jeudi 23 mars 2017, 10 heures 30, Salle 3052
Thomas Leventis (Institut de Mathématiques de Marseille) Full Abstraction of the Probabilistic Böhm Trees
A very natural notion of equivalence of programs is the observational equivalence: two programs are equivalent if they have the same behaviour in any environment. More specifically in the lambda-calculus two terms M and N are equivalent if for every context C, the terms C[M] and C[N] are either both solvable or both unsolvable. Respecting this equivalence is an important property of some models of the lambda-calculus, called the full abstraction. It is well known that the model of infinitely extensional Böhm trees is fully abstract. The question we are interested in is what becomes of these notions when we introduce probabilistic choice in the calculus.
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.
Preuves, programmes et systèmes
Jeudi 16 mars 2017, 10 heures 30, Salle 3052
Charles Grellois (INRIA - Univ. Bologna (Italie)) Verifying properties of functional programs: from the deterministic to the probabilistic case
In functional programs, also called higher-order programs, functions may take functions themselves as arguments. As a result, their model-checking relies in most approaches on semantic or type-theoretic tools. In this talk, I will explain how an analysis based on linear logic of a model-checking result of 2009 by Kobayashi and Ong led Melliès and I to the construction of a model for model-checking. This model is such that, when interpreting a term with recursion representing the tree of traces of a functional program, its denotation determines whether it satisfies a MSO property of interest. A related and similar model was obtained independently by Salvati and Walukiewicz.
In the second part of the talk, I will discuss the verification of termination for functional programs with recursion and probabilistic choice. Dal Lago and I defined recently a type system which is such that typable programs terminate with probability 1. In other terms, their set of diverging executions is negligible. If time allows, I will sketch ideas towards an extension of the model-checking results of the deterministic case to quantitative logics and functional programs with recursion.
Preuves, programmes et systèmes
Jeudi 23 février 2017, 10 heures 30, 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.
Preuves, programmes et systèmes
Jeudi 26 janvier 2017, 10 heures 30, 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.
Preuves, programmes et systèmes
Mardi 10 janvier 2017, 11 heures, Salle 3052
Camell Kachour (IRIF) Sur des modèles algébriques d'infini-n-catégories faibles cubiques