Papers

• The Epsilon Calculus with Equality and Herbrand Complexity, Kenji Miyamoto and Georg Moser, submitted, 2022. (old draft pdf at arXiv)
• Application of constructive analysis in exact real arithmetic Kenji Miyamoto, to appear as a chapter in Handbook of Constructive Mathematics, ed. Bridges, Ishihara, Rathjen and Schwichtenberg, CUP, 2022.
• Logic for Gray Code Computation, Ulrich Berger, Kenji Miyamoto, Helmut Schwichtenberg and Hideki Tsuiki. To appear in D. Probst and P. Schuster (eds), Concepts of Proof in Mathematics, Philosophy, and Computer Science, De Gruyter, 2016. (pdf)
• Program Extraction in Real Arithmetic, Kenji Miyamoto and Helmut Schwichtenberg. Mathematical Structures in Computer Science 25(8): 1692-1704, CUP, 2015 (pdf)
• Program Extraction from Nested Definitions, Kenji Miyamoto, Fredrik Nordvall Forsberg and Helmut Schwichtenberg. ITP 2013, LNCS7998, pp. 370-385, 2013. (pdf, slides, Minlog script)
• Program Extraction with Nested Inductive/Coinductive Definitions, Kenji Miyamoto and Helmut Schwichtenberg, CiE 2012 informal presentation. (pdf)
• Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras, Ulrich Berger, Kenji Miyamoto, Helmut Schwichtenberg and Monika Seisenberger. CALCO-Tools 2011, LNCS 6859, pp. 393-399, 2011. (pdf, slides)

Dissertation

Program Extraction from Coinductive Proofs and its Application to Exact Real Arithmetic