La logique, et plus particulièrement la théorie de la démonstration — domaine qui a pour objet d'étude les preuves mathématiques, a récemment donné lieu à de nombreux développements concernant l'informatique théorique. Ces développements se fondent sur une correspondance, dite de Curry-Howard, entre les preuves mathématiques et les programmes informatiques. L'intérêt de cette correspondance provient du fait que celle-ci soit dynamique: l'exécution des programmes correspond à une procédure sur les preuves, dite d'élimination des coupures. Suite à une étude poussée de la formalisation des preuves, Jean-Yves Girard a initié le programme de géométrie de l'interaction. Ce programme, dans une première approximation, a pour objectif l'obtention d'une représentation des preuves rendant compte de la dynamique de l'élimination des coupures. Via la correspondance entre preuves et programmes, cela correspond donc à obtenir une sémantique des programmes rendant compte de la dynamique de leur exécution. Cependant, le programme de géométrie de l'interaction est plus ambitieux: au-delà de la simple interprétation des preuves, il s'agit d'une complète reconstruction de la logique autour de la dynamique d'élimination des coupures. On reconstruit donc la logique des programmes eux-mêmes, dans un cadre où la notion de formule rend compte du comportement des algorithmes. Depuis l'introduction de ce programme, Jean-Yves Girard a proposé plusieurs constructions afin de le réaliser dans lesquelles les preuves sont représentées par des opérateurs dans une algèbre de von Neumann. Ces constructions étant fondées sur la notion d'exécution des programmes, le programme de géométrie de l'interaction est particulièrement pertinent pour l'étude de la complexité algorithmique. En particulier, ce programme a déjà démontré qu'il permettait de formaliser à l'aide d'outils mathématiques des classes de complexité en temps et en espace.