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.

Papers

  1. N. Veltri, C.-S. Wan, Craig interpolation for semi-substructural logics.
    Preprint, 2024.
    Agda code - paper
  2. A. Laretto, F. Loregian, N. Veltri. Directed equality with dinaturality.
    Preprint, 2024.
    paper
  3. H. R. Gylterud, E. Stenholm, N. Veltri. Terminal coalgebras and non-wellfounded sets in Homotopy Type Theory.
    Preprint, 2024.
    paper
  4. 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
  5. 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
  6. 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
  7. N. Veltri. Coherence via focusing for symmetric skew monoidal and symmetric skew closed categories.
    J. Log. Comput., to appear.
    Agda code
  8. 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 - pdf
  9. 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 - pdf
  10. 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 - pdf
  11. 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.
    pdf
  12. 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.
    pdf
  13. 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 - pdf
  14. 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 - pdf
  15. 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 - pdf
  16. 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 - pdf
  17. 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 - pdf
  18. 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.
    pdf
  19. 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 - pdf
  20. 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.
    pdf
  21. 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 - pdf
  22. 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.
    pdf
  23. 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 - pdf
  24. 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 - pdf
  25. 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.
    pdf
  26. 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 - pdf
  27. 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 - pdf
  28. 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 - pdf
  29. 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 - pdf
  30. T. Uustalu, N. Veltri. Finiteness and rational sequences, constructively.
    J. of Funct. Program, v. 27, article e13, 2017.
    Agda code - pdf
  31. J. Chapman, T. Uustalu, N. Veltri. Formalizing restriction categories.
    J. of Formaliz. Reason., v. 10, n. 1, pp. 1-36, 2017.
    Agda code - pdf
  32. 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 - pdf
  33. 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 - pdf
  34. 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 - pdf

PhD Thesis

Other stuff