Papers



Under development.
If you have the licence, look also at MathSciNet or Zentralblatt MATH

  • PhD-thesis "The type theory of categorical universes"


    • Type theory and categorical universes:



  • "Joyal's arithmetic universe as list-arithmetic pretopos"
    To appear in Theory and Applications of Categories, 2010

  • "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. Löwe, 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.

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

  • "Joyal's arithmetic universes via type theory"
    in Category Theory in 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

  • "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

  • "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

    • Formal topology:


  • "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, 2003

  • "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).