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/6597
Title: Extracting Efficient Code From Constructive Proofs
Authors: Sasaki, James T.
Keywords: computer science
technical report
Issue Date: Jun-1986
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR86-757
Abstract: Extraction is a technique for producing verified programs. A proof of $\forall chi : T \ldot \exists y : T' \ldot F$ corresponds to a function $f$ of type $T \rightarrow T'$ that maps every $\chi$ of type $T$ to a $y$ of type $T'$ such that $F$ is true. If the proof is constructive, then $f$ is recursive. The semantics of extracted code involves the manipulation of justifications, which are pieces of evidence for the truth of formulas. The raw extracted code for the formula above is actually a function $\gamma$ that maps $\chi$ to a pair $(y, \gamma')$, where $\gamma'$ is a justification that provides evidence for the truth of $F$. This thesis presents various ways to improve the efficiency of extracted programs. The first way uses traditional code optimizations. Though very helpful, they are no panacea. The second way involves small changes to its underlying semantics. Certain formulas, called singleton formulas, have no interesting justifications; if $F$ is such a formula, no justification for it needs to be built, which simplifies the extracted code. The third way to improve extracted code is to add call-by-reference parameters to it. As originally defined, extracted code passes arguments by value, which leads to inefficient code for mutable objects like arrays: passing an array by value requires making a copy of it. Adding call-by-reference parameters entails adding a state to the semantics of extracted code, which in turn leads to various semantic and syntactic design issues, like aliasing and side-effects. To account for these changes, the constructive logic used to build proofs is modified. A proof of quicksort illustrates the functional, assignment-free, side-effect-free style of proof promoted by the new logic. To relieve the user of some of the mental overhead involved in using the new logic, an array inferencing algorithm is presented. The algorithm allows users to get code that uses arrays from proofs that reason about and manipulate lists in restricted ways. In this way, users can view the use of arrays as an optimization.
URI: http://hdl.handle.net/1813/6597
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
86-757.pdf10.58 MBAdobe PDFView/Open
86-757.ps3.39 MBPostscriptView/Open

Refworks Export

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

 

© 2014 Cornell University Library Contact Us