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 (almost weekly) 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.

Publications

  1. Niccolò Veltri, Andrea 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 - pdf
  2. Niccolò Veltri, Niels 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 - pdf
  3. Tarmo Uustalu, Niccolò Veltri, Cheng-Syuan 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 - pdf
  4. Niccolò 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.
    pdf
  5. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide. Bicategories in Univalent Foundations.
    Math. Struct. Comput. Sci., v. 31, n. 10, pp. 1232-1269, 2021.
    pdf
  6. Niccolò Veltri, Niels 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 - pdf
  7. Niccolò 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 - pdf
  8. Niccolò 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 - pdf
  9. Niccolò Veltri, Niels 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 - pdf
  10. Tarmo Uustalu, Niccolò Veltri, Noam 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 - pdf
  11. Bassel Mannaa, Rasmus Ejlers Møgelberg, Niccolò 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.
    pdf
  12. Tarmo Uustalu, Niccolò Veltri, Noam 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 - pdf
  13. Tarmo Uustalu, Niccolò Veltri, Noam 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.
    pdf
  14. Tarmo Uustalu, Niccolò Veltri, Noam 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 - pdf
  15. Niccolò Veltri, Andrea 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.
    pdf
  16. Robin Kaarsgaard, Niccolò 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 - pdf
  17. Niccolò Veltri, Niels 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 - pdf
  18. Rasmus Ejlers Møgelberg, Niccolò Veltri. Bisimulation as path type for guarded recursive types.
    Proc. of ACM on Program. Lang., v. 3, n. POPL, article 4, 2019.
    pdf
  19. James Chapman, Tarmo Uustalu, Niccolò Veltri. Quotienting the delay monad by weak bisimilarity.
    Math. Struct. in Comput. Sci., v. 29, n. 1, pp. 67-92, 2019.
    Agda code - pdf
  20. Tarmo Uustalu, Niccolò Veltri, Noam 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 - pdf
  21. Tarmo Uustalu, Niccolò 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 - pdf
  22. Tarmo Uustalu, Niccolò 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 - pdf
  23. Tarmo Uustalu, Niccolò Veltri. Finiteness and rational sequences, constructively.
    J. of Funct. Program, v. 27, article e13, 2017.
    Agda code - pdf
  24. James Chapman, Tarmo Uustalu, Niccolò Veltri. Formalizing restriction categories.
    J. of Formaliz. Reason., v. 10, n. 1, pp. 1-36, 2017.
    Agda code - pdf
  25. Denis Firsov, Tarmo Uustalu, Niccolò 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 - pdf
  26. James Chapman, Tarmo Uustalu, Niccolò 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 - pdf
  27. Niccolò 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 - pdf

PhD Thesis

Other stuff