In homotopy type theory, a natural number type is freely generated by an element and an endomorphism. Similarly, an integer type is freely generated by an element and an automorphism. Using only dependent sums, identity types, extensional dependent ...

In this paper, we present a novel calculus of inductive linear constructions (CILC), combining linear types and dependent types. Our type theory addresses a looming issue in the research on linear dependent types: the lack of a general mechanism for ...

With the growing practice of mechanizing language metatheories, it has become ever more pressing that interactive theorem provers make it easy to write reusable, extensible code and proofs. This paper presents a novel language design geared towards ...

In functional programming languages, generalized algebraic data types (GADTs) are very useful as the unnecessary pattern matching over them can be ruled out by the failure of unification of type arguments. In dependent type systems, this is usually ...

Quotient inductive-inductive types (QIITs) are generalized inductive types which allow sorts to be indexed over previously declared sorts, and allow usage of equality constructors. QIITs are especially useful for algebraic descriptions of type theories ...

We present an architectural design of a library for Bayesian modelling and inference in modern functional programming languages. The novel aspect of our approach are modular implementations of existing state-of-the-art inference algorithms. Our design ...

Lenses are one the most popular approaches to define bidirectional transformations between data models. A bidirectional transformation with view-update, denoted a lens, encompasses the definition of a forward transformation projecting concrete models ...

We introduce variant types and a pattern matching operation to synchronous dataflow languages. These languages are used in the design of reactive systems. As these systems grow increasingly complex, the need for abstraction mechanisms, in particular, ...

In a previous work ("Abstract Data Type Systems", TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed λ-calculus enriched by pattern-matching definitions following a ...

Within the setting of the categorical approach to total functional programming, we introduce a "many-in-one" recursion scheme that neatly unifies a variety of seemingly diverging strengthenings of the basic recursion scheme of iteration. The new scheme ...

We present a basis for a category-theoretic account of Mendler-style inductive types. The account is based on suitably defined concepts of Mendler-style algebra and algebra homomorphism; Mendler-style inductive types are identified with initial Mendler-...