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}
}

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 ...

Windows: Click the letter of your CD drive
A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
Mac: Click here
UNIX/LINUX: mount the CD and click on the path of your mount point:
/Anthology/Popl or /cdrom