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.