We present a foundational framework, which we call D, unifying a lazy programming language with an impredicative constructive set theory IZF R by means of dependent types. We show that unification brings many benefits to both worlds. First, D supports two paramount paradigms of creating reliable software: correctness by construction and post-construction verification, while retaining the expressiveness of set theory. Second, D provides new expressive power, which makes it possible to internalize and prove inside D the standard meta-theoretic properties of constructive systems, such as Numerical Existence Property and Program Extraction. Finally, computation arising from the programming language significantly enriches set theory, as we show that D is stronger than IZF R and that its real numbers behave in a better way.

There are two major foundational frameworks used in mathematics and computer science—set theory and type theory. The former is widely accepted as the foundation of classical mathematics, the latter is being successfully applied in computer science, for the purpose of program verification, programming languages semantics, software engineering and modeling physical systems. We investigate connections between these worlds. More specifically, we prove a normalization theorem for a constructive impredicative set theory IZF. This result makes it possible to exhibit computational content hidden in set theories. We show how to use normalization to extract programs from IZF proofs. We also demonstrate that a small change to IZF can destroy the normalization property. Furthermore, we investigate two extensions of our framework. We first extend IZF to incorporate inaccessible sets, providing a framework powerful enough to provide constructive semantics for popular type theories. We demonstrate that the normalization property holds for the extension, thus enabling program extraction from its proofs. Second, we extend the logic of IZF to incorporate features typical of dependent type theories. We show that unless such extension is done very carefully, the theory will become inconsistent. However, we present a consistent, normalizing extension—a "dependent" set theory IZF D. We show that the proof-theoretic power of IZF D equals that of Zermelo-Fraenkel set theory with Choice, ZFC, the standard foundation of mathematics. (Abstract shortened by UMI.)

Set theories are traditionally based on first-order logic. We show that in a constructive setting, basing a set theory on a dependent logic yields many benefits. To this end, we introduce a dependent impredicative constructive set theory which we call IZF D . Using realizability, we prove that the underlying lambda calculus weakly normalizes, thus enabling program extraction from IZF_D proofs. We also show that IZF D can interpret IZF with Collection. By a wellknown result of Friedman, this establishes IZF D as a remarkably strong theory, with proof-theoretical power equal to that of ZFC. We further demonstrate that IZF D provides a natural framework to interpret first-order definitions, thus removing a longstanding barrier to implementing constructive set theories. Finally, we prove that IZF D extended with excluded middle is consistent, thus paving the way to using our framework in the classical setting as well.

Church's Higher Order Logic is a basis for influential proof assistants -- HOL and PVS. Church's logic has a simple set-theoretic semantics, making it trustworthy and extensible. We factor HOL into a constructive core plus axioms of excluded middle and choice. We similarly factor standard set theory, ZFC, into a constructive core, IZF, and axioms of excluded middle and choice. Then we provide the standard set-theoretic semantics in such a way that the constructive core of HOL is mapped into IZF. We use the disjunction, numerical existence and term existence properties of IZF to provide a program extraction capability from proofs in the constructive core. We can implement the disjunction and numerical existence properties in two different ways: one using Rathjen's realizability for IZF and the other using a new direct weak normalization result for IZF by Moczydlowski. The latter can also be used for the term existence property.