Papers on linear logic are on a separate page.
The interaction between category theory and set theory (in "Mathematical Applications of Category Theory," edited by J. Gray, Contemporary Mathematics 30 (1984) 5--29)
PDFThis paper is based on a lecture about the various connections between category theory and set theory. Some interactions arise from set theory's foundational role in mathematics. Others arise from category theory's role of clarifying and unifying concepts in many areas of mathematics. We also discuss categories with set-theoretic structure, primarily topoi, and some suggestive but not fully understood connections between particular topics in set theory and category theory.
I thank Dave Childs for producing an electronic version of this paper.
An induction principle and pigeonhole principle for K-finite sets (J. Symbolic Logic 59 (1995) 1186--1193)
PostScript or PDF
We establish a course-of-values induction principle for K-finite sets in intuitionistic type theory. Using this principle, we prove a pigeonhole principle conjectured by Benabou and Loiseau. We also comment on some variants of this pigeonhole principle.
Seven trees in one (J. Pure Appl. Alg. 103 (1995) 1-21)
PostScript or PDF
Following a remark of Lawvere, we explicitly exhibit a particularly elementary bijection between the set T of finite binary trees and the set T^7 of seven-tuples of such trees. "Particularly elementary" means that the application of the bijection to a seven-tuple of trees involves case distinctions only down to a fixed depth (namely four) in the given seven-tuple. We clarify how this and similar bijections are related to the free commutative semiring on one generator X subject to X=1+X^2. Finally, our main theorem is that the existence of particularly elementary bijections can be deduced from the provable existence, in intuitionistic type theory, of any bijections at all.
Topoi and Computation (Bull. European Assoc. Theoret. Comp. Sci. 36 (1988) 57-65)
PostScript or PDF
This is the written version of a talk given at the C.I.R.M. Workshop on Logic in Computer Science at Marseille in June, 1988. Its purpose is to argue that there is a close connection between the theory of computation and the geometric side of topos theory. We begin with a brief outline of the history and basic concepts of topos theory.