Browse Prior Art Database

Extracting Efficient Code From Constructive Proofs

IP.com Disclosure Number: IPCOM000148376D
Original Publication Date: 1986-May-31
Included in the Prior Art Database: 2007-Mar-29
Document File: 168 page(s) / 7M

Publishing Venue

Software Patent Institute

Related People

Sasaki, James T.: AUTHOR [+2]

Abstract

James T. Sasaki

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 3% of the total text.

Page 1 of 168

Extracting Efficient Code From
Constructive Proofs

James T. Sasaki

Ph.D. Thesis TR 8G757

May 1986

Department of Computer Science Cornell University
Ithaca,
NY 14853

[This page contains 1 picture or other non-text object]

Page 2 of 168

[This page contains 1 picture or other non-text object]

Page 3 of 168

EXTRACTING EFFICIENT PROGRAMS FROM CONSTRUCTIVE PROOFS

           A Thesis
presented to the Faculty of the Gaduate School
of Cornell University

in Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy

by


James Toshio Sasaki June, 1986

[This page contains 1 picture or other non-text object]

Page 4 of 168

[This page contains 1 picture or other non-text object]

Page 5 of 168

EXTRACTING EFFICIENT PROGRAMS FROM CONSTRUCTIVE PROOFS

@ Jamea Tmhio Sasaki 1986

ALL RIGHTS RESERVED

           A Thesis
Presented to the Faculty of the Graduate School
of Cornell University
in Partial Fulfillment of the Requirements for the
Lkgree of Doctor of Pliilo.wphy

     by
Jam- Tosbio Sasaki June, 1986

[This page contains 1 picture or other non-text object]

Page 6 of 168

Extracting Efficient Programs From Constructive Proofs James Toshio Sasaki, Ph.D.

Cornell University 1986

EzIraclion is a technique for producing verified programs. A proof of

Vz: T .3y: T' . F corresponds to a function f of type T -+ T' that maps

every z 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 juslificalions, which are pieces of evidence for the truth of for~nulas. The raw extracted code for the formula above is actually a function 7 that maps z to a pair (y,f), where 7' is a.justification that provides evidence for the truth of F.

  This thesis presents various ways to improve the eficiency of extracted programs. The first way uses traditional code optimizations. Though very Belpful, they are no panacea. The second way involves small changes to its underlying semantics. Certain formulas, called single1011 formulas, have no interesting justifications; if F is such a formula, no justification for it needs to be buill, which simplifies the extracted code.

by value, which leads to ineficient 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 se-
mantics 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, sideeffect-froe 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 army in/ercncing algorithm is presented. The algorithm allows users to get code that uses array...