Show simple item record

dc.contributor.authorConstable, Robert L.en_US
dc.date.accessioned2007-04-23T16:39:24Z
dc.date.available2007-04-23T16:39:24Z
dc.date.issued1980-05en_US
dc.identifier.citationhttp://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR80-423en_US
dc.identifier.urihttps://hdl.handle.net/1813/6263
dc.description.abstractPrograms 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.en_US
dc.format.extent1778234 bytes
dc.format.extent516091 bytes
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.language.isoen_USen_US
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titlePrograms As Typesen_US
dc.typetechnical reporten_US


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Statistics