- Gdtlogprog - Listes du LIPN

Gdt de Paulin annulé
by Damiano Mazza 22 Jan '19

22 Jan '19

Bonjour, Suite aux intémperies et l'absence de plusieurs personnes, nous avons décidé de reporter l'exposé de Paulin prévu ce matin à une date ultérieure, qui sera fixée au plus vite. Amicalement, Damiano

1 0

Thomas Seiller, 22/06/2018 13:30
by Flavien Breuvart 21 Jun '18

21 Jun '18

Bonsoir, Il n'y aura pas de séminaire demain, par contre, Thomas donne un groupe de travail à 13h30 sur la GOI et les graphages. à demain, Flavien

1 0

Antoine Kaszczyc, 27/10/2017 11:00
by Flavien Breuvart 25 Oct '17

25 Oct '17

Les personnes qui seront présente peuvent-elles se manifester rapidement? Avec les vacances, je voudrait être sur qu'il y a un peu de monde... *Eviter le dépassement de mémoire avec la monade Etat en OCaml* [Intervenant] Antoine Kaszczyc, LIPN [Localisation] Salle B107, bâtiment B, Université de Villetaneuse [Date] 27/10/2017 11:00 - 12:00 [Description] Résumé : Selon une configuration classique, avec une implémentation classique de la monade Etat en OCaml, on obtient normalement une "stack overflow" au bout d'un million de compositions avec "bind". On va voir pourquoi ça arrive, et comment l'éviter avec des continuations. Ensuite on verra que cela n'est pas suffisant si on utilise en même temps la monade Writer. On verra alors un compromis sous forme de "bind répétitif". Si quelqu'un a des idées de solutions, elles sont bienvenues. ----------------------------------

1 1

[SEMINAIRE LCR] Damiano Mazza, 23/06/2017 11:00
by breuvart 21 Jun '17

21 Jun '17

PETITE INTRODUCTION À LA LOGIQUE CATÉGORIQUE Damiano Mazza, LIPN Salle B107, bâtiment B, Université de Villetaneuse 23/06/2017 11:00 - 12:30 Résumé : On entend dire parfois que le lambda-calcul est "le langage interne des catégories cartesiennes fermées". Le "langage interne" d'une catégorie est une notion très générale (mais, à vrai dire, pas tout à fait formelle) de logique catégorique. Dans cet exposé, j'introduirai les concepts de base pour comprendre cette notion et expliquer comment elle est reliée à la sémantique dénotationnelle.

1 0

Fwd: [SEMINAIRE LCR] Hadrien Batmalle, 16/06/2017 11:00
by breuvart 13 Jun '17

13 Jun '17

BAR-RÉCURSION, ANALYSE ET RÉALISABILITÉ CLASSIQUE Hadrien Batmalle, IRIF Salle B107, bâtiment B, Université de Villetaneuse 16/06/2017 11:00 - 12:30 Résumé : La réalisabilité classique est une théorie née des travaux de Jean-Louis Krivine dans les années 1990, à la frontière entre la logique et l'informatique théorique. Côté informatique, elle offre un cadre adapté à l'interprétation calculatoire de preuves classiques. Côté logique, elle apparaît comme une généralisation prometteuse du forcing de Cohen. À un modèle du lambda-calcul, on peut ainsi associer un modèle de la théorie des ensembles ZF. On s'intéresse ici à des modèles de programmation vérifiant une propriété de continuité: il peut s'agir de modèles basés sur les domaines de la sémantique dénotationnelle, ou bien de modèles de termes d'une version infinitaire du lambda-calcul. Dans ces modèles, l'instruction 'quote' (qu'on utilise usuellement en réalisabilité classique pour interpréter l'axiome du choix dépendant) n'est pas disponible. On utilise donc la technique de la bar-récursion pour interpréter l'axiome du choix dépendant. Or (en considérant la réalisabilité classique comme une généralisation du forcing), il apparaît que la bar-récursion est de plus l'analogue de la condition de chaîne descendante dans les algèbres de forcing (qui correspond à une propriété de préservation des réels). On obtient alors que toute formule de l'analyse vraie dans le modèle ambiant est réalisée dans ces nouveaux modèles, ce qui nous amène à la question suivante: quel est le comportement des programmes réalisant des formules de l'analyse?

1 0

Valentin Blot, 09/06/2017 11:00
by breuvart 09 Jun '17

