Two set-based implementations of quotients in type theory. - Niccolò Veltri (SPLST, 2015)

Variations on Noetherianness. - Denis Firsov; Tarmo Uustalu; Niccolò Veltri (MSFP, 2016)

Partiality and Container Monads. - Tarmo Uustalu; Niccolò Veltri (APLAS, 2017)

The Delay Monad and Restriction Categories. - Tarmo Uustalu; Niccolò Veltri (ICTAC, 2017)

Finiteness and rational sequences, constructively. - Tarmo Uustalu; Niccolò Veltri (J. Funct. Program., 2017)

Formalizing Restriction Categories. - James Chapman 001; Tarmo Uustalu; Niccolò Veltri (J. Formaliz. Reason., 2017)

The Sequent Calculus of Skew Monoidal Categories. - Tarmo Uustalu; Niccolò Veltri; Noam Zeilberger (MFPS, 2018)

En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad. - Robin Kaarsgaard; Niccolò Veltri (MPC, 2019)

Guarded Recursion in Agda via Sized Types. - Niccolò Veltri; Niels van der Weide (FSCD, 2019)

Quotienting the delay monad by weak bisimilarity. - James Chapman 001; Tarmo Uustalu; Niccolò Veltri (Math. Struct. Comput. Sci., 2019)

Bisimulation as path type for guarded recursive types. - Rasmus Ejlers Møgelberg; Niccolò Veltri (Proc. ACM Program. Lang., 2019)

Formalizing π-calculus in guarded cubical Agda. - Niccolò Veltri; Andrea Vezzosi (CPP, 2020)

Eilenberg-Kelly Reloaded. - Tarmo Uustalu; Niccolò Veltri; Noam Zeilberger (MFPS, 2020)

Deductive Systems and Coherence for Skew Prounital Closed Categories. - Tarmo Uustalu; Niccolò Veltri; Noam Zeilberger (LFMTP, 2020)

Proof Theory of Partially Normal Skew Monoidal Categories. - Tarmo Uustalu; Niccolò Veltri; Noam Zeilberger (ACT, 2020)

Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory. - Bassel Mannaa; Rasmus Ejlers Møgelberg; Niccolò Veltri (Log. Methods Comput. Sci., 2020)

Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor. - Niccolò Veltri (FSCD, 2021)

Coherence via Focusing for Symmetric Skew Monoidal Categories. - Niccolò Veltri (WoLLIC, 2021)

Inductive and Coinductive Predicate Liftings for Effectful Programs. - Niccolò Veltri; Niels F. W. Voorneveld (MFPS, 2021)

Constructing Higher Inductive Types as Groupoid Quotients. - Niccolò Veltri; Niels van der Weide (Log. Methods Comput. Sci., 2021)

Bicategories in univalent foundations. - Benedikt Ahrens; Dan Frumin; Marco Maggesi; Niccolò Veltri; Niels van der Weide (Math. Struct. Comput. Sci., 2021)

Streams of Approximations, Equivalence of Recursive Effectful Programs. - Niccolò Veltri; Niels F. W. Voorneveld (MPC, 2022)

Normalization by Evaluation for the Lambek Calculus. - Niccolò Veltri (NCL, 2022)

Proof Theory of Skew Non-Commutative MILL. - Tarmo Uustalu; Niccolò Veltri; Cheng-Syuan Wan (NCL, 2022)

Report on PPDP/LOPSTR 2021. - Niccolò Veltri (ACM SIGLOG News, 2022)

Constructive Final Semantics of Finite Bags. - Philipp Joram; Niccolò Veltri (ITP, 2023)

Maximally Multi-focused Proofs for Skew Non-Commutative MILL. - Niccolò Veltri (WoLLIC, 2023)

Semi-Substructural Logics with Additives. - Niccolò Veltri; Cheng-Syuan Wan (LSFA/HCVS, 2023)

Formalizing CCS and π-calculus in Guarded Cubical Agda. - Niccolò Veltri; Andrea Vezzosi (J. Log. Algebraic Methods Program., 2023)

Data Types with Symmetries via Action Containers. - Philipp Joram; Niccolò Veltri (TYPES, 2024)

Directed equality with dinaturality. - Andrea Laretto; Fosco Loregiàn; Niccolò Veltri (CoRR, 2024)

Coherence via focusing for symmetric skew monoidal and symmetric skew closed categories. - Niccolò Veltri (J. Log. Comput., 2025)

Directed First-Order Logic. - Andrea Laretto; Fosco Loregiàn; Niccolò Veltri (CoRR, 2025)