dc.contributor.author Constable, Robert L. en_US dc.contributor.author Knoblock, Todd B. en_US dc.contributor.author Bates, Joseph L. en_US dc.date.accessioned 2007-04-23T16:53:48Z dc.date.available 2007-04-23T16:53:48Z dc.date.issued 1984-10 en_US dc.identifier.citation http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR84-645 en_US dc.identifier.uri https://hdl.handle.net/1813/6484 dc.description.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. en_US dc.format.extent 3799774 bytes dc.format.extent 895301 bytes dc.format.mimetype application/pdf dc.format.mimetype application/postscript dc.language.iso en_US en_US dc.publisher Cornell University en_US dc.subject computer science en_US dc.subject technical report en_US dc.title Writing Programs that Construct Proofs en_US dc.type technical report en_US
﻿