Niccolò Veltri

42 papers B 11C 5Journal 17Unranked 9

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Di- is for Directed: First-Order Directed Type Theory via Dinaturality. Proc. ACM Program. Lang. Andrea Laretto, Fosco Loregiàn, Niccolò Veltri
2025	B	`conf`	An Agda Formalization of Nonassociative Lambek Calculus and its Metatheory. TABLEAUX Niccolò Veltri, Cheng-Syuan Wan
2025	J	`jnl`	Coherence via focusing for symmetric skew monoidal and symmetric skew closed categories. J. Log. Comput. Niccolò Veltri
2025	J	`jnl`	Derivatives for Containers in Univalent Foundations. CoRR Philipp Joram, Niccolò Veltri
2025	J	`jnl`	Directed First-Order Logic. CoRR Andrea Laretto, Fosco Loregiàn, Niccolò Veltri
2025	—	`conf`	Monoid Structures on Indexed Containers. LSFA Michele De Pascalis, Tarmo Uustalu, Niccolò Veltri
2024	—	`conf`	Data Types with Symmetries via Action Containers. TYPES Philipp Joram, Niccolò Veltri
2024	J	`jnl`	Directed equality with dinaturality. CoRR Andrea Laretto, Fosco Loregiàn, Niccolò Veltri
2023	B	`conf`	Constructive Final Semantics of Finite Bags. ITP Philipp Joram, Niccolò Veltri
2023	J	`jnl`	Formalizing CCS and J. Log. Algebraic Methods Program. Niccolò Veltri, Andrea Vezzosi
2023	C	`conf`	Maximally Multi-focused Proofs for Skew Non-Commutative MILL. WoLLIC Niccolò Veltri
2023	—	`conf`	Semi-Substructural Logics with Additives. LSFA/HCVS Niccolò Veltri, Cheng-Syuan Wan
2022	—	`conf`	Normalization by Evaluation for the Lambek Calculus. NCL Niccolò Veltri
2022	—	`conf`	Proof Theory of Skew Non-Commutative MILL. NCL Tarmo Uustalu, Niccolò Veltri, Cheng-Syuan Wan
2022	J	`jnl`	Report on PPDP/LOPSTR 2021. ACM SIGLOG News Niccolò Veltri
2022	B	`conf`	Streams of Approximations, Equivalence of Recursive Effectful Programs. MPC Niccolò Veltri, Niels F. W. Voorneveld
2021	J	`jnl`	Bicategories in univalent foundations. Math. Struct. Comput. Sci. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide
2021	C	`conf`	Coherence via Focusing for Symmetric Skew Monoidal Categories. WoLLIC Niccolò Veltri
2021	J	`jnl`	Constructing Higher Inductive Types as Groupoid Quotients. Log. Methods Comput. Sci. Niccolò Veltri, Niels van der Weide
2021	B	`conf`	Inductive and Coinductive Predicate Liftings for Effectful Programs. MFPS Niccolò Veltri, Niels F. W. Voorneveld
2021	C	`ed.`	PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming, Tallinn, Estonia, September 6-8, 2021 PPDP Niccolò Veltri, Nick Benton, Silvia Ghilezan
2021	B	`conf`	Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor. FSCD Niccolò Veltri
2020	—	`conf`	Deductive Systems and Coherence for Skew Prounital Closed Categories. LFMTP Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
2020	B	`conf`	Eilenberg-Kelly Reloaded. MFPS Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
2020	B	`conf`	Formalizing π-calculus in guarded cubical Agda. CPP Niccolò Veltri, Andrea Vezzosi
2020	—	`conf`	Proof Theory of Partially Normal Skew Monoidal Categories. ACT Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
2020	J	`jnl`	The Sequent Calculus of Skew Monoidal Categories. CoRR Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
2020	J	`jnl`	Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory. CoRR Bassel Mannaa, Rasmus Ejlers Møgelberg, Niccolò Veltri
2020	J	`jnl`	Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory. Log. Methods Comput. Sci. Bassel Mannaa, Rasmus Ejlers Møgelberg, Niccolò Veltri
2019	J	`jnl`	Bisimulation as path type for guarded recursive types. Proc. ACM Program. Lang. Rasmus Ejlers Møgelberg, Niccolò Veltri
2019	B	`conf`	En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad. MPC Robin Kaarsgaard, Niccolò Veltri
2019	B	`conf`	Guarded Recursion in Agda via Sized Types. FSCD Niccolò Veltri, Niels van der Weide
2019	J	`jnl`	Quotienting the delay monad by weak bisimilarity. Math. Struct. Comput. Sci. James Chapman, Tarmo Uustalu, Niccolò Veltri
2018	J	`jnl`	Bisimulation as path type for guarded recursive types. CoRR Rasmus Ejlers Møgelberg, Niccolò Veltri
2018	B	`conf`	The Sequent Calculus of Skew Monoidal Categories. MFPS Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
2017	J	`jnl`	Finiteness and rational sequences, constructively. J. Funct. Program. Tarmo Uustalu, Niccolò Veltri
2017	J	`jnl`	Formalizing Restriction Categories. J. Formaliz. Reason. James Chapman, Tarmo Uustalu, Niccolò Veltri
2017	B	`conf`	Partiality and Container Monads. APLAS Tarmo Uustalu, Niccolò Veltri
2017	C	`conf`	The Delay Monad and Restriction Categories. ICTAC Tarmo Uustalu, Niccolò Veltri
2016	—	`conf`	Variations on Noetherianness. MSFP Denis Firsov, Tarmo Uustalu, Niccolò Veltri
2015	C	`conf`	Quotienting the Delay Monad by Weak Bisimilarity. ICTAC James Chapman, Tarmo Uustalu, Niccolò Veltri
2015	—	`conf`	Two set-based implementations of quotients in type theory. SPLST Niccolò Veltri