Skip to main content


eCommons@Cornell

eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/6484
Title: Writing Programs that Construct Proofs
Authors: Constable, Robert L.
Knoblock, Todd B.
Bates, Joseph L.
Keywords: computer science
technical report
Issue Date: Oct-1984
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR84-645
Abstract: When 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.
URI: http://hdl.handle.net/1813/6484
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
84-645.pdf3.71 MBAdobe PDFView/Open
84-645.ps874.32 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.

 

© 2014 Cornell University Library Contact Us