Rencontre, 21 novembre 2024

Programme

• Isabelle Collet (Université de Genève)
  Invited talk: Femmes et numérique : pratiques égalitaires, dispositifs inclusifs

  L’informatique joue un rôle croissant dans l’évolution de nos sociétés, mais les femmes sont largement sous-représentées dans ces métiers depuis plusieurs décennies. On retrouve avec l’informatique la division sociosexuée des savoirs : il y a des savoirs considérés comme normaux ou adaptés pour un genre, mais tabou, inadaptés ou inaccessibles pour l’autre… Les composantes de cette division fluctuent, historiquement et géographiquement : le peu de femmes en informatique est un problème récent et local : il est apparu après les années 80, en occident.

  Le but de cette conférence est tout d’abord de déconstruire des idées reçues sur les femmes et l’informatique, puis de passer en revue quelques bonnes pratiques qui ont permis de s’approcher de la parité dans plusieurs institutions. Ces bonnes pratiques, mises en place notamment aux États-Unis ou en Norvège, peinent à s’installer en France à cause d’un système éducatif assez rigide aux réformes parfois contre-productives. Les succès internationaux montrent qu’il n’y a pas de fatalité ou de prédétermination. Toutefois, ils montrent aussi qu’il faut des mesures fortes pour renverser la tendance.

  The talk will be in french.

  • 21 novembre 2024, 10:30
• Théo Winterhalter (Deducteam, INRIA)
  Invited talk: Dependent Ghosts Have a Reflection for Free

  We introduce ghost type theory (GTT) a dependent type theory extended with a new universe for ghost data that can safely be erased when running a program but which is not proof irrelevant like with a universe of (strict) propositions. Instead, ghost data carry information that can be used in proofs or to discard impossible cases in relevant computations. Casts can be used to replace ghost values by others that are propositionally equal, but crucially these casts can safely be ignored for conversion. We provide a type-preserving erasure procedure which gets rid of all ghost data and proofs, a step which may be used as a first step to program extraction. We give a syntactical model of GTT using a program translation akin to the parametricity translation and thus show consistency of the theory. Because it is a parametricity model, it can also be used to derive free theorems about programs using ghost code. We further extend GTT to support equality reflection and show that we can eliminate its use without the need for the usual extra axioms of function extensionality and uniqueness of identity proofs. In particular we validate the intuition that indices of inductive types—such as the length index of vectors—do not matter for computation and can safely be considered modulo theory. The results of the paper have been formalised in Coq.