Show simple item record

dc.contributor.authorConstable, Robert L.en_US
dc.contributor.authorKnoblock, Todd B.en_US
dc.contributor.authorBates, Joseph L.en_US
dc.date.accessioned2007-04-23T16:53:48Z
dc.date.available2007-04-23T16:53:48Z
dc.date.issued1984-10en_US
dc.identifier.citationhttp://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR84-645en_US
dc.identifier.urihttps://hdl.handle.net/1813/6484
dc.description.abstractWhen we learn mathematics, we learn more than definitions and theorems. We learn techniques of proof. In this paper, we describe a particular way to express these techniques and incorporate them into formal theories and into computer systems used to build such theories. We illustrate the methods as they were applied in the $\lambda$-PRL system, essentially using the ML programming language from Edinburgh LCF [23] as the formalised metalanguage. We report our experience with such an approach emphasizing the ideas that go beyond the LCF work, such as transformation tactics, refinement tactics, and special purpose reasoners. We also show how the validity of tactics can be guaranteed. The introduction places the work in historical context and the conclusion briefly describes plans to carry the methods further. The majority of the paper presents the $\lambda$-PRL approach in detail.en_US
dc.format.extent3799774 bytes
dc.format.extent895301 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.titleWriting Programs that Construct Proofsen_US
dc.typetechnical reporten_US


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Statistics