Recursion in Logics of Programs.
David Harel:
Recursion in Logics of Programs.
POPL 1979: 81-92@inproceedings{DBLP:conf/popl/Harel79,
author = {David Harel},
title = {Recursion in Logics of Programs},
booktitle = {POPL},
year = {1979},
pages = {81-92},
ee = {db/conf/popl/Harel79.html},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
BibTeX
Abstract
The problem of reasoning about recursive programs is considered.
Utilizing a simple analogy between iterative and recursive programs viewed as unfinite unions of finite terms, we carry out an investigation analogous to that carried out recently for iterative programs.
The main results are the arithmetical completeness of axiom systems for (1) context-free dynamic logic and (2) its extension for dealing with infinite computations.
Having the power of expression of these Iogics in mind, these results can be seen to supply (as corollaries) complete proof methods for the various kinds of correctness of recursive programs.
Copyright © 1979 by the ACM,
Inc., used by permission. Permission to make
digital or hard copies is granted provided that
copies are not made or distributed for profit or
direct commercial advantage, and that copies show
this notice on the first page or initial screen of
a display along with the full citation.
POPL Proceedings Compendium
CDROM Version: Load the CDROM "POPL, The First Ten Years" and ...
BibTeX
Printed Edition
Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, January 1979.
ACM 1979 BibTeX
Contents
BibTeX
Copyright © Sat May 16 23:34:35 2009
by Michael Ley (ley@uni-trier.de)