Editors: Dale Miller, Ugo Dal Lago

This paper introduces a new family of models of intensional Martin-Löf typetheory. We use constructive ordered algebra in toposes. Identity types in themodels are given by a notion of Moore path. By considering a particular grostopos, we show that there is such a model that is non-truncated, i.e. containsnon-trivial structure at all dimensions. In other words, in this model a typein a nested sequence of identity types can contain more than one element, nomatter how great the degree of nesting. Although inspired by existingnon-truncated models of type theory based on simplicial and cubical sets, thenotion of model presented here is notable for avoiding any form of Kan fillingcondition in the semantics of types.

The main observational equivalences of the untyped lambda-calculus have beencharacterized in terms of extensional equalities between Böhm trees. It iswell known that the lambda-theory H*, arising by taking as observables the headnormal forms, equates two lambda-terms whenever their Böhm trees are equal upto countably many possibly infinite eta-expansions. Similarly, two lambda-termsare equal in Morris's original observational theory H+, generated byconsidering as observable the beta-normal forms, whenever their Böhm treesare equal up to countably many finite eta-expansions. The lambda-calculus also possesses a strong notion of extensionality called"the omega-rule", which has been the subject of many investigations. It is alongstanding open problem whether the equivalence B-omega obtained by closingthe theory of Böhm trees under the omega-rule is strictly included in H+, asconjectured by Sallé in the seventies. In this paper we demonstrate that thetwo aforementioned theories actually coincide, thus disproving Sallé'sconjecture. The proof technique we develop for proving the latter inclusion is generalenough to provide as a byproduct a new characterization, based on boundedeta-expansions, of the least extensional equality between Böhm trees.Together, these results provide a taxonomy of the different degrees ofextensionality in the theory of Böhm trees.

We introduce a sequent calculus with a simple restriction of Lambek's productrules that precisely captures the classical Tamari order, i.e., the partialorder on fully-bracketed words (equivalently, binary trees) induced by asemi-associative law (equivalently, right rotation). We establish a focusingproperty for this sequent calculus (a strengthening of cut-elimination), whichyields the following coherence theorem: every valid entailment in the Tamariorder has exactly one focused derivation. We then describe two mainapplications of the coherence theorem, including: 1. A new proof of the latticeproperty for the Tamari order, and 2. A new proof of the Tutte-Chapoton formulafor the number of intervals in the Tamari lattice $Y_n$.

We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D andfunctor F : D --> C", but instead of having a single collection of "objects ofD" with a map to the objects of C, the objects are given as a family indexed byobjects of C, and similarly for the morphisms. This encapsulates a common wayof building categories in practice, by starting with an existing category andadding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that variousproperties of functors are more naturally defined as properties of thecorresponding displayed categories. Grothendieck fibrations, for example, whendefined as certain functors, use equality on objects in their definition. Whendefined instead as certain displayed categories, no reference to equality onobjects is required. Moreover, almost all examples of fibrations in nature are,in fact, categories whose standard construction can be seen as going viadisplayed categories. We therefore propose displayed categories as a basis for the development offibrations in the type-theoretic setting, and similarly for various othernotions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayedcategories also provide a powerful tool in computer formalisation, unifying andabstracting common constructions and proof techniques of category […]

Completion is one of the most studied techniques in term rewriting andfundamental to automated reasoning with equalities. In this paper we presentnew correctness proofs of abstract completion, both for finite and infiniteruns. For the special case of ground completion we present a new proof based onrandom descent. We moreover extend the results to ordered completion, animportant extension of completion that aims to produce ground-completepresentations of the initial equations. We present new proofs concerning thecompleteness of ordered completion for two settings. Moreover, we revisit andextend results of Métivier concerning canonicity of rewrite systems. Allproofs presented in the paper have been formalized in Isabelle/HOL.

We investigate completeness and parametricity for a general class ofrealizability semantics for System F defined in terms of closure operators oversets of $\lambda$-terms. This class includes most semantics used fornormalization theorems, as those arising from Tait's saturated sets andGirard's reducibility candidates. We establish a completeness result for positive types which subsumes thoseexisting in the literature, and we show that closed realizers satisfyparametricity conditions expressed either as invariance with respect to logicalrelations or as dinaturality. Our results imply that, for positive types,typability, realizability and parametricity are equivalent properties of closednormal $\lambda$-terms.

Church's synthesis problem asks whether there exists a finite-state streamtransducer satisfying a given input-output specification. For specificationswritten in Monadic Second-Order Logic (MSO) over infinite words, Church'ssynthesis can theoretically be solved algorithmically using automata and games.We revisit Church's synthesis via the Curry-Howard correspondence byintroducing SMSO, an intuitionistic variant of MSO over infinite words, whichis shown to be sound and complete w.r.t. synthesis thanks to an automata-basedrealizability model.

In the first part of this paper, we define two resource aware typing systemsfor the {\lambda}{\mu}-calculus based on non-idempotent intersection and uniontypes. The non-idempotent approach provides very simple combinatorialarguments-based on decreasing measures of type derivations-to characterize headand strongly normalizing terms. Moreover, typability provides upper bounds forthe lengths of the head reduction and the maximal reduction sequences tonormal-form. In the second part of this paper, the {\lambda}{\mu}-calculus isrefined to a small-step calculus called {\lambda}{\mu}s, which is inspired bythe substitution at a distance paradigm. The {\lambda}{\mu}s-calculus turns outto be compatible with a natural extensionof the non-idempotent interpretationsof {\lambda}{\mu}, i.e., {\lambda}{\mu}s-reduction preserves and decreasestyping derivations in an extended appropriate typing system. We thus derive asimple arithmetical characterization of strongly {\lambda}{\mu}s-normalizingterms by means of typing.