I am a postdoc at the IT University of Copenhagen. I am a member of the Programming, Logic and Semantics research group.

Email: |
nive at itu dk |

Address: |
Rued Langgaards Vej 7, 2300 Copenhagen, Denmark |

Type theory, constructive mathematics, formalization of mathematics, category theory.

- 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), Electron. Notes in Theor. Comput. Sci., Elsevier, to appear. - 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), Lect. Notes in Comput. Sci., Springer, 2017. Agda code - pdf - 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., Springer, 2017. Agda code - pdf - N. Veltri.
**A type-theoretic study of nontermination.**

Thesis in Informatics and System Engineering C123, 143 pp. Tallinn Univ. of Techn., 2017. thesis in TUT DL - Agda code - T. Uustalu, N. Veltri.
**Finiteness and rational sequences, constructively.**

J. of Funct. Program, v. 27, article e13, 2017. Agda code - pdf - J. Chapman, T. Uustalu, N. Veltri.
**Formalizing restriction categories.**

J. of Formaliz. Reason., v. 10, n. 1, pp. 1-36, 2017. Agda code - pdf - 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 - J. Chapman, T. Uustalu, N. Veltri.
**Quotienting the delay monad by weak bisimilarity.**

Math. Struct. in Comput. Sci., to appear.

Conf. version 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 (© Springer) - N. Veltri.
**Two set-based implementations of quotients in type theory.**

In J. Nummenmaa, O. Sievi-Korte, E. Mäkinen, eds., Proc. of 14th Symposium on Programming Languages and Software Tools, SPLST 2015 (Tampere, Oct. 2015), v. 1525 of CEUR Wksh. Proc., pp. 194-205, RWTH Aachen, 2015. Agda code - pdf

- Formalization of the Max-flow Min-cut theorem in Higher-Order Logic. HOL Light code.