# Niccolò Veltri

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

## Contact

**Email:** |
nive at itu dk |

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

## Research interests

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

## Publications

- R.E. Møgelberg, N. Veltri.
**Bisimulation as path type for guarded recursive types.**
POPL 2019. arXiv
- T. Uustalu, N. Veltri, N. Zeilberger.
**The sequent calculus of skew monoidal categories.**
MFPS XXXIV. Agda code - pdf
- J. Chapman, T. Uustalu, N. Veltri.
**Quotienting the delay monad by weak bisimilarity.**
Journal version of the ICTAC 2015 paper. Math. Struct. in Comput. Sci., to appear.
- T. Uustalu, N. Veltri.
**Partiality and container monads.**
APLAS 2017. Agda code - pdf
- T. Uustalu, N. Veltri.
**The delay monad and restriction categories.**
ICTAC 2017. Agda code - pdf
- N. Veltri.
**A type-theoretic study of nontermination.**
PhD Thesis 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.**
MSFP 2016. Agda code -
pdf
- J. Chapman, T. Uustalu, N. Veltri.
**Quotienting the delay monad by weak bisimilarity.**
ICTAC 2015. Agda code -
pdf
- N. Veltri.
**Two set-based implementations of quotients in type theory.**
SPLST 2015. Agda code -
pdf

## Other stuff

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