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.

PRL Home
Introduction
The Nuprl book
Origins of the PRL Project
Goals
Dynamics of the Project
Mathematical Expression in Nuprl
Cross Links to Math & CS Fields

Knowledge Base
Math Library
Publications
Projects
CRASH
Nuprl/FDL System
EventML Software
Seminar

People
Wiki
The Book
Lectures
Other Groups

Extraction in IZF

by Wojciech Moczydlowski 2004-2005

by Wojciech Moczydlowski
2004-2005