Abstract This paper addresses the long-standing question of the predicativity of the Mahlo universe. A solution, called the extended predicative Mahlo universe, has been proposed by Kahle and Setzer in the context of explicit mathematics. It makes use of the collection of untyped terms (denoting partial functions) which are directly available in explicit mathematics but not in Martin-Löf type theory. In this paper, we overcome the obstacle of not having direct access to untyped terms in Martin-Löf type theory by formalizing explicit mathematics with an extended predicative Mahlo universe in Martin-Löf type theory with certain indexed inductive-recursive definitions. In this way, we can relate the predicativity question to the fundamental semantics of Martin-Löf type theory in terms of computation to canonical form. As a result, we get the first extended predicative definition of a Mahlo universe in Martin-Löf type theory. To this end, we first define an external variant of Kahle and Setzer’s internal extended predicative universe in explicit mathematics. This is then formalized in Martin-Löf type theory, where it becomes an internal extended predicative Mahlo universe. Although we make use of indexed inductive-recursive definitions that go beyond the type theory $\mathbf {IIRD}$ of indexed inductive-recursive definitions defined in previous work by the authors, we argue that they are constructive and predicative in Martin-Löf’s sense. The model construction has been type-checked in the proof assistant Agda.

Abstract We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end, we simultaneously define the notion of a presentation Σ of a generalized algebraic theory and the associated category CwFΣ of small cwfs with a Σ-structure and cwf-morphisms that preserve Σ-structure on the nose. Our definition refers to the purely semantic notion of uniform family of contexts, types, and terms in CwFΣ. Furthermore, we show how to syntactically construct an initial cwf with a Σ-structure. This result can be viewed as a generalization of Birkhoff’s completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer’s construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of Martin-Löf type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a small category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual cwfs.

There has been sustained interest in functional programming languages with dependent types in recent years. The foundations of dependently typed programming can be traced back to Martin–Löf's work in the 1970s. In the past decades, this vision has given rise to the development of proof assistants and functional programming languages based on dependent types. The increased popularity of systems such as Agda, Coq, Idris, and many others, reflects the growing momentum in this research area. After sending out our first call for papers in October 2015, we are happy to accept six articles in this special issue covering a wide spectrum of topics.

We show that a version of Martin-L\"of type theory with an extensional identity type former I, a unit type N1 , Sigma-types, Pi-types, and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously proved biequivalence. We show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic. Essentially the same construction also shows a slightly strengthened form of the result that equality in extensional Martin-L\"of type theory with one universe is undecidable.

Seely's paperLocally cartesian closed categories and type theory(Seely 1984) contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-Löf type theories with Π, Σ and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the Bénabou–Hofmann interpretation of Martin-Löf type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development, we employ categories with families as a substitute for syntactic Martin-Löf type theories. As a second result, we prove that if we remove Π-types, the resulting categories with families with only Σ and extensional identity types are biequivalent to left exact categories.

The decidability of equality is proved for Martin-Löf type theory with a universe á la Russell and typed beta-eta- equality judgements. A corollary of this result is that the constructor for dependent function types is injective, a property which is crucial for establishing the correctness of the type-checking algorithm. The decision procedure uses normalization by evaluation, an algorithm which first interprets terms in a domain with untyped semantic elements and then extracts normal forms. The correctness of this algorithm is established using a PER-model and a logical relation between syntax and semantics.

Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types.

Solves the decision problem for the simply typed lambda calculus with a strong binary sum, or, equivalently, the word problem for free Cartesian closed categories with binary co-products. Our method is based on the semantic technique known as "normalization by evaluation", and involves inverting the interpretation of the syntax in a suitable sheaf model and, from this, extracting an appropriate unique normal form. There is no rewriting theory involved and the proof is completely constructive, allowing program extraction from the proof.

Abstract The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Löfs universe à la Tarski. A set U0of codes for small sets is generated inductively at the same time as a function T0, which maps a code to the corresponding small set, is defined by recursion on the way the elements of U0are generated. In this paper we argue that there is an underlyinggeneralnotion of simultaneous inductive-recursive definition which is implicit in Martin-Löf's intuitionistic type theory. We extend previously given schematic formulations of inductive definitions in type theory to encompass a general notion of simultaneous induction-recursion. This enables us to give a unified treatment of several interesting constructions including various universe constructions by Palmgren, Griffor, Rathjen, and Setzer and a constructive version of Aczel's Frege structures. Consistency of a restricted version of the extension is shown by constructing a realisability model in the style of Allen.

The traditional notions of strong and weak normalization refer to properties of a binary reduction relation. In this paper we explore an alternative approach to normalization, in which we bypass the reduction relation and instead focus on the normalization function, that is, the function that maps a term to its normal form. We work in an intuitionistic metalanguage, and characterize a normalization function as an algorithm that picks a canonical representative from the equivalence class of convertible terms. This means that we also get a decision algorithm for convertibility.Such a normalization function can be constructed by building an appropriate model and a function quote, which inverts the interpretation function. The normalization function is then obtained by composing the quote function with the interpretation function. We also discuss how to get a simple proof of the property that constructors are one-to-one, which is usually obtained as a corollary of Church–Rosser and normalization in the traditional sense.We illustrate this approach by showing how a glueing model (closely related to the glueing construction used in category theory) gives rise to a normalization algorithm for a combinatory formulation of Gödel System T. We then show how the method extends in a straightforward way when we add cartesian products and disjoint unions (full intuitionistic propositional logic under a Curry–Howard interpretation) and transfinite inductive types such as the Brouwer ordinals.

Abstract A general formulation of inductive and recursive definitions in Martin-Löf's type theory is presented. It extends Backhouse's ‘Do-It-Yourself Type Theory’ to include inductive definitions of families of sets and definitions of functions by recursion on the way elements of such sets are generated. The formulation is in natural deduction and is intended to be a natural generalisation to type theory of Martin-Löf's theory of iterated inductive definitions in predicate logic. Formal criteria are given for correct formation and introduction rules of a new set former capturing definition by strictly positive, iterated, generalised induction. Moreover, there is an inversion principle for deriving elimination and equality rules from the formation and introduction rules. Finally, there is an alternative schematic presentation of definition by recursion. The resulting theory is a flexible and powerful language for programming and constructive mathematics. We hint at the wealth of possible applications by showing several basic examples: predicate logic, generalised induction, and a formalisation of the untyped lambda calculus.

Abstract Networks of communicating processes can be viewed as networks of stream transformers and programmed in a lazy functional language. Thus the correctness of concurrent systems can be reduced to the correctness of functional programs. In this paper such correctness is proved formally in the μ -calculus extended with recursion equations for functional programs. The μ -calculus is chosen since it allows the definition of properties by least fixed points (induction) as well as by greatest fixed points (coinduction), and since greatest fixed points are useful for formalising properties, such as fairness, of infinitely proceeding programs. Moreover, non-deterministic processes are represented as incompletely specified deterministic processes, that is, as properties of stream transformers. This method is illustrated by proving the correctness of the alternating bit protocol.