# 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

- 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, to appear. Agda code
- 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, to appear. Agda code
- 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

## Other stuff

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