## Publications

Homotopy limits for 2-categories

Submitted for publication, 2007.

The associated sheaf functor theorem in Algebraic Set Theory

Annals of Pure and Applied Logic. Forthcoming.

The cartesian closed bicategory of generalised
species of structures, with M. Fiore, M. Hyland, and G. Winskel

Journal of the London Mathematical Society. Forthcoming.

Spatiality
for formal topologies, with Peter Schuster

Mathematical Structures in Computer
Science, 107 (1), 2007, pp. 65-80.

The
generalised type-theoretic interpretation of constructive set theory,
with Peter Aczel

Journal of Symbolic Logic, 71 (1), 2006, pp. 67-103.

Heyting-valued interpretations for constructive set theories

Annals of Pure and Applied Logic, ** 137** (1-3), 2006, pp. 164-188.

Presheaf models for constructive set theories

In L. Crosilla and P. Schuster (eds.), From Sets and Types to Topology and
Analysis, Oxford University Press, 2005, pp. 62-77.

Wellfounded
trees and dependent polynomial functors, with Martin Hyland

In S. Berardi, M. Coppo, and F. Damiani (eds.),
Types for Proofs and Programs, LNCS 3085, © Springer, 2004, pp.
210-225.

Sheaf
interpretations for generalised predicative intuitionistic systems

Ph.D Thesis, Department of Computer Science, University of Manchester, 2002.

Collection
principles in dependent type theory, with Peter Aczel

In P. Callaghan, Z. Luo, J. McKinna and R. Pollack (eds)*,
Types for Proofs and Programs,**
*LNCS 2277, © Springer,
2002, pp. 1-23.

Types
and sets: a study on the jump to full impredicativity

Tesi di Laurea, Dipartimento di
Matematica Pura e Applicata, Universitą degli Studi di Padova,
1999.

Note: The published papers may
differ from the preprint versions. If you have problems downloading,
reading, or printing the documents, please contact me.

Last
modified: July 18th, 2007.