Type theory for foundation of constructive mathematics: in Logical Methods in Computer Science, 18(4) (2022) in Logical Methods in Computer Science, 17(2) (2021) Archive for Mathematical Logic, 57(7-8):873--888, 2018 (revised version) 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 IfColog Journal of Logics and their Applications, 3(4):595--668, 2016 Post-proceedings TYPES'14 in Leibniz International Proceedings in Informatics (LIPIcs), 2015 Annals of Pure and Applied Logic 160(3):319--354, 2009 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 in ''From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics", (L. Crosilla and P. Schuster eds.) Oxford University Press, 2005. in Types for proofs and programs. International workshop, TYPES '98. T. Altenkirch, W. Naraschewski and B. Reus editors, LNCS, 1999 in Mathematical Logic Quarterly, 45, 1999 "Direzioni della ricerca logica in Italia 2", ETS 2018, H.Hosni, G. Lolli, C. Toffalori eds. (in Italian) |
Categorical logic: 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 in Tbilisi Mathematical Journal, 10(3),141--166, 2017 (revised version) 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) Applied Categorical Structures, 2013, DOI 10.1007/s10485-013-9360-5 (revised version) Theory and Applications of Categories 27(17):445--463, 2013 (revised version) Logica Universalis,7(3): 371-402, 2013 (revised version) Journal of Pure and Applied Algebra, 216(8-9):2049--2067, 2012 Theory and Applications of Categories, 24(3):39--83, 2010 in Category Theory and Computer Science (CTCS) 2004, Electronic Notes in Theoretical Computer Science, vol.122, 2005 in Category Theory and Computer Science (CTCS) 2002, Electronic Notes in Theoretical Computer Science, vol.69, 2003 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) Technical Report, University of Birmingham, CSR-99-14, 1999 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: in Applied Categorical Structures, volume 13(1):1--36, 2005 in Proc. of Foundations of Software Science and Computation Structures, LNCS, J. Tiuryn editor, 2000 |
Constructive topology: in Logic and Logical Philosophy 22,167--199,2013 DOI: 10.12775/LLP.2013.010 in Journal of Logic and Analysis, 5(2):1--45, 2013 Logic Journal of IGPL, 21(1), 2013. in Journal of Symbolic Logic, 69(4):967--1005, 2004. in Workshop on Domains VI, Electronic Notes in Theoretical Computer Science, vol.73, 2004 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: |
If you have the licence, look also at MathSciNet or Zentralblatt MATH |