A PL/CV Precis.
Robert L. Constable, Scott Johnson:
A PL/CV Precis.
POPL 1979: 7-20@inproceedings{DBLP:conf/popl/ConstableJ79,
author = {Robert L. Constable and
Scott Johnson},
title = {A PL/CV Precis},
booktitle = {POPL},
year = {1979},
pages = {7-20},
ee = {db/conf/popl/ConstableJ79.html},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
BibTeX
Abstract
PL/CV is a new formal system which mixes commands and assertions.
It includes axioms and rules for a theory of programming over integers and characters.
Since arguments in the theory can be checked by the PL/CV Proof Checker, the system offers an approach to mechanical program verification.
The Proof Checker is efficient enough for classroom use.
Early experience with PL/CV indicates that it nicely supports formal verification of elementary arguments. Continued work should enable the formalization of non-elementary reasoning as well.
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:34 2009
by Michael Ley (ley@uni-trier.de)