Dieser Titel verbindet zwei der dominantesten Forschungsströme in der Philosophie der Logik, nämlich Spieltheorie und Beweistheorie. Wie der Untertitel der Arbeit ausdrückt, werden die Autoren diese Verbindung durch den dialogischen Ansatz zur Logik herstellen. Ein wichtiger Aspekt der vorliegenden Studie ist, dass sich die Autoren auf den logisch gültigen Teil der Konstruktiven Typentheorie (CTT) beschränken. Der Grund dafür ist, dass, sobald dieser Teil erreicht ist, das Ergebnis auf das gesamte CTT-System ausgeweitet werden kann. Die ersten Kapitel des kurzen Werkes bieten einen Überblick über die beiden in dem Buch diskutierten Rahmenbedingungen, wobei der dialogische Rahmen betont wird. Das dritte Kapitel zeigt die Richtung von links nach rechts des Äquivalenzergebnisses. Darauf folgt ein Kapitel, das die Verwendung des Algorithmus demonstriert, um zu zeigen, wie eine spezifische Gewinnstrategie in einen CCT-Beweis des Auswahlaxioms umgewandelt werden kann.