8 citations · 16 across the 4 of their papers we have counts for
7 papers
Proof Theory of Skew Non-Commutative MILL
Tarmo Uustalu, Niccolò Veltri, Cheng-Syuan Wan
Monoidal closed categories naturally model NMILL, non-commutative multiplicative intuitionistic linear logic: the monoidal unit and tensor interpret the multiplicative verum and co…
Normalization by Evaluation for the Lambek Calculus
Niccolò Veltri
The syntactic calculus of Lambek is a deductive system for the multiplicative fragment of intuitionistic non-commutative linear logic. As a fine-grained calculus of resources, it h…
Proof Theory of Partially Normal Skew Monoidal Categories
Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
The skew monoidal categories of Szlachányi are a weakening of monoidal categories where the three structural laws of left and right unitality and associativity are not required to…
Deductive Systems and Coherence for Skew Prounital Closed Categories
Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
In this paper, we develop the proof theory of skew prounital closed categories. These are variants of the skew closed categories of Street where the unit is not represented. Skew c…
The Sequent Calculus of Skew Monoidal Categories
Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
Szlachányi's skew monoidal categories are a well-motivated variation of monoidal categories in which the unitors and associator are not required to be natural isomorphisms, but mer…
Bisimulation as path type for guarded recursive types
Rasmus Ejlers Møgelberg, Niccolò Veltri
In type theory, coinductive types are used to represent processes, and are thus crucial for the formal verification of non-terminating reactive programs in proof assistants based o…