Title: Reflection Mechanism in Constructive Programming (Ph D. Thesis for Doctor of Engineering at Graduate School of Kyoto University) Author: Yukiyoshi Kameyama Supervisor: Professor Masahiko Sato Abstract: This thesis studies the role of the reflection mechanism in Constructive Programming. Constructive Programming is a method of program development based on constructive logic in which correct programs are automatically extracted from proofs of given specifications. Recently it has been widely accepted that the reflection mechanism is quite useful in Constructive Programming. RPT, Reflective Proof Theory, is a constructive logic proposed by Sato. Since the reflection mechanism is built-in in RPT, it can be a suitable basis for our study. In Chapter 2, we first propose a formal system of RPT. We then give several theorems in the formal system, which show the expressive power of the reflection mechanism of RPT. Finally, we study metamathematical properties of the formal system. In particular, the strong normalization theorem and the consistency are proved for our formal system without inductive definitions. In Chapter 3, we describe our Constructive Programming System based on the formal system given in Chapter 2. The system is implemented by the programming language Lambda, which is at the same time the object language of RPT. We give an overview of our Constructive Programming System. As a substantial example of proof development using our system, we demonstrate a mechanized proof of the Church-Rosser property of the programming language Lambda. We also present a concrete example of Constructive Programming based on our system, and present a method to eliminate redundant parts from a program. In Chapter 4, we will study yet stronger reflection mechanism. Although the reflection mechanism in RPT is quite useful, we cannot re-define a modified provability relation internally. The re-definition of the provability relation is the key to eliminate redundant parts in extracted programs. To solve this problem, we propose the mechanism of half-monotone inductive definitions. A half-monotone inductive definition is an extension of the conventional monotone inductive definition so that we can define the provability relation naturally. We give a theory and a realizability interpretation of the half-monotone inductive definitions. We also interpret several theories such as Martin-Lof's type theory and the Logical Theory of Constructions using this mechanism. We also apply the mechanism to the provability relations and show a method of program refinement. In Chapter 5, we turn our attention to programming languages. The programming language Lambda given in Chapter 2 is a purely functional one in the sense that there are no side-effects. It is an interesting research problem to introduce imperative features into our language. The programming language Lambda! (pronounced ``lambda bang'') was proposed by Sato as an extension of Lambda in which the assignment and the while statements are introduced. We give some conservativeness results on Lambda! in Chapter 5. In Chapter 6, we give concluding remarks of the thesis.