Quotienting the delay monad by weak bisimilarity J Chapman, T Uustalu, N Veltri International Colloquium on Theoretical Aspects of Computing, 110-125, 2015 | 20 | 2015 |

Quotienting the delay monad by weak bisimilarity J Chapman, T Uustalu, N Veltri Mathematical Structures in Computer Science 29 (1), 67-92, 2019 | 18 | 2019 |

The sequent calculus of skew monoidal categories T Uustalu, N Veltri, N Zeilberger Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, 377-406, 2021 | 10 | 2021 |

Bicategories in univalent foundations B Ahrens, D Frumin, M Maggesi, N Veltri, N van der Weide arXiv preprint arXiv:1903.01152, 2019 | 10 | 2019 |

A type-theoretical study of nontermination N Veltri PhD thesis, Tallinn University of Technology, 2017 | 10 | 2017 |

Formalizing 𝜋-calculus in guarded cubical Agda N Veltri, A Vezzosi Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 9 | 2020 |

The delay monad and restriction categories T Uustalu, N Veltri International Colloquium on Theoretical Aspects of Computing, 32-50, 2017 | 9 | 2017 |

Bisimulation as path type for guarded recursive types RE Møgelberg, N Veltri Proceedings of the ACM on Programming Languages 3 (POPL), 1-29, 2019 | 8 | 2019 |

Guarded recursion in agda via sized types N Veltri, NM van der Weide Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2019 | 5 | 2019 |

Partiality and container monads T Uustalu, N Veltri Asian Symposium on Programming Languages and Systems, 406-425, 2017 | 5 | 2017 |

Variations on Noetherianness D Firsov, T Uustalu, N Veltri arXiv preprint arXiv:1604.01186, 2016 | 5 | 2016 |

Two set-based implementations of quotients in type theory. N Veltri SPLST 1525, 194-205, 2015 | 5 | 2015 |

Finiteness and rational sequences, constructively T Uustalu, N Veltri Journal of Functional Programming 27, 2017 | 4 | 2017 |

Proof theory of partially normal skew monoidal categories T Uustalu, N Veltri, N Zeilberger arXiv preprint arXiv:2101.10487, 2021 | 3 | 2021 |

Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory N Veltri, RE Møgelberg, B Mannaa Logical Methods in Computer Science 16, 2020 | 3 | 2020 |

En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad R Kaarsgaard, N Veltri International Conference on Mathematics of Program Construction, 366-384, 2019 | 3 | 2019 |

Constructing Higher Inductive Types as Groupoid Quotients N van der Weide, N Veltri Logical Methods in Computer Science 17, 2021 | 2 | 2021 |

Deductive Systems and Coherence for Skew Prounital Closed Categories T Uustalu, N Veltri, N Zeilberger arXiv preprint arXiv:2101.03809, 2021 | 2 | 2021 |

Eilenberg-Kelly Reloaded T Uustalu, N Veltri, N Zeilberger Electronic Notes in Theoretical Computer Science 352, 233-256, 2020 | 2 | 2020 |

Constructing Higher Inductive Types as Groupoid Quotients N Veltri, N van der Weide arXiv preprint arXiv:2002.08150, 2020 | 1 | 2020 |