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.
for formal topologies, with Peter Schuster
Mathematical Structures in Computer
Science, 107 (1), 2007, pp. 65-80.
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.
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.
interpretations for generalised predicative intuitionistic systems
Ph.D Thesis, Department of Computer Science, University of Manchester, 2002.
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.
and sets: a study on the jump to full impredicativity
Tesi di Laurea, Dipartimento di
Matematica Pura e Applicata, Universitą degli Studi di Padova,
Note: The published papers may
differ from the preprint versions. If you have problems downloading,
reading, or printing the documents, please contact me.
modified: July 18th, 2007.