JavaScript is disabled for your browser. Some features of this site may not work without it.
Programs As Types

Author
Constable, Robert L.
Abstract
Programs are interpreted as types in a constructive type theory. Rules for a logic of programs can then be derived from rules for types. This approach is the basis of nonelementary reasoning in the PL/CV3 (program) verification system. This paper summarizes the type theory and shows how to develop higher order logic and algorithmic (or programming or dynamic) logic in the theory. The theory described here is an evolution from de Bruijn's AUTOMATH and Martin-Lof's Intuitionistic Theory of Types.
Date Issued
1980-05Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR80-423
Type
technical report