We study the system IFP of intuitionistic fixed point logic, an extension of intuitionistic first-order logic by strictly positive inductive and coinductive definitions. We define a realizability interpretation of IFP and use it to extract computational content from proofs about abstract structures specified by arbitrary classically true disjunction free formulas. The interpretation is shown to be sound with respect to a domain-theoretic denotational semantics and a corresponding lazy operational semantics of a functional language for extracted programs. We also show how extracted programs can be translated into Haskell. As an application we extract a program converting the signed digit representation of real numbers to infinite Gray-code from a proof of inclusion of the corresponding coinductive predicates.

翻译：我们研究直觉不动点逻辑系统IFP，它是直觉一阶逻辑通过严格正归纳与余归纳定义扩展得到的系统。我们定义了IFP的可实现性解释，并利用该解释从关于任意经典真值无析取公式所指定的抽象结构的证明中提取计算内容。该解释被证明相对于一个域论指称语义及其对应的惰性操作语义（用于提取程序的函数式语言）具有可靠性。我们还展示了如何将提取的程序翻译成Haskell。作为应用，我们从相应余归纳谓词包含关系的证明中提取了将实数符号位表示转化为无穷格雷码的程序。