Mardi 5 Septembre
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
On the shape of random Pólya structures |
Description: |
Michael Wallner |
Mardi 19 Septembre
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
TBA |
Description: |
Valentin Bonzom |
Vendredi 22 Septembre
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Circular Proofs for Subtyping and Termination |
Description: |
Rodolphe Lepigre In a recent (submitted) work with Christophe Raffalli, we designed a rich type system for an extension of System F with subtyping. It includes primitive sums and products, existential types, and (co-)inductive types. Using a combination of (pointed) subtyping and circular proofs, we were able to express the system with typing and subtyping rules that are syntax-directed (up to circularity). During my talk, I will try to give you a flavour of the techniques we used. In particular, I will show how choice operators can be used to get rid of typing contexts, and to allow the commutation of quantifiers with other connectives. I will then introduce the circular proof framework that is used for handling inductive and co-inductive types in subtyping rules, and general recursion in typing rules. |
Vendredi 13 Octobre
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Smooth models of Differential Linear Logic |
Description: |
Marie Kerjean Differential Linear Logic was constructed following a study of discrete vectorial models of Linear Logic. We want to extend the semantics of Linear Logic in the natural domain of continuous objects and analysis. From the basic fact that Seely's formulas is the direct interpretation of the Kernel Theorem for distributions, we explain two developments :
On one hand we axiomatize a Smooth Differential Linear Logic with a graded syntax where to each solvable Linear partial differential equation one associate an exponential. We construct a model of nuclear Fréchet/ Df spaces for this syntax.
On the other hand, we argue that the interpretation of the $parr$ as Schwartz's epsilon product should be the cornestone of the construction of a smooth classical model of DiLL. From a first-model of $k$-reflexive spaces, and based on pioneering works by Kriegl, Michor and Meise, we construct a variety of (at least two) new models of DiLL. This part is joint work with Y. Dabrowski. |
Vendredi 20 Octobre
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Inlining après l'élimination de fermeture pour OCaml |
Description: |
Pierre Chambart Usuellement, dans les langages de haut niveau, l'inlining est fait sur un langage intermédiaire proche d'un lambda calcul, où celà revient pour les cas simple à de la beta-réduction. Pour diverses raisons, dans OCaml, nous avons décidé d'introduire un autre langage intermédiaire où les fermetures sont explicite (flambda) sur lequel les optimisations haut niveau sont effectuées. Nous discuterons des avantages et complexités qui viennent avec ce choix. |
Mardi 24 Octobre
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Bijections for Weyl Chamber walks ending on an axis, and arc diagrams |
Description: |
Mathias Lepoutre |
Heure: |
15:30 - 18:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
False Beliefs in mathematics |
Description: |
thé combinatoire |
Mardi 7 Novembre
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Combinatorial physics. TBC |
Description: |
Joseph Ben Geloun |
Mercredi 8 Novembre
Heure: |
15:00 - 16:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Formal language theory beyond trees and forests |
Description: |
Tobias Heindel The talk presents the theorems of Myhill-Nerode and Chomsky-Schützenberger, replacing trees and words by rewriting diagrams of semi-Thue systems, which are the paradigm example of planar acyclic circuit diagrams (PLACIDs)---the graphical syntax of monoidal categories. The talk will focus on the proposal of a definition of recognizable language in monoidal categories, namely sets of arrows that coincide with the inverse image of their direct image under a monoidal functor to a finite monoidal category. For the case of PLACIDs, this class of languages is shown to coincide with the languages of automata in the sense of Bossut, under modest assumptions on gates of circuit diagrams; moreover, the usual notion of recognizable tree language is recovered. The talk presents the Myhill-Nerode theorem as a tool for solving Bossut's open problem of automata complementation. The remainder of the talk describes work in progress and future work, in particular the Chomsky-Schützenberger theorem for PLACIDs. |
Mardi 14 Novembre
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Tilings. TBA |
Description: |
Michaël Rao |
Heure: |
15:45 - 18:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
False Beliefs in mathematics |
Description: |
thé combinatoire |
Jeudi 16 Novembre
Heure: |
10:00 - 11:00 |
Lieu: |
Salle A303 ? , Université de Villetaneuse |
Résumé: |
[Réunion] réunion d'équipe Axe LO |
Description: |
Stefano Guerrini Réunion |
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Réseaux de preuve pour MLL+Mix et algorithmes sur les graphes arêtes-coloriés |
Description: |
Nguy?n Lê Thành D?ng Le critère de correction de Danos-Regnier mène à poser le problème d'algorithmique des graphes suivant : étant donné un graphe apparié, trouver un cycle (ou un chemin) passant au plus une fois par chaque paire. Ce problème a été traité en théorie des graphes sous la forme plus générale de graphes munis d'une coloration sur leurs arêtes ("edge-colored graphs") ; la solution fait intervenir une réduction aux couplages parfaits et rejoint donc le travail de C. Retoré sur les "handsome proof-nets". Partant de cela, on obtient facilement d'une part un critère de correction pour MLL+Mix en temps linéaire, et d'autre part que le problème de correction des réseaux MLL+Mix est probablement plus difficile que celui pour MLL sans la règle Mix (qui est NL-complet). Ce dernier résultat explique que la littérature sur les critères de correction pour MLL+Mix soit plus maigre que celle pour MLL. Nous verrons également d'autres conséquences de ces liens entre logique linéaire et théorie des graphes, notamment en lien avec le graphe de dépendances d'un réseau introduit par Bagnol, Doumane et Saurin. |
Vendredi 17 Novembre
Heure: |
14:15 - 16:30 |
Lieu: |
amphi Copernic, Université de Villetaneuse |
Résumé: |
[soutenance] Polyadic Approximations in Logic and Computation |
Description: |
Damiano Mazza |
Lundi 20 Novembre
Heure: |
15:00 - 16:00 |
Lieu: |
Salle A303, bâtiment A, campus de Villetaneuse |
Résumé: |
Séminaire SV : Fadwa Rekik |
Description: |
Fadwa Rekik Larchitecture orientée service (SOA) est un paradigme qui offre des mécanismes permettant une grande flexibilité des architectures des systèmes logiciels tout en réduisant leurs coûts de développement puisquelle se base sur des entités modulaires et réutilisables appelées services. Ces services peuvent être réutilisés dans le cadre dune composition ou dune chorégraphie de services pour la construction de nouveaux processus métiers transverses. De son côté, le paradigme de lIngénierie Dirigé par les Modèles (IDM) offre au travers de ses deux principes fondateurs, labstraction et lautomatisation, deux moyens puissants de gestion de la complexité sans cesse croissante des systèmes. Combiner les deux paradigmes et concevoir ainsi une approche de type SOA dirigée par les modèles semble une piste prometteuse. Cependant, malgré les progrès de lapplication des principes de lIDM la spécification et le développement des applications SOA, plusieurs problèmes restent à résoudre. Un de ces problèmes est deffectuer une vérification rigoureuse des modèles de spécification des applications orientées services. Ces modèles sont généralement composés de plusieurs vues sémantiquement liées les unes aux autres. Un deuxième problème est la transformation de ces modèles de spécification en code exécutable. En particulier, les chorégraphies de service doivent être transformées en orchestrations exécutables tout en préservant la sémantique des scénarios de haut niveau décrits par ces chorégraphies et en tenant compte des aspects critiques inhérents aux systèmes distribués tels que lasynchronisme. La vérification de l'exécution est aussi nécessaire afin de détecter les comportements erronés lors de lexécution. Pour relever ces défis, nous proposons une approche SOA dirigée par les modèles qui repose sur le standard OMG SoaML. Lors de la spécification, la cohérence des modèles SoaML est vérifiée en utilisant la validation statique des modèles moyennant des règles OCL que nous avons définies. Nous avons spécifié également des règles de transformation pour permettre la génération automatique d'artefacts exécutables. Enfin, nous avons défini un cadre de test à base de modèles pour vérifier la conformité de lexécution des chorégraphies de services, incluant les orchestrateurs générés, aux modèles de spécification. L'ensemble de notre méthode a été outillé en extension de loutil de modélisation UML, Papyrus, et de loutil danalyse formelle, Diversity. |
Mardi 21 Novembre
Heure: |
11:00 - 14:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
On the polynomial part of a restricted partition function |
Description: |
Karl Dilcher We prove an explicit formula for the polynomial part of a restrictedpartition function, also known as the first Sylvester wave. This isachieved by way of some identities for higher-order Bernoulli polynomials,one of which is analogous to Raabe's well-known multiplication formula forthe ordinary Bernoulli polynomials. As a consequence of our main result weobtain an asymptotic expression of the first Sylvester wave as thecoefficients of the restricted partition grow arbitrarily large.(Joint work with Christophe Vignat). |
Heure: |
14:45 - 17:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Euler Polynomials and Identities for Non-Commutative Operators |
Description: |
Christophe Vignat |
Heure: |
15:30 - 18:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
False Beliefs in mathematics |
Description: |
thé combinatoire |
Vendredi 24 Novembre
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
A discussion on the conjectures NP vs PSPACE and NP vs coNP |
Description: |
Hermann Hauesler The aim of this talk is to open a discussion on the justification of the conjectures NP = coNP and NP = PSPACE by means of purely proof-theoretical arguments. |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
[répétition] répétition de soutenance de thèse |
Description: |
Thomas Rubiano |
Mardi 28 Novembre
Heure: |
10:00 - 13:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Journée 'flips': Alexander Pilz, Thomas Budzinski, Lionel Pournin, Thomas Fernique |
Description: |
Journée MathStic |
|
|