Niccolò Veltri

I am an Assistant Professor at the Department of Software Science of Tallinn University of Technology.
I am a member of the Logic and Semantics research group.
We run a regular research seminar, the Theory Seminar (TSEM).

Contact

Email: niccolo at cs ioc ee
Address: Akadeemia tee 21b, 12618 Tallinn, Estonia

Research interests

Type theory, programming language semantics, formalization of mathematics, categorical proof theory.

PhD students

Papers

  1. N. Veltri, C.-S. Wan. An Agda formalization of nonassociative Lambek calculus and its metatheory.
    In G. L. Pozzato, T. Uustalu, eds., Proc. of 34th Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX'25 (Reykjavik, Sept./Oct. 2025), Lect. Notes in Comput. Sci., Springer, to appear.
    Agda code
  2. M. De Pascalis, T. Uustalu, N. Veltri. Monoid structures on indexed containers.
    In H. Barbosa, C. Ringeissen, eds., Proc. of 20th Int. Symp. on Logical and Semantic Frameworks, with Applications, LSFA'25 (Brasília, Oct. 2025), Electron. Proc. in Theor. Comput. Sci., Open Publishing Assoc., to appear.
    Agda code
  3. P. Joram, N. Veltri. Data types with symmetries via action containers.
    In R. E. Møgelberg, B. van der Berg eds., Proc. of 30th Int. Conf. on Types for Proofs and Programs, TYPES 2024 (Copenhagen, June 2024), v. 336 of Leibniz Int. Proc. in Inform., art. 6, 21 pp., Dagstuhl Publishing, 2025.
    Agda code - paper
  4. A. Laretto, F. Loregian, N. Veltri. Directed first-order logic.
    Preprint, 2025.
    paper
  5. N. Veltri, C.-S. Wan. Craig interpolation for a semi-substructural logic.
    Studia Logica, to appear, 2025.
    Agda code - paper
  6. A. Laretto, F. Loregian, N. Veltri. Directed equality with dinaturality.
    Preprint, 2024.
    paper
  7. H. R. Gylterud, E. Stenholm, N. Veltri. Terminal coalgebras and non-wellfounded sets in Homotopy Type Theory.
    Preprint, 2024.
    paper
  8. N. Veltri, C.-S. Wan. Semi-substructural logics with additives.
    In T. Kutsia, D. Ventura, D. Monniaux, J. F. Morales, eds., Proc. of 18th Int. Wksh. on Logical and Semantic Frameworks with Applications, LSFA 2023 (Rome, July 2023) and 10th Wksh. of Horn Clauses for Verification and Synthesis, HCVS 2023 (Paris, Apr. 2023), v. 402 of Electron. Proc. in Theor. Comput. Sci., pp. 63-80. Open Publishing Assoc., 2024.
    Agda code - paper
  9. N. Veltri. Maximally multi-focused proofs for skew non-commutative MILL.
    In H. H. Hansen, A. Scedrov, R. J. G. B. de Queiroz eds., Proc. of 29th Int. Wksh. on Logic, Language and Information, WoLLIC 2023 (Halifax, NS, July 2023), v. 13923 of Lect. Notes in Comput. Sci., pp. 377-393. Springer, 2023.
    Agda code - paper
  10. P. Joram, N. Veltri. Constructive final semantics of finite bags.
    In A. Naumowicz, R. Thiemann, eds., Proc. of 14th Int. Conf. on Interactive Theorem Proving, ITP 2023 (Białystok, July/Aug. 2023), v. 268 of Leibniz Int. Proc. in Inform., art. 20, 19 pp., Dagstuhl Publishing, 2023.
    Agda code - paper
  11. N. Veltri. Coherence via focusing for symmetric skew monoidal and symmetric skew closed categories.
    J. Log. Comput., to appear.
    Agda code
  12. N. Veltri, A. Vezzosi. Formalizing CCS and π-calculus in Guarded Cubical Agda.
    J. Log. and Algebraic Methods in Comput., v. 131, art. 100846, 23 pp., 2023.
    Agda code - paper
  13. N. Veltri, N. Voorneveld. Streams of approximations, equivalence of recursive effectful programs.
    In E. Komendantskaya, ed., Proc. of 14th Int. Conf. on Mathematics of Program Construction, MPC 2022 (Tbilisi, Sept. 2022), v. 13544 of Lect. Notes in Comput. Sci., pp. 198-221. Springer, 2022.
    Agda code - paper
  14. T. Uustalu, N. Veltri, C.-S. Wan. Proof theory of skew non-commutative MILL.
    In A. Indrzejczak, M. Zawidzki, eds., Proc. of 10th Int. Conf. on Non-classical Logics: Theory and Applications, NCL '22 (Łódź, March 2022), v. 358 of Electron. Proc. in Theor. Comput. Sci., pp. 118-135. Open Publishing Assoc., 2022.
    Agda code - paper
  15. N. Veltri. Normalization by evaluation for the Lambek calculus.
    In A. Indrzejczak, M. Zawidzki, eds., Proc. of 10th Int. Conf. on Non-classical Logics: Theory and Applications, NCL '22 (Łódź, March 2022), v. 358 of Electron. Proc. in Theor. Comput. Sci., pp. 102-117. Open Publishing Assoc., 2022.
    paper
  16. B. Ahrens, D. Frumin, M. Maggesi, N. Veltri, N. van der Weide. Bicategories in Univalent Foundations.
    Math. Struct. Comput. Sci., v. 31, n. 10, pp. 1232-1269, 2021.
    paper
  17. N. Veltri, N. Voorneveld. Inductive and coinductive predicate liftings for effectful programs.
    In A. Sokolova, ed., Proc. of 37th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXVII (Salzburg, Aug./Sept. 2021), v. 351 of Electron. Proc. in Theor. Comput. Sci., pp. 260-277. Open Publishing Assoc., 2021.
    Agda code - paper
  18. N. Veltri. Coherence via focusing for symmetric skew monoidal categories.
    In A. Silva, R. Wassermann, R. de Queiroz, eds., Proc. of 27th Wksh. on Logic, Language, Information and Computation, WoLLIC 2021 (Oct. 2021), v. 13038 of Lect. Notes in Comput. Sci., pp. 184-200. Springer, 2021.
    Agda code - paper
  19. N. Veltri. Type-theoretic constructions of the final coalgebra of the finite powerset functor.
    In N. Kobayashi, ed., Proc. of 6th Int. Conf. on Formal Structures for Computation and Deduction, FSCD 2021 (Buenos Aires, July 2021), Leibniz Int. Proc. in Inform., v. 195 of Leibniz Int. Proc. in Inf., article 22. Dagstuhl Publishing, 2021.
    Agda code - paper
  20. N. Veltri, N. van der Weide. Constructing higher inductive types as groupoid quotients.
    Log. Methods Comput. Sci., v.17, n. 2, article 8, 42 pp., 2021.
    UniMath code - paper
  21. T. Uustalu, N. Veltri, N. Zeilberger. Deductive systems and coherence for skew prounital closed categories.
    In C. Sacerdoti Coen, A. Tiu, eds., Proc. of 15th Int. Wksh. on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP 2020 (Paris, June 2020), v. 332 of Electron. Proc. in Theor. Comput. Sci., pp. 35-53, Open Publishing Assoc., 2021.
    Agda code - paper
  22. B. Mannaa, R. E. Møgelberg, N. Veltri. Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory.
    Log. Methods Comput. Sci., v.16, n. 4, article 17, 31 pp., 2020.
    paper
  23. T. Uustalu, N. Veltri, N. Zeilberger. Proof theory of partially normal skew monoidal categories.
    In D. Spivak, J. Vicary, eds., Proc. of 3rd Applied Category Theory Conf., ACT 2020 (Cambridge, MA, July 2020), v. 333 of Electron. Proc. in Theor. Comput. Sci., pp. 230-246, Open Publishing Assoc., 2021.
    Agda code - paper
  24. T. Uustalu, N. Veltri, N. Zeilberger. Eilenberg-Kelly reloaded.
    In P. Johann, ed., Proc. of 36th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXVI (Paris, June 2020), v. 352 of Electron. Notes in Theor. Comput. Sci., pp. 233-256, Elsevier, 2020.
    paper
  25. T. Uustalu, N. Veltri, N. Zeilberger. The sequent calculus of skew monoidal categories.
    In C. Casadio, P. J. Scott, eds., Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, v. 20 of Outstanding Contributions to Logic, pp. 377-406, Springer, 2021.
    Agda code - paper
  26. N. Veltri, A. Vezzosi. Formalizing π-calculus in Guarded Cubical Agda.
    In Proc. of 9th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs, CPP 2020 (New Orleans, LA, Jan. 2020), pp. 270-283. ACM Press, 2020.
    paper
  27. R. Kaarsgaard, N. Veltri. En garde! Unguarded iteration for reversible computation in the delay monad.
    In G. Hutton, ed., Proc. of 13th Int. Conf. on Mathematics of Program Construction, MPC 2019 (Porto, Oct. 2019), v. 11825 of Lect. Notes in Comput. Sci., pp. 366-384. Springer, 2019.
    Agda code - paper
  28. N. Veltri, N. van der Weide. Guarded recursion in Agda via sized types.
    In H. Geuvers, ed., Proc. of 4th Int. Conf. on Formal Structures for Computation and Deduction, FSCD 2019 (Dortmund, June 2019), v. 131 of Leibniz Int. Proc. in Inf., article 32. Dagstuhl Publishing, 2019.
    Agda code - paper
  29. R. E. Møgelberg, N. Veltri. Bisimulation as path type for guarded recursive types.
    Proc. of ACM on Program. Lang., v. 3, n. POPL, article 4, 2019.
    paper
  30. J. Chapman, T. Uustalu, N. Veltri. Quotienting the delay monad by weak bisimilarity.
    Math. Struct. in Comput. Sci., v. 29, n. 1, pp. 67-92, 2019.
    Agda code - paper
  31. T. Uustalu, N. Veltri, N. Zeilberger. The sequent calculus of skew monoidal categories.
    In S. Staton, ed., Proc. of 34th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXIV (Halifax, NS, June 2018), v. 341 of Electron. Notes in Theor. Comput. Sci., pp. 345-370. Elsevier, 2018.
    Agda code - paper
  32. T. Uustalu, N. Veltri. Partiality and container monads.
    In B.-Y. E. Chang, ed., Proc. of 15th Asian Symp. on Programming Languages and Systems, APLAS 2017 (Suzhou, Nov. 2017), v. 10695 of Lect. Notes in Comput. Sci., pp. 406-425. Springer, 2017.
    Agda code - paper
  33. T. Uustalu, N. Veltri. The delay monad and restriction categories.
    In D. V. Hung, D. Kapur, eds., Proc. of 14th Int. Coll. on Theoretical Aspects of Computing, ICTAC 2017 (Hanoi, Oct. 2017), v. 10580 of Lect. Notes in Comput. Sci., pp. 32-50. Springer, 2017.
    Agda code - paper
  34. T. Uustalu, N. Veltri. Finiteness and rational sequences, constructively.
    J. of Funct. Program, v. 27, article e13, 2017.
    Agda code - paper
  35. J. Chapman, T. Uustalu, N. Veltri. Formalizing restriction categories.
    J. of Formaliz. Reason., v. 10, n. 1, pp. 1-36, 2017.
    Agda code - paper
  36. D. Firsov, T. Uustalu, N. Veltri. Variations on Noetherianness.
    In R. Atkey, N. Krishnaswami, eds., Proc. of 6th Wksh. on Mathematically Structured Functional Programming, MSFP 2016 (Eindhoven, April 2016), v. 207 of Electron. Proc. in Theor. Comput. Sci., pp. 76-88. Open Publishing Assoc., 2016.
    Agda code - paper
  37. J. Chapman, T. Uustalu, N. Veltri. Quotienting the delay monad by weak bisimilarity.
    In M. Leucker, C. Rueda, F. D. Valencia, eds., Proc. of 12th Int. Coll. on Theoretical Aspects of Computing, ICTAC 2015 (Cali, Oct. 2015), v. 9399 of Lect. Notes in Comput. Sci., pp. 110-125. Springer, 2015.
    Agda code - paper
  38. N. Veltri. Two set-based implementations of quotients in type theory.
    In J. Nummenmaa, O. Sievi-Korte, E. Mäkinen, eds., Proc. of 14th Symp. on Programming Languages and Software Tools, SPLST '15 (Tampere, Oct. 2015), v. 1525 of CEUR Wksh. Proc., pp. 194-205. RWTH Aachen, 2015.
    Agda code - paper

PhD Thesis

Other stuff