Effectively Eliminating Auxiliaries

Stijn de Gouw, Jurriaan Rot

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

Abstract

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
PublisherSpringer
Pages226-241
Number of pages16
ISBN (Electronic)978-3-319-30734-3
ISBN (Print)978-3-319-30733-6
DOIs
Publication statusPublished - 2016
Externally publishedYes

Publication series

SeriesLecture Notes in Computer Science
Volume9660
ISSN0302-9743
SeriesTheoretical Computer Science and General Issues
Volume9660

    Fingerprint

Cite this

Gouw, S. D., & Rot, J. (2016). Effectively Eliminating Auxiliaries. In E. Ábrahám, M. Bonsangue, & E. Broch Johnsen (Eds.), Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday (pp. 226-241). Springer. Lecture Notes in Computer Science, Vol.. 9660, Theoretical Computer Science and General Issues, Vol.. 9660 https://doi.org/10.1007/978-3-319-30734-3_16