Dismiss
There will be a system update on Tuesday, January 16th, 8 PM ET. You may experience a brief service interruption.
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 Ph.D. Thesis TR 8G757 May 1986 Department of Computer Science Cornell UniversityIthaca, NY 14853 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 EXTRACTING EFFICIENT PROGRAMS FROM CONSTRUCTIVE PROOFS Jamea Tmhio Sasaki 1986 ALL RIGHTS RESERVED A ThesisPresented to the Faculty of the Graduate Schoolof Cornell Universityin Partial Fulfillment of the Requirements for the Lkgree of Doctor of Pliilo.wphy byJam- Tosbio Sasaki June, 1986 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 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

Page 2 of 168

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

Page 4 of 168

Page 5 of 168

EXTRACTING EFFICIENT PROGRAMS FROM CONSTRUCTIVE PROOFS

@ Jamea Tmhio Sasaki 1986

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

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.