Contents of Report

[Data of Report]

	Abstract	.... 2
1	Introduction	.... 2
2	Outline of QPC	.... 3
2.1	Core part of QPC	.... 4
2.2	Some modified features	.... 10
3	QPC	.... 13
3.1	Language of QPC	.... 13
3.2	Rules on Formula and Abstract	.... 14
3.3	Second Order Rules of Inference	.... 14
3.4	Normalization rule	.... 14
4	General Scheme of Specifications and program Extrction	.... 15
4.1	Specification	.... 15
4.2	Extaraction of program Schemata	.... 16
4.3	Redudancy in the Extracted Code	.... 18
4.4	Polymorphism	.... 18
5	Extraction of map function	.... 19
5.1	Specification and Proofs	.... 20
5.2	Extracted Codes from the Proofs of Map,Succ,and Even_Odd	.... 20
5.3	Codes from Map applied to Succ	.... 21
5.4	Codes from Map applied to Even_Odd	.... 21
6	Extended Projection with ordinary Projection	.... 23
7	Conclusion	.... 24
	References	.... 24
	Appendix	.... 27
	End	.... 35

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