Contents of Report

[Data of Report]

	Abstract	.... 2
1	Introduction	.... 2
2	Proof Compiler	.... 3
2.1	Notational Preliminaries	.... 3
2.2	Interface Rules	.... 4
2.3	Program Extraction Algorithm	.... 5
3	Proof of Course of value Induction in QJ	.... 8
4	Simple Example;GCD Program	.... 10
4.1	GCD Proof	.... 10
4.2	Proof Compilation of GCD Proof	.... 12
5	Performance Evaluation of the GCD Program	.... 13
5.1	Exection of the GCD Program	.... 13
5.2	Comparison with Divide and Conquer Type Program	.... 15
6	Optimization Technique	.... 16
6.1	Proof Normalization and Partial Evaluation of Program	.... 16
6.2	Example of Proof Normalization	.... 18
6.3	Optimized V code	.... 20
7	Implementation of the QPC System	.... 21
8	Conclusion	.... 21
	Acknowledgments	.... 22
	References	.... 22
	End	.... 34

目次をクリックすると、PDFファイルが表示されます。