Gray code (also called re ected binary code) is widely known in digital communication, due to its property that the Hamming distance between adjacent Gray codes is always 1. Based on Gray code, Tsuiki has studied an expansion of real numbers as streams of 0,1,unde ned each of which contains at most one unde ned, and called it the modi ed Gray expansion. We consider a representation of modi ed Gray expansion as ordinary streams, called pre-Gray code. Through the realizability interpretation we extract programs from proofs in a theory with inductive and coinductive de nitions; the realizers involve (higher type) recursion and corecursion operators. As case studies we extract real number algorithms in our setting of pre-Gray code. The correctness of the extracted programs is automatically ensured by the soundness theorem. (j.w.w. Ulrich Berger, Kenji Miyamoto and Hideki Tsuiki)