Effectively Eliminating Auxiliaries

Stijn de Gouw, Jurriaan Rot

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review


Auxiliary variables are used in the intermediate steps of a correctness proof to store additional information about the computation. We investigate for which classes of programs auxiliary variables can be avoided in the associated proof system, and give effective translations of proofs whenever this is the case.
Original languageEnglish
Title of host publicationTheory and Practice of Formal Methods
Subtitle of host publicationEssays Dedicated to Frank de Boer on the Occasion of His 60th Birthday
EditorsErika Ábrahám, Marcello Bonsangue, Einar Broch Johnsen
Number of pages16
ISBN (Electronic)978-3-319-30734-3
ISBN (Print)978-3-319-30733-6
Publication statusPublished - 2016
Externally publishedYes

Publication series

SeriesLecture Notes in Computer Science
SeriesTheoretical Computer Science and General Issues (LNCS subseries)

Fingerprint Dive into the research topics of 'Effectively Eliminating Auxiliaries'. Together they form a unique fingerprint.

Cite this