Contents of Report

[Data of Report]

	Abstract	.... 2
1	Introduction	.... 2
2	The Language and Constructive Logic	.... 4
2.1	Tiny Quty	.... 4
2.2	QPC	.... 5
2.3	q-realizability	.... 6
3	Declaration and Marking	.... 6
3.1	Realizing variables, length, and ∃-v information of a formula	.... 6
3.2	Declaration	.... 7
3.3	Marking	.... 7
4	Marking of Proofs in Induction	.... 10
4.1	Overflowed and missing marking numbers	.... 10
4.2	Elimination of overflowed marking numbers	.... 11
5	Program Extractor	.... 13
6	An Example	.... 15
6.1	Extraction of a prime number checker program	.... 15
6.2	Extraction of multiple programs	.... 17
7	Proof Theoretic Analysis	.... 18
7.1	Critical Segments	.... 18
7.2	Overflowed marking number in the example in 6	.... 20
8	Conclusion	.... 20
	Acknowledgment	.... 21
	References	.... 21

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