8 citations · 29 across the 15 of their papers we have counts for
15 papers
Derivatives for Containers in Univalent Foundations
Philipp Joram, Niccolò Veltri
Containers conveniently represent a wide class of inductive data types. Their derivatives compute representations of types of one-hole contexts, useful for implementing tree-traver…
Monoid Structures on Indexed Containers
Michele De Pascalis, Tarmo Uustalu, Niccolò Veltrì
Containers represent a wide class of type constructions relevant for functional programming and (co)inductive reasoning. Indexed containers generalize this notion to better fit the…
Doctrinal Semantics of Directed First-Order Logic
Andrea Laretto, Fosco Loregian, Niccolò Veltri
We present a first-order logic equipped with an "asymmetric" directed notion of equality, which can be thought of as rewrites between terms, allowing for types to be interpreted as…
Di- is for Directed: First-Order Directed Type Theory via Dinaturality
Andrea Laretto, Fosco Loregian, Niccolò Veltri
We show how dinaturality plays a central role in the interpretation of directed type theory where types are interpreted as (1-)categories and directed equality is represented by $\…
Semi-Substructural Logics with Additives
Niccolò Veltri, Cheng-Syuan Wan
This work concerns the proof theory of (left) skew monoidal categories and their variants (e.g. closed monoidal, symmetric monoidal), continuing the line of work initiated in recen…
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…
Inductive and Coinductive Predicate Liftings for Effectful Programs
Niccolò Veltri, Niels F. W. Voorneveld
We formulate a framework for describing behaviour of effectful higher-order recursive programs. Examples of effects are implemented using effect operations, and include: execution…
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…
Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory
Bassel Mannaa, Rasmus Ejlers Møgelberg, Niccolò Veltri
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning ab…
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…
Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory
Hakon Robbestad Gylterud, Elisabeth Stenholm, Niccolò Veltri
Non-well-founded material sets have been modelled in Martin-Löf type theory by Lindström using setoids. In this paper we construct models of non-wellfounded material sets in Homoto…
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…
Variations on Noetherianness
Denis Firsov, Tarmo Uustalu, Niccolò Veltri
In constructive mathematics, several nonequivalent notions of finiteness exist. In this paper, we continue the study of Noetherian sets in the dependently typed setting of the Agda…