In some cases, I am uncertain which is the best version. This explains some apparent duplications.

- Set theory, philosophical or survey pieces
The first two are on the philosophical motivation for NF. The last two are general surveys of alternative set theories.

- Miscellaneous logic and set theory
- representation of functions and relations in third order logic
and this.
it does have a connection to NF3, of course, but it is not really an NF paper.

- The set of sets hereditarily of size less than kappa exists in ZF

- representation of functions and relations in third order logic
and this.
- Stratified combinatory logic and lambda-calculus
This was the original program of my thesis, and led to the Watson program.

- The Urysohn paper
This was an isolated foray into mainstream mathematics. The paper is based on my Masters thesis. My advisor admitted later that it was really a PhD thesis, but it would have been quite disastrous for me to get a PhD thesis in functional analysis...without knowing any functional analysis!

- Set theory (stratified or typed)
This has been my main line of work. Substantial time spent thinking about the model theory of NFU is manifest in the strong axioms paper, with a footnote in the paper about models preserving information. The tangled type theory paper is the start of my main line of attack on the consistency problem for NF itself. The other papers touch on other consistent fragments of NF or important techniques in NF. The acyclic comprehension paper is about a very peculiar proposal about the axiomatics of NFU...which turns out to work perfectly. The Tarski's Theorem and NFU paper is an oddment.

- Strong axioms of infinity in NFU with errata corrected
- The usual model construction for NFU preserves information
Also this: preserves3 seems to be the submitted version; I have no idea what preserves4 actually is in versioning terms.

- tangled type theory
- cahiers 7 article on modelling fragments of NF
- subsystems of NF with predicativity restrictions
- permutation methods in NF(U) with Forster
- forcing in NFU and NF
- there is a Forster term model of TST
- The acyclic comprehension paper with Zuhair and Nathan.
- Tarski's theorem and NFU and this.

- Strong axioms of infinity in NFU with errata corrected
- Double extension set theory
- The ramified theory of types of Russell
- subsystems of NF with predicativity restrictions
This paper also appears under the general NF set theory heading, but it says something about the type theory of PM.

- type checking the ramified type theory of PM also this and this and this and this.
This is the version of the paper I packed with the sources (visible in my RTT directory).

- subsystems of NF with predicativity restrictions
- Theories of sets and classes with a symmetry criterion for sethood: these lead to versions of NF.
- The Watson theorem prover
- the Watson theorem prover
- Disguising recursively chained rewrite rules as equational theorems (the tactic language of Watson)
- a strong and mechanizable grand logic (the logic of Watson)
This also appeared under stratified lambda calculus above. The untyped lambda calculus paper which appears there also mentions Watson but seems less a Watson paper than this one.

- the Watson theorem prover
- Master's theses of my students (there are three, putting one up now with this reminder to myself)

- The acyclic comprehension paper with Zuhair and Nathan.
- alternative set theory chapter with Thomas and Thierry.
- cahiers 7 article on modelling fragments of NF
- the structure of the ordinals in double extension set theory
- type checking the ramified type theory of PM also this and this and this and this.
This is the version of the paper I packed with the sources (visible in my RTT directory).

- subsystems of NF with predicativity restrictions
- the Urysohn space and its embeddings into Banach spaces and this and this.
- forcing in NFU and NF
- there is a Forster term model of TST
- foundations of mathematics in polymorphic type theory
- systems of combinatory logic based on NFP and NFI and this.
- representation of functions and relations in third order logic
and this.
- permutation methods in NF(U) with Forster
- a strong and mechanizable grand logic (the logic of Watson)
- the set theoretical program of Quine succeeded, but nobody noticed
- Tarski's theorem and NFU and this.
- Strong axioms of infinity in NFU with errata corrected
- Paradoxes in double extension set theories
- Disguising recursively chained rewrite rules as equational theorems (the tactic language of Watson)
- The SEP article on alternative set theories
- Untyped lambda calculus with relative typing
- the Watson theorem prover
- the first symmetric comprehension paper, with superclasses
- the second symmetric comprehension paper, no superclasses
- tangled type theory
- the paper based on my thesis: a combinatory logic equivalent to NF