Related papers: Generic Zero-Cost Reuse for Dependent Types
We introduce the notion of identity coercions between non-indexed and indexed variants of inductive datatypes, such as lists and vectors. An identity coercion translates one type to another such that the coercion function definitionally…
Dependently typed programming languages have become increasingly relevant in recent years. They have been adopted in industrial strength programming languages and have been extremely successful as the basis for theorem provers. There are…
We present a novel dependent linear type theory in which the multiplicity of some variable-i.e., the number of times the variable can be used in a program-can depend on other variables. This allows us to give precise resource annotations to…
We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the type system…
Dependently typed programming languages allow sophisticated properties of data to be expressed within the type system. Of particular use in dependently typed programming are indexed types that refine data by computationally useful…
Over twenty years ago, Abadi et al. established the Dependency Core Calculus (DCC) as a general purpose framework for analyzing dependency in typed programming languages. Since then, dependency analysis has shown many practical benefits to…
For many compiled languages, source-level types are erased very early in the compilation process. As a result, further compiler passes may convert type-safe source into type-unsafe machine code. Type-unsafe idioms in the original source and…
In Open Source Software, resources of any project are open for reuse by introducing dependencies or copying the resource itself. In contrast to dependency-based reuse, the infrastructure to systematically support copy-based reuse appears to…
We present an approach to develop folds for nested data types using dependent types. We call such folds $\textit{dependently typed folds}$, they have the following properties. (1) Dependently typed folds are defined by well-founded…
Type theories with higher-order subtyping or singleton types are examples of systems where computation rules for variables are affected by type information in the context. A complication for these systems is that bounds declared in the…
Programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of data-types: we can finally write correct-by-construction software. However, this extreme accuracy is also a…
We propose a type-based resource usage analysis for the π-calculus extended with resource creation/access primitives. The goal of the resource usage analysis is to statically check that a program accesses resources such as files and…
Type-preserving translations are effective rigorous tools in the study of core programming calculi. In this paper, we develop a new typed translation that connects sequential and concurrent calculi; it is governed by type systems that…
Nakano's later modality can be used to specify and define recursive functions which are causal or synchronous; in concert with a notion of clock variable, it is possible to also capture the broader class of productive (co)programs. Until…
Curry-style system F, ie. system F with no explicit types in terms, can be seen as a core presentation of polymorphism from the point of view of programming languages. This paper gives a characterisation of type isomorphisms for this…
In this paper we describe how to leverage higher-order unification to type check a dependently typed language with meta-variables. The literature usually presents the unification algorithm as a standalone component, however the need to…
The expression problem describes how most types can easily be extended with new ways to produce the type or new ways to consume the type, but not both. When abstract syntax trees are defined as an algebraic data type, for example, they can…
We revisit occurrence typing, a technique to refine the type of variables occurring in type-cases and, thus, capturesome programming patterns used in untyped languages. Although occurrence typing was tied from its inceptionto set-theoretic…
In dependently typed programming, proofs of basic, structural properties can be embedded implicitly into programs and do not need to be written explicitly. Besides saving the effort of writing separate proofs, a most distinguishing and…
Graded Type Theory provides a mechanism to track and reason about resource usage in type systems. In this paper, we develop GraD, a novel version of such a graded dependent type system that includes functions, tensor products, additive…