Chuangjie Xu, January 2017 We implement the term extraction algorithm via a nonstandard Dialectica interpretation for system H introduced in B. van den Berg, E. Briseid, and P. Safarik, A functional interpretation for nonstandard arithmetic, Annals of pure and applied logic 163 (2012), no. 12, 1962–1994. We define system H with 4 inductive datatypes \begin{code} import H \end{code} and then the term extraction algorithm via a nonstandard Dialectica interpretation. \begin{code} import Dialectica \end{code} Extracted terms contain noncomputational information. So we define a simplify function to remove it. \begin{code} import Simp \end{code} In the end We present a few simple examples and compare the terms extracted from different proofs of a theorem. \begin{code} import Examples \end{code}