Papers




Type theory for foundation of constructive mathematics:



  • "The Compatibility of the Minimalist Foundation with Homotopy Type theory." with Michele Contente
    in Theoretical Computer Science, 991 (2024) 114421, 30 pages.

  • ``A Topological Counterpart of Well-founded Trees in Dependent Type Theory." with
    in ENTICS, vol3, Proceedings of MFPS 2023, 16 pages.

  • "Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice." with Samuele Maschio and Michael Rathjen
    in Logical Methods in Computer Science, 18(4) (2022) (revised version)

  • "A realizability semantics for inductive formal topologies, Church's Thesis and Axiom of Choice." with Samuele Maschio and Michael Rathjen
    in Logical Methods in Computer Science, 17(2) (2021)

  • "Consistency of the intensional level of the Minimalist Foundation with Church's thesis and Axiom of Choice." with Hajime Ishihara, Samuele Maschio and Thomas Streicher
    Archive for Mathematical Logic, 57(7-8):873--888, 2018 (revised version)

  • "Choice rules in dependent type theory"
    in Theory and Applications of Models of Computation - 14th Annual Conference, TAMC 2017, Bern, Switzerland, April 20-22, 2017, Proceedings. Lecture Notes in Computer Science, 12-23, 2017

  • "A predicative variant of a realizability tripos for the Minimalist Foundation" with Samuele Maschio
    IfColog Journal of Logics and their Applications, 3(4):595--668, 2016

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

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



  • "La teoria dei tipi"
    "Direzioni della ricerca logica in Italia 2", ETS 2018, H.Hosni, G. Lolli, C. Toffalori eds. (in Italian)

    • Categorical logic:


  • "A characterizations of generalized existential completions" with Davide Trotta
    in Annals of Pure and Applied Logic, vol.174 (4) 2023

    "A predicative variant of Hyland's Effective Topos" with Samuele Maschio
    in the Journal of Symbolic Logic,vol 86 (2) 2021

    "Elementary Quotient Completions, Church's Thesis, and Partitioned Assemblies" with Fabio Pasquali and Giuseppe Rosolini
    in Logical Methods in Computer Science, 15(2), 2019

  • "Triposes, exact completions, and Hilbert's ε-operator" with Fabio Pasquali and Giuseppe Rosolini
    in Tbilisi Mathematical Journal, 10(3),141--166, 2017 (revised version)

  • "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. p 229-250, De Gruyter, 2016.
    (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