"Extracting computational content from proofs" (Helmut Schwichtenberg)

We develop a Logic for Inductive Definitions (LID), a self-generating system built from scratch and based on minimal logic, the only underlying notion being that of a computable functional on partial continuous objects. We sketch the realizability interpretation and a proof of the crucial Soundness Theorem. Then we address the delicate question of how to ``decorate'' proofs in order to optimize their computational content (joint work with Diana Ratiu).

内容はこちらの論文に相当する模様。