09 Jun '17

AN INTERPRETATION OF SYSTEM F THROUGH BAR RECURSION Valentin Blot, Queen Mary University of London Salle B107, bâtiment B, Université de Villetaneuse 09/06/2017 11:00 - 12:30 Résumé : 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.

1 1

Re: [GdT Log&Prog] [Séminaire ouvert LCR] Jérémy Dubut, 19/05/2017 11:00
by breuvart 19 May '17

19 May '17

C'est maintenant Le 2017-05-17 14:56, breuvart a écrit : > Le séminaire d'équipe LCR du LIPN de ce vendredi (ci-dessous) pourra > potentiellement intéresser au delà. Toute participation extérieure est > la bienvenue. > > > Directed homology theories for geometric models of true concurrency > > Jérémy Dubut, LSV (ENS Cachan) > > Salle B107, bâtiment B, Université de Villetaneuse > > 19/05/2017 11:00 - 12:30 > > Résumé : > > Studying a system through its geometry is the main purpose of directed > algebraic topology. This topic emerged in computer science, more > particularly in true concurrency, where Pratt introduced his higher > dimensional automata (HDA) in 1991 (actually, the idea of geometry of > concurrency can be tracked down Dijkstra in 1965). Those automata are > geometric by nature: every set of n processes executing independent > actions can be modeled by a n-cube, and such an automata then gives > rise to a topological space, obtained by glueing such cubes together, > with a specific direction of time coming from the execution flow. It > then seems natural to use tools from algebraic topology to study those > spaces: paths model executions, homotopies of paths, that is > continuous deformations of paths, model equivalence of executions > modulo scheduling of independent actions, and so on, but all those > notions must preserve the direction somehow. This brings many > complications and the theory must be done again, essentially from > scratch. > > In this talk, after developing this idea of geometry of true > concurrency, I will focus on homology. Homology is a nice computable > tool from algebraic topology and it is a challenge in directed > algebraic topology to find a satisfactory analogue that behaves well > with direction. I will present our candidate of `directed homology’, > called natural (or bimodule) homology. This object consists in a > functor with values in modules, which looks at the classical homology > of trace spaces (a nice abstraction of what we may call `space of > executions’) and how those homologies evolve with time. This evolution > can be studied through an abstract notion of bisimulation of functors > with values in modules, that has many equivalent characterizations > (using relations, using lifting properties, using Grothendieck > construction, …) and whose existence is decidable in simple cases. > Finally, among nice properties of our directed homology, I will show > you that it is computable on simple spaces, which are already enough > to model simple truly concurrent systems. > > Joint work with Eric Goubault and Jean Goubault-Larrecq.

1 0

[SEMINAIRE LCR] Flavien Breuvart, 12/05/2017 11:00
by breuvart 11 May '17

11 May '17

MONADES ET COMONADES (SUITE) Flavien Breuvart, LIPN Salle B107, bâtiment B, Université de Villetaneuse 12/05/2017 11:00 - 12:30 Résumé : Dans cette deuxième séance du GdT modades et comonades, je présenterais les monades et comonades gradées. J'insisterais, en particulier, sur ma vision de ces objets comme potentielle piste pour faire interagir interprétation abstraite et typage dans les langages fonctionnels.

1 0

Re: [GdT Log&Prog] Double GdT?
by breuvart 06 Feb '17

06 Feb '17

Salut à tous, La semaine prochaine, pas de séminaire d'équipe à cause des vacances, mais pour cette semaine, on pourrait en avoir deux: - Christophe animera un GdT sur les derniers travaux de Girard vendredi (titre et abstract à venir, mais je pense que tous le monde sais de quoi il s'agit) - Gabriel Scherer serait dispo demain ou après demain pour présenter ses travaux (notamment un POPL en seul auteur...) mais uniquement demain ou après demain. Y aurait-il des personnes disponible? quand? Dites moi rapidement ;) Amicalement, Flavien

1 1

Changement de garde !
by Damiano Mazza 02 Feb '17

02 Feb '17

Bonjour, Jutse une annonce rapide pour vous dire que, après des nombreuses années, je laisse la responsabilité du séminaire/gdt à Flavien, que je remercie pour avoir accepté de s'occuper de cette tâche dans le future. Dorénavant, vous pouvez donc vous adresser à Flavien pour toute requête concernant notre séminaire/gdt. Amicalement, Damiano

1 0