Related papers: Path Types in Algebraic Type Theory
We present generalized algebraic theories corresponding to slightly modified versions of two of the type theories in our paper Type Theory with Explicit Universe Polymorphism. We first present a generalized algebraic theory for categories…
Abstract algebra provides a large hierarchy of properties that a collection of objects can satisfy, such as forming an abelian group or a semiring. These classifications can arranged into a broad and typically acyclic directed graph. This…
We present two Dialectica-like constructions for models of intensional Martin-L\"of type theory based on G\"odel's original Dialectica interpretation and the Diller-Nahm variant, bringing dependent types to categorical proof theory. We set…
One of the aims of Implicit Computational Complexity is the design of programming languages with bounded computational complexity; indeed, guaranteeing and certifying a limited resources usage is of central importance for various aspects of…
Refinement types sharpen systems of simple and dependent types by offering expressive means to more precisely classify well-typed terms. We present a system of refinement types for LF in the style of recent formulations where only canonical…
The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer,…
We introduce a new model construction for Martin-L\"{o}f intensional type theory, which is sound and complete for the 1-truncated version of the theory. The model formally combines the syntactic model with a notion of realizability; it also…
The algebraic approach to the Constraint Satisfaction Problem (CSP) uses high order symmetries of relational structures -- polymorphisms -- to study the complexity of the CSP. In this paper we further develop one of the methods the…
The use of standard statistical methods, such as maximum likelihood, is often justified based on their asymptotic properties. For suitably regular models, this theory is standard but, when the model is non-regular, e.g., the support depends…
Session types statically prescribe bidirectional communication protocols for message-passing processes and are in a Curry-Howard correspondence with linear logic propositions. However, simple session types cannot specify properties beyond…
We introduce and analyze a new quantity, the path integral ideal, governing the flow of generic discrete theories to the continuum limit and greatly increasing their convergence. The said flow is classified according to the degree of…
It is common to model inductive datatypes as least fixed points of functors. We show that within the Cedille type theory we can relax functoriality constraints and generically derive an induction principle for Mendler-style lambda-encoded…
In the first part of this paper we show that path categories are enriched over groupoids, in a way that is compatible with a suitable 2-category of path categories. In the second part we introduce a new notion of homotopy exponential and…
L-infinity morphisms are studied from the point of view of perturbative quantum field theory, as generalizations of Feynman expansions. The connection with the Hopf algebra approach to renormalization is exploited. Using the coalgebra…
A linear parameter must be consumed exactly once in the body of its function. When declaring resources such as file handles and manually managed memory as linear arguments, a linear type system can verify that these resources are used…
We give a polymorphic account of the relational algebra. We introduce a formalism of ``type formulas'' specifically tuned for relational algebra expressions, and present an algorithm that computes the ``principal'' type for a given…
We investigate the problem of type isomorphisms in the presence of higher-order references. We first introduce a finitary programming language with sum types and higher-order references, for which we build a fully abstract games model…
Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of locally cartesian closed categories (LCCCs) with disjoint coproducts and W-types, and…
There are many ways to represent the syntax of a language with binders. In particular, nominal frameworks are metalanguages that feature (among others) name abstraction types, which can be used to specify the type of binders. The resulting…
We show how (well-established) type systems based on non-idempotent intersection types can be extended to characterize termination properties of functional programming languages with pattern matching features. To model such programming…