Author: Helmut Schwichtenberg
Title: Program extraction in constructive analysis
Abstract:
We consider a formal arithmetical system with type and
predicate parameters. Moreover inductive definitions with their
introduction and elimination axioms are allowed. For this system we
define extracted terms and the notion of (modified) realizability, and
prove a soundness theorem. Then constructive analysis is developed in
this setting, with special emphasis on low type level witnesses (which
is possible when we assume separability). As an example we discuss the
intermediate value theorem, and the form and usefulness of extracted
programs form its proof.