Home » Évènement

Soutenance de thèse de Gaëtan GILBERT (équipe Gallinette)

Gaëtan Gilbert, doctorant au sein de l’équipe Gallinette, soutiendra sa thèse intitulée « Une théorie des types avec insignifiance des preuves définitionnelle » / « A type theory with definitional proof-irrelevance »

vendredi 20 décembre 2019 à 10h, dans l’amphi Besse de l’IMT-A.

Jury :
Directeur thèse : TABAREAU Nicolas
Co encadrant : SOZEAU Matthieu (CR Inria)
Rapporteurs : ABEL Andreas (Chalmers Techniska Hogskola AB), SPITTERS Bas (Aarhus University)
Autres membres : MAHBOUBI Assia, BERTOT Yves (DR Inria Antipolis), SMOLKA Gert (Saarland University)

Résumé : L’égalité définitionnelle, aussi appelée conversion, pour une théorie des types avec une vérification de type décidable est l’outil le plus simple pour prouver que deux
objets sont les mêmes, laissant le système décider en utilisant uniquement le calcul. Par conséquent, plus il y a de choses égales par conversion, plus il est simple d’utiliser un
langage basé sur la théorie des types. L’insignifiance des preuves, indiquant que deux preuves quelconques de la même proposition sont égales, est une manière possible
d’étendre la conversion afin de rendre une théorie des types plus puissante. Cependant, ce nouveau pouvoir a un prix si nous l’intégrons naïvement, soit en rendant la vérification
de type indécidable, soit en réalisant de nouveaux axiomes—tels que l’unicité des preuves d’identité (UIP)—qui sont incompatibles avec d’autres extensions, comme l’univalence.
Dans cette thèse, nous proposons un moyen général d’étendre une théorie des types avec l’insignifiance des preuves, de manière à ce que la vérification du type soit décidable
et est compatible avec l’univalence. Nous fournissons un nouveau critère pour décider si une proposition peut être éliminée sur un type (en corrigeant et en améliorant la règle
d’élimination des singletons de Coq) en utilisant des techniques provenant de développements récents du filtrage dépendant sans UIP. Nous fournissons aussi une preuve de
la décidabilité du typage à base de relations logiques. Cette extension de la théorie des types a été implementée dans les assistants de preuve Coq et Agda.

Mot-clés : Assistant de preuve, Coq, insignifiance des preuves, univers, UIP

********

Abstract: Definitional equality, a.k.a conversion, for a type theory with a decidable type checking is the simplest tool to prove that two objects are the same, letting the system decide just using computation. Therefore, the more things are equal by conversion, the simpler it is to use a language based on type theory. Proof-irrelevance, stating that any two proofs of the same proposition are equal, is a possible way to extend conversion to make a type theory more powerful. However, this new power comes at a price if we integrate it naively, either by making type checking undecidable or by realizing new axioms—such as uniqueness of identity proofs (UIP)—that are incompatible with other extensions, such as univalence. In this thesis, we propose a general way to extend a type theory with definitional proof irrelevance, in a way that keeps type checking decidable and is compatible 
with univalence. We provide a new criterion to decide whether a proposition can be eliminated over a type (correcting and improving the so-called singleton elimination of Coq) byusing techniques coming from recent development on dependent pattern matching without UIP. We show the decidability of type checking using logical relations. This extension of type theory has been implemented both in Coq and Agda.

Keywords: Proof assistant, Coq, proof-irrelevance, universes, UIP

Soutenance de thèse d’Ambroise LAFONT (équipe Gallinette)

Ambroise Lafont, doctorant au sein de l’équipe Gallinette, soutiendra sa thèse intitulée « Signatures et modèles pour la syntaxe et la sémantique opérationnelle en présence de liaison de variables » / « Signatures and models for syntax and operational semantics in the presence of variable binding »

lundi 2 décembre 2019 à 10h, dans la salle 3 du bâtiment 11 sur le site de la FST.

Jury :

  • Directeur thèse : Nicolas Tabareau
  • Co encadrant : Tom Hirschowitz (CR CNRS LAMA)
  • Rapporteurs : Peter Lefanu Lumsdaine, U Stocklom), Marcelo Fiore (U Cambridge)
  • Autres membres : Benedikt Ahrens (U Birmingham), Thomas Ehrhard (U Paris Diderot), Delia Kesner (U Paris Diderot)

