La première partie propose des systèmes de réécriture munis de réductions atomiques, locales et parallèles qui permettent l'exécution des preuves de la logique linéaire (ce sont des programmes exprimés avec des mathématiques). On y ajoute aussi une construction qui permet d'introduire la récursion.
La deuxième partie s'articule autour de la logique linéaire différentielle et de ses ressources à usage unique. On lui ajoute une super-promotion, mieux adaptée à ce formalisme que la promotion ordinaire. Elle peut être exprimée dans les réseaux ou dans un calcul de structures adéquat.
Il est aussi question de réalisabilité pour les systèmes différentiels et de sémantique relationnelle.