| 1 | Introduction | .... 2 |
| 2 | Outline of Proof Compilation | .... 3 |
| 3 | Generator Programs | .... 6 |
| 3.1 | Prime Number Generator in Constructive Mathematics | .... 6 |
| 3.2 | Prime Number Generator in Prolog | .... 8 |
| 4 | Parameterized Proof in Constructive Logic | .... 13 |
| 4.1 | Proof Parameterization Method | .... 13 |
| 4.2 | Operational Semantics | .... 15 |
| 5 | Prime Number Generator in the Extended Framework | .... 20 |
| 5.1 | 'sieve' | .... 20 |
| 5.2 | Parallel Exection of Realizer Code of 'sieve' | .... 23 |
| 5.3 | 'two-digit-nat' | .... 26 |
| 5.4 | Prime Number Generator | .... 28 |
| 6 | Subsequent Research | .... 29 |
| Acknowledgment | .... 30 | |
| References | .... 30 |
ICOT研究論文（TR）一覧に戻る / Back to the list of ICOT Technical Reports