Rencontre, 21 novembre 2024

Programme

10:30 – 12:00

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.

13:45 – 14:45

Adrienne Lancelot (IRIF - Université Paris Cité)

Invited talk: Interaction Equivalence

Contextual equivalence is the de facto standard notion of program equivalence. A key theorem is that contextual equivalence is an equational theory. Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does not induce an equational theory, for an apparently essential reason: cost is not invariant under reduction.

In the paradigmatic case of the untyped λ-calculus, we introduce interaction equivalence. Inspired by game semantics, we observe the number of interaction steps between terms and contexts but -- crucially -- ignore their own internal steps. We prove that interaction equivalence is an equational theory and we characterize it as B, the well-known theory induced by Böhm tree equality. Ours is the first observational characterization of B obtained without enriching the discriminating power of contexts with extra features such as non-determinism. To prove our results, we develop interaction-based refinements of the Böhm-out technique and of intersection types. Joint work with Beniamino Accattoli, Giulio Manzonetto and Gabriele Vanoni.

15:15 – 16:15

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.