Intuitionistic Fixed Point Logic
Abstract
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.
Cite
@article{arxiv.2002.00188,
title = {Intuitionistic Fixed Point Logic},
author = {Ulrich Berger and Hideki Tsuiki},
journal= {arXiv preprint arXiv:2002.00188},
year = {2023}
}
Comments
65 pages. This is a new Version where some minor details in the Soundness Theorem were corrected and some added