 |
 |
Selected Papers of the 2nd International Conference on Formal Structures and Deduction (FSCD 2017)
Editors: Dale Miller, Ugo Dal Lago
1. Models of Type Theory Based on Moore Paths
This paper introduces a new family of models of intensional Martin-Löf type theory. We use constructive ordered algebra in toposes. Identity types in the models are given by a notion of Moore path. By considering a particular gros topos, we show that there is such a model that is non-truncated, i.e. contains non-trivial structure at all dimensions. In other words, in this model a type in a nested sequence of identity types can contain more than one element, no matter how great the degree of nesting. Although inspired by existing non-truncated models of type theory based on simplicial and cubical sets, the notion of model presented here is notable for avoiding any form of Kan filling condition in the semantics of types.
Section:
Type theory and constructive mathematics
2. Degrees of extensionality in the theory of Böhm trees and Sallé's conjecture
The main observational equivalences of the untyped lambda-calculus have been characterized in terms of extensional equalities between Böhm trees. It is well known that the lambda-theory H*, arising by taking as observables the head normal forms, equates two lambda-terms whenever their Böhm trees are equal up to countably many possibly infinite eta-expansions. Similarly, two lambda-terms are equal in Morris's original observational theory H+, generated by considering as observable the beta-normal forms, whenever their Böhm trees are 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 a longstanding open problem whether the equivalence B-omega obtained by closing the theory of Böhm trees under the omega-rule is strictly included in H+, as conjectured by Sallé in the seventies. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture. The proof technique we develop for proving the latter inclusion is general enough to provide as a byproduct a new characterization, based on bounded eta-expansions, of the least extensional equality between Böhm trees. Together, these results provide a taxonomy of the different degrees of extensionality in the theory of Böhm trees.
3. A sequent calculus for a semi-associative law
We introduce a sequent calculus with a simple restriction of Lambek's product rules that precisely captures the classical Tamari order, i.e., the partial order on fully-bracketed words (equivalently, binary trees) induced by a semi-associative law (equivalently, right rotation). We establish a focusing property for this sequent calculus (a strengthening of cut-elimination), which yields the following coherence theorem: every valid entailment in the Tamari order has exactly one focused derivation. We then describe two main applications of the coherence theorem, including: 1. A new proof of the lattice property for the Tamari order, and 2. A new proof of the Tutte-Chapoton formula for the number of intervals in the Tamari lattice $Y_n$.
4. Displayed Categories
We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D and functor F : D --> C", but instead of having a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof […]
5. Abstract Completion, Formalized
Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstract completion, both for finite and infinite runs. For the special case of ground completion we present a new proof based on random descent. We moreover extend the results to ordered completion, an important extension of completion that aims to produce ground-complete presentations of the initial equations. We present new proofs concerning the completeness of ordered completion for two settings. Moreover, we revisit and extend results of Métivier concerning canonicity of rewrite systems. All proofs presented in the paper have been formalized in Isabelle/HOL.
6. On completeness and parametricity in the realizability semantics of System F
We investigate completeness and parametricity for a general class of realizability semantics for System F defined in terms of closure operators over sets of $\lambda$-terms. This class includes most semantics used for normalization theorems, as those arising from Tait's saturated sets and Girard's reducibility candidates. We establish a completeness result for positive types which subsumes those existing in the literature, and we show that closed realizers satisfy parametricity conditions expressed either as invariance with respect to logical relations or as dinaturality. Our results imply that, for positive types, typability, realizability and parametricity are equivalent properties of closed normal $\lambda$-terms.
7. A Curry-Howard Approach to Church's Synthesis
Church's synthesis problem asks whether there exists a finite-state stream transducer satisfying a given input-output specification. For specifications written in Monadic Second-Order Logic (MSO) over infinite words, Church's synthesis can theoretically be solved algorithmically using automata and games. We revisit Church's synthesis via the Curry-Howard correspondence by introducing SMSO, an intuitionistic variant of MSO over infinite words, which is shown to be sound and complete w.r.t. synthesis thanks to an automata-based realizability model.
8. Non-idempotent types for classical calculi in natural deduction style
In the first part of this paper, we define two resource aware typing systems for the {\lambda}{\mu}-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments-based on decreasing measures of type derivations-to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the lengths of the head reduction and the maximal reduction sequences to normal-form. In the second part of this paper, the {\lambda}{\mu}-calculus is refined to a small-step calculus called {\lambda}{\mu}s, which is inspired by the substitution at a distance paradigm. The {\lambda}{\mu}s-calculus turns out to be compatible with a natural extensionof the non-idempotent interpretations of {\lambda}{\mu}, i.e., {\lambda}{\mu}s-reduction preserves and decreases typing derivations in an extended appropriate typing system. We thus derive a simple arithmetical characterization of strongly {\lambda}{\mu}s-normalizing terms by means of typing.