Papers




Type theory for foundation of constructive mathematics:


  • "Choice rules in dependent type theory"
    LNCS volume of TAMC 2917, to appear

  • "A predicative variant of a realizability tripos for the Minimalist Foundation" with Samuele Maschio
    IfColog Journal of Logics and their Applications, 73 pages, to appear

  • "An extensional Kleene realizability semantics for the Minimalist Foundation" (revised version) with Samuele Maschio
    Post-proceedings TYPES'14 in Leibniz International Proceedings in Informatics (LIPIcs), 2015

  • "Consistency of the minimalist foundation with Church thesis and Bar Induction"

  • "A minimalist two-level foundation for constructive mathematics"
    Annals of Pure and Applied Logic 160(3):319--354, 2009

  • "Quotients over Minimal Type Theory"
    in "Computation and Logic in the Real World - Third Conference of Computability in Europe, CiE 2007", (Barry Cooper, B. Lwe, and A. Sorbi eds.) LNCS 4497, 2007

  • "Toward a minimalist foundation for constructive mathematics" with Giovanni Sambin
    in ''From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics", (L. Crosilla and P. Schuster eds.) Oxford University Press, 2005.

  • "About effective quotients in constructive type theory."
    in Types for proofs and programs. International workshop, TYPES '98. T. Altenkirch, W. Naraschewski and B. Reus editors, LNCS, 1999

  • "Can you add powersets to Martin-Loef intuitionistic type theory?" with S. Valentini
    in Mathematical Logic Quarterly, 45, 1999


  • Categorical logic:


  • "Relating quotient completions via categorical logic" with Giuseppe Rosolini
    in Dieter Probst and Peter Schuster (eds.), "Concepts of Proof in Mathematics, Philosophy, and Computer Science". Ontos Mathematical Logic. Walter de Gruyter, Berlin. To appear.
    (revised version)

  • "Unifying exact completions" with Giuseppe Rosolini
    Applied Categorical Structures, 2013, DOI 10.1007/s10485-013-9360-5 (revised version)

  • "Elementary quotient completion" with Giuseppe Rosolini
    Theory and Applications of Categories 27(17):445--463, 2013 (revised version)

  • "Quotient completion for the foundation of constructive mathematics" with Giuseppe Rosolini
    Logica Universalis,7(3): 371-402, 2013 (revised version)

  • "An induction principle for consequence in arithmetic universes" with Steve Vickers
    Journal of Pure and Applied Algebra, 216(8-9):2049--2067, 2012

  • "Subspaces of an arithmetic universe via type theory"

  • "Joyal's arithmetic universe as list-arithmetic pretopos"
    Theory and Applications of Categories, 24(3):39--83, 2010

  • "Reflection into models of finite decidable FP-sketches in an arithmetic universe"
    in Category Theory and Computer Science (CTCS) 2004, Electronic Notes in Theoretical Computer Science, vol.122, 2005

  • "Joyal's arithmetic universes via type theory"
    in Category Theory and Computer Science (CTCS) 2002, Electronic Notes in Theoretical Computer Science, vol.69, 2003

  • "Modular correspondence between dependent type theories and categorical universes including pretopoi and topoi."
    in "Mathematical Structures in Computer Science, 15(6):1089--1149, 2005"
    (this is a revised version of "Modular correspondence between dependent type theories and categorical universes."
    Mittag-Leffler preprint, 2001)

  • "The typed calculus of arithmetic universes."
    Technical Report, University of Birmingham, CSR-99-14, 1999

  • "The internal type theory of an Heyting Pretopos."
    in Types for Proofs and Programs. Selected papers of International Workshop Types '96, Aussois, E. Gimenez, C.Paulin-Mohring editors, LNCS, 1998.


  • Intuitionistic Linear Logic and its categorical semantics:


  • Relating Categorical Semantics for Intuitionistic Linear Logic with P. Maneggia, V. de Paiva and E. Ritter
    in Applied Categorical Structures, volume 13(1):1--36, 2005

  • "Categorical Models for Intuitionistic and Linear Type Theory." with V. de Paiva and E. Ritter
    in Proc. of Foundations of Software Science and Computation Structures, LNCS, J. Tiuryn editor, 2000

  • Constructive topology:


  • ``Why topology in the Minimalist Foundation must be pointfree" with G. Sambin
    in Logic and Logical Philosophy 22,167--199,2013 DOI: 10.12775/LLP.2013.010

  • "Convergence in Formal Topology: a unifying notion" with F. Ciraulo and G. Sambin
    in Journal of Logic and Analysis, 5(2):1--45, 2013

  • "Constructive version of Boolean algebra" with F. Ciraulo and P. Toto
    Logic Journal of IGPL, 21(1), 2013.

  • "A structural investigation on formal topology: coreflection of formal covers and exponentiability". with S. Valentini
    in Journal of Symbolic Logic, 69(4):967--1005, 2004.

  • "Exponentiation of Scott formal topologies" with S. Valentini
    in Workshop on Domains VI, Electronic Notes in Theoretical Computer Science, vol.73, 2004

  • "Predicative exponentiation of locally compact formal topologies over inductively generated ones"
    in ''From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics", (L. Crosilla and P. Schuster eds.) Oxford University Press, 2005. (for more detailed proofs see the technical report).

  • PhD-thesis:

  • "The type theory of categorical universes"


  • If you have the licence, look also at MathSciNet or Zentralblatt MATH