Nous présentons une construction algébrique qui a pour loi de composition l’unification de termes du premier ordre, et comment y représenter le calcul. La correspondance preuve-programme fournit alors une façon innovante de représenter les entiers binaires comme des fonctions dialoguant avec les programmes. Les machines abstraites que l’on peut y encoder (les observations) peuvent naturellement être vues comme des machines à pointeurs, qui parcourent l’entrée sans la modifier. On montre alors que ces observations sont suffisamment expressives pour caractériser l’espace logarithmique, et que décider de l’acceptation d’un mot par une observation est réductible au problème d’acyclicité d’un graphe, un problème également en espace logarithmique. (En collaboration avec Marc Bagnol [http://iml.univ-mrs.fr/ bagnol/], Paolo Pistone et Thomas Seiller [http://www.ihes.fr/ seiller/])