Résumé : Cette thèse traite de la spécification et la construction de la syntaxe et sémantique opérationnelle d’un langage de programmation. Nous travaillons avec une notion générale de “signature” pour spécifier des objets d’une catégorie donnée comme des objets initiaux dans une catégorie appropriée de modèles. Cette caractérisation, dans l’esprit de la sémantique initiale, donne une justification du principe de récursion.  Les langages avec liaisons, telles que le lambda calcul pur, sont des monades sur la catégorie des ensembles spécifiées par les signatures algébriques classiques. Les premières extensions de syntaxes avec des équations que nous considérons sont des “quotients” de ces signatures algébriques. Ils  permettent, par exemple, de spécifier une opération commutative binaire. Cependant, certaines équations, comme l’associativité, semblent hors d’atteinte. Ceci motive la notion de 2-signature qui complète la définition précédente avec la donnée d’un ensemble d’équations. Nous identifions la classe des “2- signatures algébriques” pour lesquelles l’existence de la syntaxe associée est garantie. Finalement, nous abordons la spécification de la sémantique opérationnelle d’un langage de programmation tel que le lambda calcul avec -réduction. Nous introduisons à cette fin la notion de monade de réduction et leur signatures, puis les généralisons pour aboutir à la notion de monade opérationnelle.

Mot-clés : monades, syntaxe, sémantique, signature

*******

Abstract: This thesis deals with the specification and construction of syntax and operational semantics of a programming language. We work with a general notion of “signature” for specifying objects of a given category as initial objects in a suitable category of models. This characterization, in the spirit of Initial Semantics, gives a justification of the recursion principle. Languages with variable binding, such as the pure lambda calculus, are monads on the category of sets specified through the classical algebraic signatures. The first extensions to syntaxes with equations that we consider are “quotients” of these algebraic signatures. They allow, for example, to specify a binary commutative operation. But some equations, such as associativity, seem to remain out of reach. We thus introduce the notion of 2-signature, consisting in two parts: a specification of operations through a usual signature as before, and a set of equations among them. We identify the class of “algebraic 2-signatures” for which the existence of the associated syntax is guaranteed. Finally, we takle the specificiation of the operational semantics of a programming language such as lambda calculus with – reduction. To this end, we introduce the notion of reduction monad and their signatures, then we generalize them to get the notion of operational them to get the notion of operational monad.

Keywords: monads, syntax, semantic, signature

Chantiers Arts Technologie et Sciences

Le Théâtre Athénor suscite et soutient la collaboration d'artistes
(compositeurs, comédiens, écrivains,...) avec des scientifiques, au
travers de ses Chantiers Arts Technologie et Science. En particulier,
il entretient depuis 2011 une relation privilégiée avec nos voisins
mathématiciens du Laboratoire Jean Leray autour des Chantiers Arts
Technologie et Science (CHATS):
- création d'objets artistiques professionnels (spectacles, livres,
oeuvres musicales...) nourris des rencontres avec des scientifiques;
- ateliers pour enfants et adolescents en milieu scolaire et en
  maisons de quartier, co-animés par des artistes, des scientifiques
  et des médiateurs du théâtre Athénor ou des réseaux REP+ de la ville
  de Nantes;
- actions de diffusion de la science originales (spectacles, livres,
   jeux...), soutenues par le savoir faire des artistes.

Quelques exemples d'actions Arts&Sciences récentes sont citées en fin
de ce message.

Si vous êtes intéressés par ces chantiers, que vous ayez ou non une
idée de la forme qu'un tel projet pourrait prendre, n'hésitez pas à
nous contacter rapidement (arts-sciences.math@univ-nantes.fr, Assia.Mahboubi@inria.fr).
Nous organiserons une petite réunion informelle fin août/début septembre
pour discuter de ces actions.

