# * Extraction in IZF *

## by Wojciech Moczydlowski

2004-2005

IZF is an intuitionistic version of Zermelo-Fraenkel set theory (ZFC). We present a practical approach to doing extraction in IZF, based on formulas-as-types principle.