[FOM] Adventures in Formalization

[Freek Wiedijk]

Tim:

>>A great many
>>constructive type theories are used, above all in Coq;
>>unfortunately I have no clear idea how the strength of such
>>formalisms compares with that of ZFC.
>
>I think that this is an important and fundamental question, and not
>just for die-hard fans of ZFC like Friedman.  The one paper that I'm
>aware of that addresses it is "Sets in Coq, Coq in Sets" by Bruno
>Barras.

There is also Peter Aczel's "On Relating Type Theories and
Set Theories".

Freek