******
Quelques exemples d'actions Arts & Sciences récentes: 
- l'installation audiovisuelle générative "structure.workshop.installation" au Stereolux du 13 au 22 septembre, restituant le travail de l’artiste Julien Bayle et de l’enseignant-chercheur Frédéric Hérau avec des étudiants L2 de l'université de Nantes. https://www.stereolux.org/agenda/julien-bayle-frederic-herau-et-des-etudiants-de-l-universite-de-nantes 
- les ateliers croisés du compositeur Alessandro Bosetti et de la   chercheuse Assia Mahboubi au lycée professionnel Michelet, autour du   langage. Les élèves de 1ère ont ensuite organisé et conduit une série de performances publiques à l'université : https://sciences-techniques.univ-nantes.fr/actualites/actualites-vie-de-la-faculte-et-de-l-universite/restitution-du-chantier-arts-technologies-et-sciences-2460166.kjsp   
Alessandro Bosetti parle de ce travail sur JetFM, qui a aussidiffusé la pièce radiophonique RadioMaths issue de ce travail.   http://jetfm.fr/site/jeudi-30-mai-a-14h.html 
- un travail de Samuel Tapie, enseignant chercheur, et des artistes de la compagnie n + 1, avec les élèves de l'école primaire Jean Zay (Nantes)  autour des surfaces, est illustré dans le court-métrage suivant: http://www.math.sciences.univ-nantes.fr/~tapie/video-JeanZay-surfaces.mov 
- les impromptus scientifiques de la compagnie n+1, des discours   spectaculaires qui mettent en scène un chercheur, dont les travaux   sérieux sont joyeusement déréglés par le groupe n+1 de la compagnie Les ateliers du spectacle. Ils tentent de faire tenir ensemble un propos scientifique et une approche poétique. Ils peuvent sedérouler dans des espaces publics variés (théâtre, café, librairie…). Ils sont toujours suivis d’un temps de discussion et d’échange avec le public. http://www.ateliers-du-spectacle.org/spectacle/les-impromptus-scientifiques/ 

Atelier « Musique, langues et logique » avec le lycée professionnel Michelet

Un musicien, Alessandro Bossetti, et une chercheuse, Assia Mahboubi (équipe Gallinette), appuyés par une équipe enseignante, ont exploré avec des élèves préparant en bac professionnel au Lycée Michelet quelques interactions entre mathématiques, logique, langage et musique. Ils vous présentent le fruit de leurs échanges le mardi 28 mai 2019 à la Faculté des Sciences et des Techniques.

Ce projet implique des élèves de première Bac ISEC (installateur thermique) et GT (géomètre topographe) du Lycée professionnel Michelet de Nantes, ainsi qu’une équipe d’enseignantes et documentaliste du lycée. Tout au long de l’année, une scientifique (Assia Mahboubi, chercheuse en informatique au LS2N) et un compositeur (Alessandro Bossetti) ont animé des ateliers croisés avec les élèves atour de quelques interactions entre mathématiques, logique, langage et musique.

Venez découvrir la projection de leur travail et un ensemble de 4 performances le mardi 28 mai 2019, de 14h à 16h30, sur le campus Lombarderie (salles 212 et 213 – bâtiment 26).

En savoir plus : http://www.fpl.math.cnrs.fr/mm-ouest/informations/musique-langues-et-logique

Soutenance de thèse de Simon BOULIER (équipe Gallinette)

Simon Boulier, doctorant au sein de l’équipe Gallinette, soutiendra sa thèse intitulée « extending type Theory with Syntactic Models »

jeudi 29 novembre 2018 à 14h00, dans l’amphi Blaise Pascale, à l’IMT Atlantique.

Jury : Nicolas Tabareau (dir thèse), Thierry Coquand (Université de Gothenburg, rapporteur), Hugo Herbelin (laboratoire IRIF PPS, rapporteur), Assia Mahboubi, Ambrus Kaposi Eötvös Lorand University Hongrie), Pierre Cointe

ACM distinguished paper award pour Nicolas Tabareau à ICFP 2018

Nicolas Tabareau (équipe Gallinette) a reçu l’ACM distinguished paper award à la conférence ICFP (International Conference on Functional Programming) qui a eu lieu à Saint-Louis (USA) du 23 au 29 septembre 2018.

Ce prix récompense la publication intitulée « Equivalences for Free: Univalent Parametricity for Effective Transport », rédigé avec Mathieu Sozeau, chercheur au sein de l’équipe parisienne PI.R2, et Éric Tanter de l’University of Chile.

Voir l’article.

Interview de Nicolas Tabareau pour le magazine « Chercheurs européens » de l’UBL

Le magazine « Chercheurs européens » de l’Université Bretagne Loire a rencontré Nicolas Tabareau, chargé de recherche Inria au sein de l’équipe Gallinette, afin de l’interroger sur son heureuse expérience de candidat à l’ERC Starting Grants avec son projet CoqHoTT.

Retrouvez son interview (pdf) en page 11 du N° 5 de juillet 2018.

Copyright : LS2N 2017 - Mentions Légales - 
 -