JavaScript is disabled for your browser. Some features of this site may not work without it.
The Type Theory of PL/CV3

Author
Constable, Robert L.; Zlatin, Daniel R.
Abstract
The programming logic PL/CV3 is based on the notion of a mathematical type. We present the core of the type theory, from which the full theory for program verification and specification can be derived. Whereas the full theory was designed to be useable, the core theory was selected to be analyzable. This presentation strives to be succinct yet thorough. The last section consists of examples, but the approach here is not tutorial. Key Words and phrases: automated logic, program verification, program specification, semantics of programming languages, type theory, foundations of mathematics.
Date Issued
1981-08Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR81-464
Type
technical report