Title: A Framework for Formalizing Set Theories

An unofficial abstract:

This is my annual report on the progress done in the research
on safety relations and their use in Set theory. The talk will
be self-contained.

An official abstract:
 
We present a new unified framework for formalizations of axiomatic set theories
of different strength, from rudimentary set theory to full $ZF$. It
allows the use of abstract terms, but provides a  static check of
their validity.  Like the inconsistent ``ideal calculus" for set theory,
it is based on just two set-theoretical principles: extensionality and
comprehension (to which one may add
the axiom of foundations and the axiom of choice).
Comprehension is formulated as:
$x\in\{x\mid\fe\}\leftrightarrow\fe$, where $\{x\mid\fe\}$
is a valid term of the theory (the formula $\fe$ itself may
contain other valid abstract terms).  In order for $\{x\mid\fe\}$
to be a valid term, $\fe$ should be {\em safe} with respect to $\{x\}$,
where safety is a relation between formulas and finite sets of
variables.  The various systems we consider differ from each other only with
respect to the safety relations they employ. These relations are all
purely syntactically defined (using some induction on the logical
structure of formulas).  The basic one
is based on the safety relation which implicitly underlies
commercial query languages for relational database systems (like SQL),
and corresponds to the minimal set theory in which all
rudimentary set functions are definable.
Our framework makes it possible to reduce all extensions by 
definitions to abbreviations. Hence it is very convenient
for mechanical manipulations and for interactive theorem proving. It
also provides a unified treatment of comprehension axioms and of 
absoluteness properties of formulas.