Related papers: Foundations of Substructural Dependent Type Theory

The unprecedented pace of machine learning research has lead to incredible advances, but also poses hard challenges. At present, the field lacks strong theoretical underpinnings, and many important achievements stem from ad hoc design…

In a Systems Engineering setting, various models are produced using a variety of methods and tools. Focusing on a type of models -- called descriptive models -- which we shall describe, we argue that, while the clarity and precision of…

Linearity and dependency analyses are key to several applications in computer science, especially, in resource management and information flow control. What connects these analyses is that both of them need to model at least two different…

We present a new coherence theorem for comprehension categories, providing strict models of dependent type theory with all standard constructors, including dependent products, dependent sums, identity types, and other inductive types.…

The ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradual typing. These casts all exhibit a common structural…

Formal deductive systems are very common in computer science. They are used to represent logics, programming languages, and security systems. Moreover, writing programs that manipulate them and that reason about them is important and…

We present a unifying framework for type systems for process calculi. The core of the system provides an accurate correspondence between essentially functional processes and linear logic proofs; fragments of this system correspond to…

The logic of Dependence and Independence Bunched Implications (DIBI) is a logic to reason about conditional independence (CI); for instance, DIBI formulas can characterise CI in probability distributions and relational databases, using the…

Parametricity is a key metatheoretic property of type systems, which implies strong uniformity & modularity properties of the structure of types within systems possessing it. In recent years, various systems of dependent type theory have…

In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in…

We introduce $\infty$-type theories as an $\infty$-categorical generalization of the categorical definition of type theories introduced by the second named author. We establish analogous results to the previous work including the…

We seize the opportunity of the publication of selected papers from the \emph{Logic, categories, semantics} workshop in the \emph{Journal of Applied Logic} to survey some current trends in logic, namely intuitionistic and linear type…

Ordered logics and type systems have been used in a variety of applications including computational linguistics, memory allocation, stream processing, logical frameworks, parametricity, and enforcing security protocols. In most…

In categorical realizability, it is common to construct categories of assemblies and categories of modest sets from applicative structures. These categories have structures corresponding to the structures of applicative structures. In the…

Deep learning, despite its remarkable achievements, is still a young field. Like the early stages of many scientific disciplines, it is marked by the discovery of new phenomena, ad-hoc design decisions, and the lack of a uniform and…

Type theory plays an important role in foundations of mathematics as a framework for formalizing mathematics and a base for proof assistants providing semi-automatic proof checking and construction. Derivation of each theorem in type theory…

We study a resource-sensitive fragment of the problem of extracting a logical discipline from a class of neural architectures by passing through categorization. The starting point is not a pre-existing logic but a category of zone-labelled…

We present a domain-specific type theory for constructions and proofs in category theory. The type theory axiomatizes notions of category, functor, profunctor and a generalized form of natural transformations. The type theory imposes an…

We present two logical systems based on dependent types that are comparable to ZFC, both in terms of simplicity and having natural set theoretic interpretations. Our perspective is that of a mathematician trained in classical logic, but…

We give an account of the basic combinatorial structure underlying the notion of type dependency. We do so by considering the category of all dependent sequent calculi, and exhibiting it as the category of algebras for a monad on a presheaf…