Président Du

Professeur Bruno Martin

Professeur Silvia Ghilezan

Delia Kesner

Giuseppe Castagna

Luigi Liquori

Types union, intersection, et dépendants dans le lambda-calcul explicitement typé Jury

Keywords: lambda-calcul, théorie des types, correspondance de Curry-Howard. Combining union, intersection and dependent types lambda-calculus, type theory, Curry-Howard correspondence. ix Remerciements - Γ λx:σ.M : σ → τ

dans le lambda-calcul explicitement typé Résumé :

Le sujet de cette thèse est sur le lambda-calcul décoré avec des types, communément appelé « lambda-calcul typé à la Church ». Nous étudions des versions de ce lambdacalcul muni de types intersections, tels que ceux décrits dans le livre « Lambda-calculus with types » de Barendregt, Dekkers et Statman ; les types unions, qui ont été introduits par Plotkin, MacQueen et Sethi ; et les types dépendants, tels qu'ils ont été décrits par Plotkin, Harper et Honsell lorsqu'ils ont introduit le Logical Framework d'Edinbourgh LF. Les types intersections et unions sont un moyen d'exprimer du polymorphisme ad hoc et sont une alternative au polymorphisme paramétrique de Girard. Les types dépendants ont été introduits pour formaliser la logique intuitionniste avec la correspondance de Curry-Howard. Le système de types obtenu peut être enrichi avec une relation de soutypage décidable. La combinaison de ces trois disciplines de type donne lieu à une famille de calculs qui peuvent être paramétrés et classifiés. Nous appelons le système générique le Delta-calcul. Nous discutons ensuite des décisions de conception qui nous ont amené à la formulation de ces calculs, nous étudions leur métathéorie, et nous présentons divers exemples d'applications avant de présenter une implémentation logicielle du Delta-calcul, avec une description des algorithmes de vérification de type, de raffinement, de soutypage, d'évaluation, ainsi que de l'interface en ligne de commande. Ce travail de recherche peut être vu comme un petit pas franchi dans la direction d'une théorie des types alternative pour définir du polymorphisme dans les langages de programmation et dans les assistants de preuve interactifs.

Chapter 1

Introduction "That logic has advanced in this sure course, even from the earliest times, is apparent from the fact that, since Aristotle, it has been unable to advance a single step and, thus, to all appearance, has reached its completion."

Immanuel Kant, Preface to the second edition of The Critique of Pure Reason, 1787

Prolegomenon

When George Boole wrote Mathematical Analysis of Logic in 1847 [START_REF] Boole | The Mathematical Analysis of Logic, being an essay towards a calculus of deductive reasoning[END_REF], he modestly aimed at an algebraic clarification of Aristotelian logic, and did not immediately realize his work was the beginning of a deep change in the study of mathematics which would later trigger the foundational crisis of mathematics.

In 1903, Bertrand Russell [START_REF] Russell | The Principles of Mathematics[END_REF], in The Principles of Mathematics1 , opened a Pandora's box when he considered "predicates which are not predicable of themselves"2 . As it is widely known nowadays, Russell's contradiction -a modern version of the liar's paradox -consists of defining a predicate P (x) def = ¬x(x), and deducing both P (P ) and ¬P (P ). In order to circumvent this contradiction, Russell introduced, in the Appendix B of the same book, the Doctrine of Types: "The doctrine of types is here put forward tentatively, as affording a possible solution of the contradiction [. . . ]. Every propositional function φ(x) -so it is contended -has, in addition to its range of truth, a range of significance, i.e. a range in which x must lie if φ(x) is to be a proposition at all, whether true or false. This is the first point in the theory of types; the second point is that ranges of significance form types, i.e. if x belongs to the range of significance of φ(x), then there is a class of objects, the type of x, all of which must also belong to the range of significance of φ(x)."

This general idea set the foundation of the (many) theories of types, which were widely developed during the course of the twentieth century. In 1934, Haskell Curry was "concerned with statements [. . . ] of the form "f is a function on X to Y "" [START_REF] Haskell | Functionality in combinatory logic[END_REF]. Haskell Curry, and later William Howard, discovered that rules determining that a function has some type where very similar to logical rules determining that a proof shows the validity of some proposition. The proofs-as-functions/propositions-as-types principle is now known as the Curry-Howard correspondence [START_REF] Howard | The Formulae-as-Types Notion of Construction[END_REF].

In short, types are a tool used to give a notion of a well-formed expression:

-we can use types to describe well-formed propositions and proofs;

-we can use types to describe well-formed computable functions.

Among the most impactful developments from the previous century of type theory as a foundation for mathematics, we can cite Automath by N. G. de Bruijn [START_REF] De Bruijn | Automath, a language for mathematics[END_REF], the first theorem prover, whose development started in the sixties, the intuitionistic type theory of Per Martin-Löf [START_REF] Martin-Löf | Intuitionistic type theory[END_REF], and finally the Calculus of (Inductive) Constructions by Thierry Coquand, Gérard Huet [START_REF] Coquand | The calculus of constructions[END_REF], Frank Pfenning, and Christine Paulin-Mohring [START_REF] Pfenning | Inductively defined types in the calculus of constructions[END_REF], which is the theoretical foundation of the Coq theorem prover [START_REF]The Coq Proof Assistant[END_REF].

The model of computation which is the most associated with type theory is the λcalculus, this language developed by Alonzo Church in the thirties. The pure λ-calculus has two basic operations:

1. the first one is application, simply noted with a space: the expression M N denotes the function M applied to its argument N ; reason for (A ∪ B) ⊃ C, which is also a reason to assert A ⊃ C and B ⊃ C. A simple example of a logical theorem involving intuitionistic disjunction which does not hold for strong disjunction is ((A ⊃ B) ∪ B) ⊃ A ⊃ B. Otherwise there would exist a term which behaves both as I and as K.

-Strong (relevant) implication is yet another proof-functional connective that was interpreted in [8] as a relevant arrow type → r . As explained in [8], it can be viewed as a special case of implication whose related function space is the simplest one, namely the one containing only the identity function. Because the operators ⊃ and → r differ, A → r B → r A is not derivable.

-Dependent types, as introduced in the Edinburgh Logical Framework [START_REF] Harper | A framework for defining logics[END_REF] by Robert Harper, Furio Honsell, and Gordon Plotkin, allows considering proofs as first-class citizens, albeit differently, with respect to proof-functional logics. The interaction of both dependent and proof-functional operators is intriguing. Their combination opens up new possibilities of formal reasoning on proof-theoretic semantics.

We have also implemented a prototype of an interactive theorem prover based on this logical framework, called Bull. For instance, the following code snippet shows the implementation of a polymorphic identity on A and B, using a strong pair, which ensures that id1 and id2 have the same essence.

Definition poly_id : (A

-> A) & (B -> B) := let id1 x := x in let id2 x := x in < id1, id2 >.

Organization of this thesis

This thesis is organized as follows:

-Chapter 2 presents a generic ∆-calculus, i.e. a generic typed λ-calculus with intersection types. We study some of its instances and their properties, as well as their relation with standard λ-calculus with intersection types; -Chapter 3 extends the previous ∆-calculus with union types, and defines a typed λcalculus λ@ BDdL , and recalls the original λ-calculus [7] these new systems are inspired from;

-Chapter 4 sketches the logical interpretation of intersection and union types. More precisely, we define an interpretation of typing judgments M : σ into a first-order logical proposition r σ [M ] in the logic NJ(β);

-Chapter 5 defines a subtyping algorithm for intersection and union types. This algorithm is then fully implemented and certified in Coq. We detail the Coq implementation;

-Chapter 6 extends the ∆-calculus by adding dependent types, in the style of the Edinburgh Logical Framework (LF). We call the resulting system the ∆-framework LF ∆ , and we prove its metatheoretical properties; -Chapter 7 presents an OCaml implementation of the ∆-framework into an interactive theorem prover, called Bull. The technical details of the implementation (syntax, semantics, typechecking, and Read-Eval-Print loop) are described;

-Chapter 8 presents some examples of encodings in the ∆-framework, as well as their implementation in Bull.

Publications

During the course of my thesis, I published the following conference papers:

-

Software

During the course of my thesis, I developed a prototype of an interactive theorem prover implementing the ∆-framework, called Bull [START_REF] Stolze | [END_REF].

Related works

In order to foster the imagination of the reader about the topic we will study in this thesis, we shortly present works related to our field of interest.

λ-calculi with intersection types à la Curry

Intersection type theories T were first introduced as a form of ad hoc polymorphism in (pure) λ-calculi à la Curry. The paper by Barendregt,Coppo,and Dezani [11] is a classic reference, while [START_REF] Barendregt | Lambda calculus with types[END_REF] is a definitive reference. Intersection type assignment systems λ T ∩ have been well-known in the literature for almost 40 years for many reasons: among them, characterization of strongly normalizing λ-terms [START_REF] Barendregt | Lambda calculus with types[END_REF], λ-models [4], automatic type inference [START_REF] Kfoury | Principality and type inference for intersection types using expansion variables[END_REF], type inhabitation [START_REF] Pawel Urzyczyn | The emptiness problem for intersection types[END_REF][START_REF] Rehof | The complexity of inhabitation with explicit intersection[END_REF], type unification [START_REF] Dudenhefner | The algebraic intersection type unification problem[END_REF]. As intersection had its classical development for type assignment systems, many papers tried to find an explicitly typed λ-calculus à la Church corresponding to the original intersection type assignment systems à la Curry. The programming language Forsythe, by Reynolds [START_REF] Reynolds | Preliminary design of the programming language Forsythe[END_REF], is probably the first reference, while Pierce's Ph.D. thesis [START_REF] Pierce | Programming with intersection types, union types, and bounded polymorphism[END_REF] combines also unions, intersections and bounded polymorphism. Wells et al. [START_REF] Wells | A calculus with polymorphic and polyvariant flow types[END_REF] use intersection types as a foundation for typed intermediate languages for optimizing compilers for higher-order polymorphic programming languages; implementations of typed programming language featuring intersection (and union) types can be found in CDuce [START_REF] Frisch | CDuce[END_REF][START_REF] Frisch | Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types[END_REF], SML-CIDRE [START_REF] Davies | Practical Refinement-Type Checking[END_REF], and in StardustML [START_REF] Dunfield | Refined typechecking with Stardust[END_REF][START_REF] Dunfield | Elaborating intersection and union types[END_REF].

Intersection and union type disciplines started to be investigated in a explicitly typed programming language settings à la Church, much later by Reynolds and Pierce [START_REF] Reynolds | Preliminary design of the programming language Forsythe[END_REF][START_REF] Pierce | Programming with intersection types, union types, and bounded polymorphism[END_REF], Wells et al. [START_REF] Wells | A calculus with polymorphic and polyvariant flow types[END_REF][START_REF] Wells | Branching types[END_REF], Liquori et al. [START_REF] Liquori | Intersection typed system à la Church[END_REF][START_REF] Daniel | Logic and computation in a lambda calculus with intersection and union types[END_REF], Frisch et al. [START_REF] Frisch | Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types[END_REF] and Dunfield [START_REF] Dunfield | Elaborating intersection and union types[END_REF].

λ-calculi with intersection types à la Church

Several calculi à la Church appeared in the literature: they capture the power of intersection types; we briefly review them.

The Forsythe programming language by Reynolds [START_REF] Reynolds | Preliminary design of the programming language Forsythe[END_REF] annotates a λ-abstraction with types as in λx:σ 1 |• • •|σ n .M . However, we cannot type a typed term, whose type erasure is the combinator K ≡ λx.λy.x, with the type (σ → σ → σ) ∩ (τ → τ → τ ).

Pierce [START_REF] Pierce | Programming with intersection types, union types, and polymorphism[END_REF] improves Forsythe by using a for construct to build ad hoc polymorphic typing, as in for α ∈ {σ, τ }.λx:α, λy:α.x. However, we cannot type a typed term, whose type erasure is λx.λy.λz.(x y, x z), with the type [START_REF] Wells | Branching types[END_REF]:

((σ → ρ) ∩ (τ → ρ ) → σ → τ → ρ × ρ ) ∩ ((σ → σ) ∩ (σ → σ) → σ → σ → σ × σ)
Freeman and Pfenning [START_REF] Freeman | Refinement types for ML[END_REF] introduced refinement types, that is types that allow ad hoc polymorphism for ML constructors. Intuitively, refinement types can be seen as subtypes of a standard type: the user first defines a type and then the refinement types of this type. The main motivation for these refinement types is to allow non-exhaustive pattern matching, which becomes exhaustive for a given refinement of the type of the argument. As an example, we can define a type boolexp for boolean expressions, with constructors True, And, Not and Var, and a refinement type ground for boolean expressions without variables, with the same constructors except Var: then, the constructor True has type boolexp ∩ ground, the constructor And has type (boolexp * boolexp → boolexp) ∩ (ground * ground → ground) and so on. However, intersection is meaningful only when using constructors.

Wells et al. [START_REF] Wells | A calculus with polymorphic and polyvariant flow types[END_REF] introduced λ CIL , a typed intermediate λ-calculus for optimizing compilers for higher-order programming languages. The calculus features intersection, union and flow types, the latter being useful to optimize data representation. λ CIL can faithfully encode an intersection type assignment derivation by introducing the concept of virtual tuple, i.e. a special kind of pair whose type erasure leads to exactly the same untyped λ-term. A parallel context and parallel substitution, similar to the notion of [START_REF] Liquori | Towards an intersection typed system à la Church[END_REF][START_REF] Liquori | Intersection typed system à la Church[END_REF], is defined to reduce expressions in parallel inside a virtual tuple. Subtyping is defined only on flow types and not on intersection types: this system can encode the λ CD ∩ type assignment system.

Wells and Haak [START_REF] Wells | Branching types[END_REF] introduced λ B , a more compact typed calculus encoding of λ CIL : in fact, by comparing Figure 1 and Figure 2 of [START_REF] Wells | Branching types[END_REF] we can see that the set of typable terms with intersection types of λ CIL and λ B are the same. In that paper, virtual tuples are removed by introducing branching terms, typable with branching types, the latter representing intersection type schemes. Two operations on types and terms are defined, namely expand, expanding the branching shape of type annotations when a term is substituted into a new context, and select, to choose the correct branch in terms and types. As there are no virtual tuples, reductions do not need to be done in parallel. As in [START_REF] Wells | A calculus with polymorphic and polyvariant flow types[END_REF], the λ CD ∩ type assignment system can be encoded. Frisch, Castagna, and Benzaken [START_REF] Frisch | Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types[END_REF] designed a typed system with intersection, union, negation and recursive types. The authors inherit the usual problem of having a domain space D that contains all the terms and, at the same time, all the functions from D to D. They prevent this by having an auxiliary domain space which is the disjoint union of D 2 and P(D 2 ). The authors interpret types as sets in a well-suited model where the setinspired type constructs are interpreted as the corresponding to set-theoretical constructs. Moreover, the model manages higher-order functions in an elegant way. The subtyping relation is defined as a relation on the set-theoretical interpretationof the types. For instance, the problem σ ∩ τ σ will be interpreted as σ ∩ τ ⊆ σ , where ∩ becomes the set intersection operator, and the decision program actually decides whether ( σ ∩ τ ) ∩ σ is the empty set.

Bono et al. [START_REF] Bono | A typed lambda calculus with intersection types[END_REF] introduced a relevant and strict parallel term constructor to build inhabitants of intersections and a simple call-by-value parallel reduction strategy. An infinite number of constants c σ⇒τ is applied to typed variables x σ such that c σ⇒τ x σ is upcasted to type τ . It also uses a local renaming typing rule, which changes type decoration in λ-abstractions, as well as coercions. Term synchronicity in the tuples is guaranteed by the typing rules. The calculus uses van Bakel's strict version [START_REF] Steffen Van Bakel | Cut-elimination in the strict intersection type assignment system is strongly normalizing[END_REF] of the T CD intersection type theory.

λ-calculi with intersection and union types

Union types were introduced as a dual of intersection by MacQueen, Plotkin, and Sethi [START_REF] Macqueen | An ideal model for recursive polymorphic types[END_REF]: Barbanera, Dezani, and de'Liguoro [7] is a definitive reference (see Figure 3.1); Frisch, Castagna, and Benzaken [START_REF] Frisch | Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types[END_REF] designed a type system with intersection, union, negation, and recursive types whose semantics fits the intuitive behaviour of the corresponding set-theoretical constructs.

A classical example of the expressiveness of union types, due to Pierce [START_REF] Pierce | Programming with intersection types, union types, and bounded polymorphism[END_REF], is shown in Figure 1.1. Without union types, the best information we can get for (Is_0 Test) in this example is a boolean type.

Algorithm for subtyping intersection and union types

Intersection and union types have an intuitive notion of subtyping. For instance, a term M of type σ ∩ τ has also type σ and type τ , therefore σ ∩ τ σ and σ ∩ τ τ . Hindley was the first to give a subtyping algorithm for intersection types [START_REF] Hindley | The simple semantics for Coppo-Dezani-Sallé types[END_REF]. There is a rich literature reducing the subtyping problem in presence of intersection and union to a set constraint problem: good references are [START_REF] Damm | Subtyping with union types, intersection types and recursive types[END_REF]1,[START_REF] Dunfield | Tridirectional typechecking[END_REF][START_REF] Frisch | Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types[END_REF]. For instance, Aiken and Wimmers [2] designed an algorithm whose input is a list of set constraints with unification variables, usual arrow types, intersection, complementation, and constructor types. Their algorithm first rewrites types in disjunctive normal form, then simplifies the constraints until it shows the system has no solution, or until it can safely unify the variables. Rewriting in disjunctive normal form makes this algorithm exponential in time and space in the worst case.

Logical interpretation of intersection and union types

Mints [START_REF] Mints | The completeness of provable realizability[END_REF] presented a logical interpretation of strong conjunction using realizers: the logical predicate r A∩B [M ] is true if the pure λ-term M is a realizer (also read as "M is a method to assess A ∩ B") for both the formulae r A [M ] and r B [M ]. Inspired by this, Barbanera and Martini tried to answer the question of realizing other proof-functional connectives, like strong implication, López-Escobar's strong equivalence, or Bruce, Di Cosmo, and Longo provable type isomorphism [START_REF] Bruce | Provable isomorphisms of types[END_REF].

Pfenning work on refinement types [START_REF] Pfenning | Refinement types for logical frameworks[END_REF] pioneered an extension of Edinburgh Logical Framework with subtyping and intersection types. Dezani-Ciancaglini, Ghilezan, and Venneri [START_REF] Dezani-Ciancaglini | The "relevance" of intersection and union types[END_REF] investigated a Curry-Howard interpretation of intersection and union types (for Combinatory Logic): using the well-understood relation between combinatory logic and λ-calculus, they encode type-free λ-terms into suitable combinatory logic formulae and then type them using intersection and union types.

Strong connectives arise naturally in investigating the propositions-as-types analogy for intersection and union type assignment systems. Proof-functional (or strong) logical connectives, introduced by Pottinger [START_REF] Pottinger | A type assignment for the strongly normalizable λ-terms[END_REF], take into account the shape of logical proofs, thus allowing for polymorphic features of proofs to be made explicit in formulae. This differs from classical or intuitionistic connectives where the meaning of a compound formula is only dependent on the truth value or the provability of its subformulae.

Pottinger was the first to consider the intersection ∩ as a proof-functional connective. He contrasted it to the intuitionistic connective ∧ as follows: "The intuitive meaning of ∩ can be explained by saying that to assert A ∩ B is to assert that one has a reason for asserting A which is also a reason for asserting B, while to assert A ∧ B is to assert that one has a pair of reasons, the first of which is a reason for asserting A and the second of which is a reason for asserting B".

A simple example of a logical theorem involving intuitionistic conjunction which does not hold for proof-functional conjunction is (A ⊃ A) ∧ (A ⊃ B ⊃ A). Otherwise there would exist a term which behaves both as I and as K.

It is not immediate to extend the judgments-as-types Curry-Howard paradigm to logics supporting proof-functional connectives. These connectives need to compare the shapes of derivations and do not just take into account their provability, i.e. the inhabitation of the corresponding type. There are many other proposals to find a suitable logic to fit intersection types; among them we cite [START_REF] Venneri | Intersection types as logical formulae[END_REF][START_REF] Ronchi | Intersection logic[END_REF][START_REF] Miquel | The implicit calculus of constructions[END_REF][START_REF] Capitani | Hyperformulae, Parallel Deductions and Intersection Types[END_REF][START_REF] Bono | A typed lambda calculus with intersection types[END_REF][START_REF] Pimentel | Intersection types from a proof-theoretic perspective[END_REF], and previous papers by the author [START_REF] Daniel | A realizability interpretation for intersection and union types[END_REF][START_REF] Liquori | A decidable subtyping logic for intersection and union types[END_REF][START_REF] Stolze | Towards a logical framework with intersection and union types[END_REF]. This is still an open question that I am currently investigating.

Chapter 2

A typed calculus with intersection types

In this chapter, we define and prove the main properties of the generic ∆-calculus, a generic intersection typed system for an explicitly typed λ-calculus à la Church enriched with strong pairs, projections, and type coercions.

This chapter is organized as follows: in Section 2.1, we present the system. We also give then instances of the generic ∆-calculus in a diagram called the ∆-chair. In Section 2.2, we show a number of typable examples in the systems presented in the ∆-chair: each example is provided with a corresponding type assignment derivation of its essence. The aims of this section is both to make the reader comfortable with the different intersection typed systems, and to give a first intuition of the correspondence between Church-style and Curry-style calculi. In Section 2.3, we prove the metatheory for all the systems in the ∆-chair: Church-Rosser, unicity of type, subject reduction, strong normalization, decidability of type checking and type reconstruction. In Section 2.4, we study the relations between intersection type assignment systems à la Curry and the corresponding intersection typed systems à la Church. We also show how to get rid of type coercions ∆ τ defining a translation function, denoted by _ , inspired by the one of Tannen et al. [START_REF] Tannen | Inheritance as implicit coercion[END_REF].

The most original feature of the generic ∆-calculus is the concept of strong pair. A strong pair ∆ 1 , ∆ 2 is a special kind of cartesian product such that the two parts of a pair satisfies a given relation R on their essence, that is ∆ 1 R ∆ 2 . The essence ∆ of a ∆-term is a pure λ-term obtained by erasing type decorations, projections and choosing one of the two elements inside a strong pair. As examples,

λx:σ ∩ τ.pr 2 x, λx:σ ∩ τ.pr 1 x = λx.x λx:(σ → τ ) ∩ σ.(pr 1 x)(pr 2 x) = λx.x x λx:σ ∩ (τ ∩ ρ). pr 1 x, pr 2 pr 1 x , pr 2 pr 2 x = λx.x
and so on. Therefore, the essence of a ∆-term is its untyped skeleton: a strong pair ∆ 1 , ∆ 2 can be typechecked if and only if ∆ 1 R ∆ 2 is verified, otherwise the strong pair will be ill-typed. The essence also gives the exact mapping between a term and its typing à la Church and its corresponding term and type assignment à la Curry. The generic ∆-calculus is parametered with the essence relation R, along with a type theory T (see Definition 2.1). Changing the parameters T and R results in defining a totally different intersection typed system. For the purpose of this chapter, we study the four well-known intersection type theories T , namely Coppo-Dezani T CD [START_REF] Coppo | An extension of the basic functionality theory for the λ-calculus[END_REF], Coppo-Dezani-Sallé T CDS [START_REF] Coppo | Functional characterization of some semantic equalities inside λ-calculus[END_REF], Coppo-Dezani-Venneri T CDV [START_REF] Coppo | Functional characters of solvable terms[END_REF]

(refl) σ σ (incl) σ ∩ τ σ, σ ∩ τ τ (glb) ρ σ, ρ τ ⇒ ρ σ ∩ τ (trans) σ τ, τ ρ ⇒ σ ρ
Axiom schemes

(U top ) σ U (U → ) U σ → U (→∩) (σ → τ ) ∩ (σ → ρ) σ → (τ ∩ ρ)
Rule scheme

(→) σ 2 σ 1 , τ 1 τ 2 ⇒ σ 1 → τ 1 σ 2 → τ 2
x:σ ∈ Γ Γ T ∩ x : σ (top) Γ T ∩ M : σ σ T τ Γ T ∩ M : τ ( T )
Figure 2.2: Generic intersection type assignment system λ T ∩ (from Figure 13.8 of [START_REF] Barendregt | Lambda calculus with types[END_REF])

T BCD [11]. We will inspect the above type theories using three equivalence relations R on pure λ-terms, namely syntactical equality ≡, β-equality = β and βη-equality = βη . The combination of the above T and R allows to define ten meaningful instances of the generic ∆-calculus that can be displayed in the ∆-chair (see Definition 2.9).

Syntax, Reduction and Types

Definition 2.1 (Type atoms, type syntax, type theories and type assignment systems). We briefly review some basic definition from Subsection 13.1 of [START_REF] Barendregt | Lambda calculus with types[END_REF], in order to define type assignment systems. The set of atoms, intersection types, intersection type theories and intersection type assignment systems are defined as follows:

1. (Atoms). Let A denote a set of symbols which we will call type atoms, and let U be a special type atom denoting the universal type. In particular, we will use

A ∞ = {a i | i ∈ N} with a i being different from U and A U ∞ = A ∞ ∪ {U}; 2. (Syntax).
The syntax of intersection types, parametrized by A, is: ∩ ). We define in Figure 2.2 an infinite collection of type assignment systems 1 parametrized by a set of atoms A and a type theory T . We name four particular type assignment systems in the table below, which is an excerpt from Figure 13.4 of [START_REF] Barendregt | Lambda calculus with types[END_REF]. Γ T ∩ M : σ denotes a derivable type assignment judgment in the type assignment system λ T ∩ . Type checking is not decidable for λ CD ∩ , λ CDV ∩ , λ CDS ∩ , and λ BCD ∩ (see Theorem 2.24).

σ ::= A | σ → σ | σ ∩ σ; λ T ∩ T A min plus ref. λ CD ∩ T CD A ∞ - [27] λ CDS ∩ T CDS A U ∞ (U top ) [28] λ CDV ∩ T CDV A ∞ (→), (→∩) [29] λ BCD ∩ T BCD A U ∞ (→), (

The ∆-calculi

Intersection type assignment systems and ∆-calculi have in common their type syntax and intersection type theories. The syntax of the generic ∆-calculus is defined as follows:

Definition 2.2 (Generic ∆-calculus syntax).

∆ ::= u M | x | λx:σ.∆ | ∆ ∆ | ∆, ∆ | pr i ∆ | ∆ σ i ∈ {1, 2}
Intuitively, u M denotes an infinite set of constants, indexed with a particular pure λ-term. ∆ τ denotes an explicit coercion 2 of a term ∆ to type τ , where the typing rules will ensure that ∆ has a type σ such that σ T τ . The expression ∆, ∆ denotes a pair that, following the López-Escobar jargon [START_REF] Edgar | Proof functional connectives[END_REF], we call strong pair with respective projections pr 1 and pr 2 . The essence function _ is an erasing function mapping typed ∆-terms into pure λ-terms. It is defined as follows:

Definition 2.3 (Essence function).

x def = x ∆ σ def = ∆ u M def = M λx:σ.∆ def = λx. ∆ ∆ 1 ∆ 2 def = ∆ 1 ∆ 2 ∆ 1 , ∆ 2 def = ∆ 1 pr i ∆ def = ∆ i ∈ {1, 2} 1
Although rules (∩E i ) are derivable with min , we add them for clarity. 2 If type coercions are implicit, then we lose the uniqueness of type property.

One could argue that the choice of ∆ 1 , ∆ 2 def = ∆ 1 is arbitrary and could have been replaced with ∆ 1 , ∆ 2 def = ∆ 2 . However, the typing rules will ensure that, if ∆ 1 , ∆ 2 is typable, then, for some suitable equivalence relation R, we have that ∆ 1 R ∆ 2 . Thus, strong pairs can be viewed as constrained cartesian products. The reduction semantics reduces terms of the generic ∆-calculus as follows: Definition 2.4 (Generic reduction semantics). Let syntactical equality by denoted by ≡.

1. (Substitution) Substitution on ∆-terms is defined as usual, with the additional rules:

u M [∆/x] def = u (M [ ∆ /x]) ∆ σ 1 [∆ 2 /x] def = (∆ 1 [∆ 2 /x]) σ
2. (One-step reduction). We define three notions of reduction:

(λx:σ.∆ 1 ) ∆ 2 → ∆ 1 [∆ 2 /x] (β) pr i ∆ 1 , ∆ 2 → ∆ i i ∈ {1, 2} (pr i ) λx:σ.∆ x → ∆ x ∈ Fv(∆) (η)
Observe that (λx:σ.∆ 1 ) σ ∆ 2 is not a redex, because the λ-abstraction is coerced. The contextual closure is defined as usual except for reductions inside the index of u M that are forbidden (even though substitutions are propagated). We write -→ βpr i for the contextual closure of the (β) and (pr i ) notions of reduction, -→ η for the contextual closure of (η). We also define a synchronous contextual closure, which is like the usual contextual closure except for the strong pairs, as defined in point (3). Synchronous contextual closure of the notions of reduction generates the reduction relations -→ βpr i and -→ η .

3. (Synchronous closure of -→ ). Synchronous closure is defined on the strong pairs with the following constraint:

∆ 1 -→ ∆ 1 ∆ 2 -→ ∆ 2 ∆ 1 ≡ ∆ 2 ∆ 1 , ∆ 2 -→ ∆ 1 , ∆ 2 (Clos )
Note that we reduce in the two components of the strong pair. A longer and more detailed definition of synchronous reduction is given in Subsection 2.1.2;

(Multistep reduction).

We write -→ -→ βpr i (resp. -→ -→ βpr i ) as the reflexive and transitive closure of -→ βpr i (resp. -→ βpr i );

(Congruence).

We write = βpr i as the symmetric, reflexive, transitive closure of -→ -→ βpr i .

We mostly consider βpr i -reductions, thus to ease the notation, we will often omit the subscript in βpr i -reductions.

The next definition introduces a notion of synchronization inside strong pairs. Definition 2.5 (Synchronization). A ∆-term is synchronous if and only if, for all its subterms of the shape ∆ 1 , ∆ 2 , we have that

∆ 1 ≡ ∆ 2 . Γ T R ∆ : σ σ T τ Γ T R ∆ τ : τ ( T ) Γ, x:σ T R ∆ : τ Γ T R λx:σ.∆ : σ → τ (→I) Γ T R ∆ 1 : σ → τ Γ T R ∆ 2 : σ Γ T R ∆ 1 ∆ 2 : τ (→E) x:σ ∈ Γ Γ T R x : σ (ax) Γ T R ∆ 1 : σ Γ T R ∆ 2 : τ ∆ 1 R ∆ 2 Γ T R ∆ 1 , ∆ 2 : σ ∩ τ (∩I) U ∈ A Γ T R u M : U (top) Γ T R ∆ : σ ∩ τ Γ T R pr 2 ∆ : τ (∩E 2 ) Γ T R ∆ : σ ∩ τ Γ T R pr 1 ∆ : σ (∩E 1 ) Figure 2.4: Generic ∆-calculus ∆ T R
It is easy to verify that -→ preserves synchronization, while it is not the case for -→. The next definition introduces an intersection typed system for the generic ∆-calculus that is parametrizable by R, a suitable equivalence relation on pure λ-terms, and T , a type theory, as follows:

Definition 2.6 (Generic ∆-calculus ∆ T R
). The generic ∆-calculus is defined in Figure 2.4. We denote by ∆ T R a particular typed system with the type theory T and under an equivalence relation R and by Γ T R ∆ : σ a corresponding typing judgment.

The typing rules are intuitive for a calculus à la Church except rules (∩I), (top) and ( T ).

The typing rule for a strong pair (∩I) is similar to the typing rule for a cartesian product, except for the side-condition ∆ 1 R ∆ 2 , forcing the two parts of the strong pair to have essences equivalent under R, thus making a strong pair a special case of a cartesian pair. For instance, λx:σ.λy:τ.x, λx:σ.x is not typable in ∆ T ≡ ; meanwhile (λx:σ.x) y, y is not typable in ∆ T ≡ but it is in ∆ T = β ; and x, λy:σ.(λz:τ.z) x y is not typable in ∆ T ≡ nor ∆ T = β but it is in ∆ T = βη . In the typing rule (top), the subscript M in u M is an arbitrary pure λ-term. The typing rule ( T ) allows to change the type of a ∆-term from σ to τ if σ T τ : the term in the conclusion must record this change with an explicit type coercion _ τ , producing the new term ∆ τ : explicit type coercions are important to keep the unicity of typing derivations.

The next definition introduces the generic intersection typed system.

Definition 2.7 (Generic intersection typed system λ@ T R ). For historical reasons (see [START_REF] Liquori | Towards an intersection typed system à la Church[END_REF][START_REF] Liquori | Intersection typed system à la Church[END_REF][START_REF] Daniel | Logic and computation in a lambda calculus with intersection and union types[END_REF]), we used judgments where ∆-terms were decorated by their essence. We thus get judgments of the form Γ T R M @∆ : σ for a system called λ@ T R . The derivation rules are given in Figure 2.5. The properties of λ@ T R are the same than those of ∆ T R , because the decorations do nothing but make the terms easier to understand for newcomers.

The next definition introduces a partial order over equivalence relations on pure λterms and an inclusion over typed systems as follows:

Γ T R M @∆ : σ σ T τ Γ T R M @∆ τ : τ ( T ) Γ, x:σ T R M @∆ : τ Γ T R λx.M @λx:σ.∆ : σ → τ (→I) Γ T R M @∆ 1 : σ → τ Γ T R N @∆ 2 : σ Γ T R M N @∆ 1 ∆ 2 : τ (→E) x:σ ∈ Γ Γ T R x@x : σ (ax) Γ T R M @∆ 1 : σ Γ T R N @∆ 2 : τ M R N Γ T R M @ ∆ 1 , ∆ 2 : σ ∩ τ (∩I) U ∈ A Γ T R M @u M : U (top) Γ T R M @∆ : σ ∩ τ Γ T R M @pr 2 ∆ : τ (∩E 2 ) Γ T R M @∆ : σ ∩ τ Γ T R M @pr 1 ∆ : σ (∩E 1 )
Figure 2.5: Generic intersection typed system λ@ T R Definition 2.8 (R and ).

1. Let R ∈ {≡, = β , = βη }. R 1 R 2 if, for all pure λ-terms M, N such that M R 1 N , we have that M R 2 N ; 2. ∆ T 1 R 1 ∆ T 2 R 2 if, for any Γ, ∆, σ such that Γ T 1 R 1 ∆ : σ, we have that Γ T 2 R 2 ∆ : σ.
Note that correspond to the standard inclusion between relation.

Proposition 2.1.

1. ∆ CD R ∆ CDS R ∆ BCD R and ∆ CD R ∆ CDV R ∆ BCD R ; 2. ∆ T 1 R 1 ∆ T 2 R 2 if T 1 T 2 and R 1 R 2 .

The ∆-chair

The next definition classifies ten instances of the generic ∆-calculus.

Definition 2.9 (∆-chair). Ten typed systems ∆ T R can be draw in a diagram called ∆chair, as in Figure 2.6, where the arrows represent an inclusion relation. ∆ CD ≡ corresponds roughly to [START_REF] Liquori | Towards an intersection typed system à la Church[END_REF][START_REF] Liquori | Intersection typed system à la Church[END_REF] (in the expression M @∆, M is the essence of ∆) and in its intersection part to [START_REF] Stolze | Towards a logical framework with intersection and union types[END_REF]; ∆ CDS ≡ corresponds roughly in its intersection part to [START_REF] Daniel | Logic and computation in a lambda calculus with intersection and union types[END_REF], ∆ BCD ≡ corresponds in its intersection part to [START_REF] Liquori | A decidable subtyping logic for intersection and union types[END_REF], ∆ CD = βη corresponds in its intersection part to [START_REF] Daniel | A realizability interpretation for intersection and union types[END_REF]. The other typed systems are basically new. The main properties of these systems are:

1. All the ∆ T ≡ systems enjoys the synchronous subject reduction property, the other systems also enjoy ordinary subject reduction (Theorem 2.11); 2. All the systems strongly normalize (Theorem 2.21); 3. All the systems correspond to the to original type assignment systems except ∆ CD = β , ∆ CDV = β , ∆ CDV = βη and ∆ BCD = βη (Theorem 2.22); 4. Type checking and type reconstruction are decidable for all the systems, except ∆ CDS = β , ∆ BCD = β , and ∆ BCD = βη (Theorem 2.24).

∆ CD ≡ ∆ CD = β ∆ CDV ≡ ∆ CDV = β ∆ CDS ≡ ∆ CDS = β ∆ BCD ≡ ∆ BCD = β ∆ CDV = βη ∆ BCD = βη

Examples

This section shows examples of typed derivations ∆ T R and highlights the corresponding type assignment judgment in λ T ∩ they correspond to, in the sense that we have a derivation Γ T R ∆ : σ and another derivation Γ T ∩ ∆ : σ. The correspondence between intersection typed systems ∆ T R and intersection type assignment λ T ∩ will be defined in Subsection 2.4.1.

Example 2.1 (Polymorphic identity). In all of the intersection type assignment systems λ T

∩ we can derive:

T ∩ λx.x : (σ → σ) ∩ (τ → τ ) A corresponding ∆-term is: λx:σ.x, λx:τ.x
It can be typed in all of the typed systems of the ∆-chair as follows:

x:σ T R x : σ T R λx:σ.x : σ → σ x:τ T R x : τ T R λx:τ.x : τ → τ λx.x R λx.x T R λx:σ.x, λx:τ.x : (σ → σ) ∩ (τ → τ ) Example 2.

(Auto application)

. In all of the intersection type assignment systems we can derive:

T ∩ λx.x x : ((σ → τ ) ∩ σ) → τ A corresponding ∆-term is: λx:(σ → τ ) ∩ σ.(pr 1 x)(pr 2 x)
It can be typed in all of the typed systems of the ∆-chair as follows:

x:(σ → τ ) ∩ σ T R x : (σ → τ ) ∩ σ x:(σ → τ ) ∩ σ T R pr 1 x : σ → τ x:(σ → τ ) ∩ σ T R x : (σ → τ ) ∩ σ x:(σ → τ ) ∩ σ T R pr 2 x : σ x:(σ → τ ) ∩ σ T R (pr 1 x)(pr 2 x) : τ T R λx:(σ → τ ) ∩ σ.(pr 1 x)(pr 2 x) : (σ → τ ) ∩ σ → τ CHAPTER 2.
z:σ, x:σ, y:U T CDS R x : σ z:σ, x:σ T CDS R λy:U.x : U → σ z:σ T CDS R λx:σ.λy:U.x : σ → U → σ z:σ T CDS R z : σ z:σ T CDS R (λx:σ.λy:U.x) z : U → σ z:σ T CDS R z : σ σ T CDS U z:σ T CDS R z U : U z:σ T CDS

R

(λx:σ.λy:U.x) z z U : σ

As another example, we can also derive:

T CDS ∩ λx.x : σ → σ ∩ U A corresponding ∆-term is: λx:σ. x, x U
It can be typed in ∆ CDS R as follows:

x:σ

T CDS R x : σ x:σ T CDS R x : σ σ T CDS U x:σ T CDS R x U : U x R x x:σ T CDS R x, x U : σ ∩ U T CDS R λx:σ. x, x U : σ → σ ∩ U Example 2.4 (An example in ∆ CDV R
). In λ CDV

∩

we can prove the commutativity of intersection:

T CDV ∩ λx.x : σ ∩ τ → τ ∩ σ A corresponding ∆-term is: λx:σ ∩ τ.pr 2 x, λx:σ ∩ τ.pr 1 x (σ∩τ )→(τ ∩σ)
It can be typed in ∆ CDV R as follows:

x:σ ∩ τ T CDS R x : σ ∩ τ x:σ ∩ τ T CDS R pr 2 x : τ T CDS R λx:σ ∩ τ.pr 2 x : (σ ∩ τ ) → τ x:σ ∩ τ T CDS R x : σ ∩ τ x:σ ∩ τ T CDS R pr 1 x : σ T CDS R λx:σ ∩ τ.pr 1 x : (σ ∩ τ ) → σ λx.x R λx.x T CDS R λx:σ ∩ τ.pr 2 x, λx:σ ∩ τ.pr 1 x : ((σ ∩ τ ) → τ ) ∩ ((σ ∩ τ ) → σ) * T CDS R λx:σ ∩ τ.pr 2 x, λx:σ ∩ τ.pr 1 x (σ∩τ )→(τ ∩σ) : (σ ∩ τ ) → (τ ∩ σ)
where * is

((σ ∩ τ ) → τ ) ∩ ((σ ∩ τ ) → σ) T CDV (σ ∩ τ ) → (τ ∩ σ).

EXAMPLES

Example 2.5 (Another polymorphic identity in ∆ T = β ). In all the ∆ T = β you can type this ∆-term: λx:σ.x, (λx:τ →τ.x) (λx:τ.x)

The typing derivation is the following:

x:σ T = β x : σ T = β λx:σ.x : σ → σ x:τ → τ T = β x : τ → τ T = β λx:τ →τ.x : (τ → τ ) → (τ → τ )
x:τ T = β x : τ

∩

we can can type any term, including the following non-terminating term:

Ω def = (λx.x x) (λx.x x)
More precisely, we have:

T BCD ∩ Ω : U A corresponding ∆-term whose essence is Ω is: (λx:U.x U→U x) (λx:U.x U→U x) U It can be typed in ∆ BCD R as follows: * T BCD R λx:U.x U→U x : U → U * T BCD R λx:U.x U→U x : U → U U → U T BCD U T BCD R (λx:U.x U→U x) U : U T BCD R (λx:U.x U→U x) (λx:U.x U→U x) U : U where * is: x:U T BCD R x : U U T BCD U → U x:U T BCD R x U→U : U → U x:U T BCD R x : U x:U T BCD R x U→U x : U In λ BCD ∩
we can type the following:

x:U → U T BCD ∩ x : (U → U) ∩ (σ → U)
A corresponding ∆-term (whose essence is x) is:

x, λy:σ.x y U

It can be typed in ∆ BCD = βη as follows:

x:U → U T BCD = βη x : U → U x:U → U, y:σ T BCD = βη x : U → U x:U → U, y:σ T BCD = βη y : σ σ U x:U → U, y:σ T BCD = βη y U : U x:U → U, y:σ T BCD = βη x y U : U x:U → U T BCD = βη λy:σ.x y U : σ → U x = βη λy.x y x:U → U T BCD = βη
x, λy:σ.x y U : (U → U) ∩ (σ → U)

Note that the = βη condition has an interesting loophole, as it is well-known that λ BCD

∩

does not enjoy = η -conversion property. Theorem 2.17 (1) will show that we can construct a ∆-term which does not correspond to any λ BCD ∩ derivation.

Example 2.7 (Pottinger [START_REF] Pottinger | A type assignment for the strongly normalizable λ-terms[END_REF]). The following examples can be typed in all the type theories of the ∆-chair (we also display in square brackets the corresponding pure λ-terms typable in λ T ∩ ). These are encodings from the examples à la Curry given by Pottinger in [START_REF] Pottinger | A type assignment for the strongly normalizable λ-terms[END_REF].

[λx.λy.x y] T R λx:(σ → τ ) ∩ (σ → ρ).λy:σ. (pr 1 x) y), (pr 2 x) y :

(σ → τ ) ∩ (σ → ρ) → σ → τ ∩ ρ [λx.λy.x y] T R λx:σ → τ ∩ ρ. λy:σ.pr 1 (x y), λy:σ.pr 2 (x y) : (σ → τ ∩ ρ) → (σ → τ ) ∩ (σ → ρ) [λx.λy.x y] T R λx:σ → ρ.λy:σ ∩ τ.x (pr 1 y) : (σ → ρ) → σ ∩ τ → ρ [λx.λy.x] T R λx:σ ∩ τ.λy:σ.pr 2 x : σ ∩ τ → σ → τ [λx.λy.x y y] T R λx:σ → τ → ρ.λy:σ ∩ τ.x (pr 1 y) (pr 2 y) : (σ → τ → ρ) → σ ∩ τ → ρ [λx.x] T R λx:σ ∩ τ.pr 1 x : σ ∩ τ → σ [λx.x] T R λx:σ. x, x : σ → σ ∩ σ [λx.x] T R λx:σ ∩ (τ ∩ ρ). pr 1 x, pr 1 pr 2 x , pr 2 pr 2 x : σ ∩ (τ ∩ ρ) → (σ ∩ τ ) ∩ ρ
In the same paper, Pottinger lists some types that cannot be inhabited by any intersection type assignment ( T ∩ ) in an empty context, namely:

σ → (σ ∩ τ ) and (σ → τ ) → (σ → ρ) → σ → τ ∩ ρ and ((σ ∩ τ ) → ρ) → σ → τ → ρ.
It is not difficult to verify that the above types cannot be inhabited by any of the type systems of the ∆-chair because of the failure of the essence condition in the strong pair type rule.

Example 2.8 (Intersection is not the conjunction operator [START_REF] Hindley | Coppo-Dezani types do not correspond to propositional logic[END_REF][START_REF] Ben-Yelles | Type assignment in the lambda-calculus: syntax and semantics[END_REF]). This counterexample is from the corresponding counter-example à la Curry given by Hindley [START_REF] Hindley | Coppo-Dezani types do not correspond to propositional logic[END_REF] and Ben-Yelles [START_REF] Ben-Yelles | Type assignment in the lambda-calculus: syntax and semantics[END_REF]. The intersection type

(σ → σ) ∩ ((σ → τ → ρ) → (σ → τ ) → σ → ρ)
where the left part of the intersection corresponds to the type for the combinator I and the right part for the combinator S cannot be assigned to a pure λ-term. Analogously, the same intersection type cannot be assigned to any ∆-term belonging to a type system from the ∆-chair, because of the failure of the essence condition.

On synchronization and subject reduction

For the typed systems ∆ T ≡ , strong pairs have an intrinsic notion of synchronization: some redexes need to be reduced in a synchronous fashion unless we want to create meaningless ∆-terms that cannot be typed. Consider the ∆-term (λx:σ.x) y, (λx:σ.x) y . If we use the -→ reduction relation, then the following reduction paths are legal:

(λx:σ.x) y, (λx:σ.x) y β (λx:σ.x) y, y β β y, (λx:σ.x) y β y, y More precisely, the first and second redexes are rewritten asynchronously, therefore they cannot be typed in any typed system ∆ T ≡ , because we fail to check that the left and the right part of the strong pair are syntactically the same: the -→ reduction relation prevents this loophole and allows to type all redexes. In summary, -→ can be thought of as the natural reduction relation for the typed systems ∆ T ≡ .

2.3 Metatheory of ∆ T R

General properties

Unless specified, all properties applies to the intersection typed systems ∆ T R . The Church-Rosser property is proved using the technique of Takahashi [START_REF] Takahashi | Parallel reductions in λ-calculus[END_REF]. The parallel reduction semantics extends Definition 2.4 and it is inductively defined as follows: Definition 2.10 (Parallel reduction semantics).

x =⇒ x u M =⇒ u M ∆ σ =⇒ (∆ ) σ if ∆ =⇒ ∆ ∆ 1 ∆ 2 =⇒ ∆ 1 ∆ 2 if ∆ 1 =⇒ ∆ 1 and ∆ 2 =⇒ ∆ 2 λx:σ.∆ =⇒ λx:σ.∆ if ∆ =⇒ ∆ (λx:σ.∆ 1 ) ∆ 2 =⇒ ∆ 1 [∆ 2 /x] if ∆ 1 =⇒ ∆ 1 and ∆ 2 =⇒ ∆ 2 ∆ 1 , ∆ 2 =⇒ ∆ 1 , ∆ 2 if ∆ 1 =⇒ ∆ 1 and ∆ 2 =⇒ ∆ 2 pr i ∆ =⇒ pr i ∆ if ∆ =⇒ ∆ and i ∈ {1, 2} pr i ∆ 1 , ∆ 2 =⇒ ∆ i if ∆ i =⇒ ∆ i and i ∈ {1, 2}
Intuitively, ∆ =⇒ ∆ means that ∆ is obtained from ∆ by simultaneous arbitrary contractions of some βpr i -redexes possibly overlapping each other. Church-Rosser can be achieved by proving a stronger statement, namely:

∆ =⇒ ∆ implies ∆ =⇒ ∆ *
where ∆ * is a ∆-term determined by ∆ and independent from ∆ . The statement (2.3.1) is satisfied by the term ∆ * which is obtained from ∆ by contracting all the redexes existing in ∆ simultaneously, as is shown in the following definition.

Definition 2.11 (The map _ * ).

x

* def = x u * M def = u M (∆ σ ) * def = (∆ * ) σ ∆ 1 , ∆ 2 * def = ∆ * 1 , ∆ * 2 (λx:σ.∆) * def = λx:σ.∆ * (∆ 1 ∆ 2 ) * def = ∆ * 1 ∆ * 2 if ∆ 1 ∆ 2 is not a β-redex ((λx:σ.∆ 1 ) ∆ 2 ) * def = ∆ * 1 [∆ * 2 /x] (pr i ∆) * def = pr i ∆ * if ∆ is not a strong pair (pr i ∆ 1 , ∆ 2 ) * def = ∆ * i i ∈ {1, 2}
The next technical lemma will be useful in showing that Church-Rosser for -→ -→ can be inherited from Church-Rosser for =⇒.

Lemma 2.2.

1. If ∆ 1 -→ ∆ 1 , then ∆ 1 =⇒ ∆ 1 ; 2. if ∆ 1 =⇒ ∆ 1 , then ∆ 1 -→ -→∆ 1 ; 3. if ∆ 1 =⇒ ∆ 1 and ∆ 2 =⇒ ∆ 2 , then ∆ 1 [∆ 2 /x] =⇒ ∆ 1 [∆ 2 /x]; 4. ∆ 1 =⇒ ∆ * 1 .
Proof. We can now prove the Church-Rosser property for the parallel reduction:

Lemma 2.3 (Confluence property for =⇒). If ∆ =⇒ ∆ , then ∆ =⇒ ∆ * .
Proof. By induction on the shape of ∆. Proof. Thanks to the first two points of Lemma 2.2, we know that -→ -→ is the transitive closure of =⇒, therefore we can deduce the confluence property of -→ -→ with the usual diagram chase, as suggested below.

-if ∆ ≡ x, then ∆ ≡ x =⇒ x ≡ ∆ * ; -if ∆ ≡ u M , then ∆ ≡ u M =⇒ u M ≡ ∆ * ; -if ∆ ≡ ∆ σ 1 ,
∆ 0,0 ∆ 0,1 ∆ 0,2 ∆ 1,0 ∆ 1,1 ∆ 1,2 ∆ 2,0 ∆ 2,1 ∆ 2,2 ∆ 3,0 ∆ 3,1 ∆ 3,2
The next lemma says that all type derivations for ∆ have an unique type.

Lemma 2.5 (Unicity of typing). If Γ T R ∆ : σ, then σ is unique. Proof. By induction on the shape of ∆.

The next lemma proves inversion properties on typable ∆-terms.

Lemma 2.6 (Inversion).

1. If Γ T R x : σ, then x:σ ∈ Γ;

2. if Γ T R λx:σ.∆ : ρ, then ρ ≡ σ → τ for some τ and Γ, x:σ T R ∆ : τ ;

3. if Γ T R ∆ 1 ∆ 2 : τ , then there is σ such that Γ T R ∆ 1 : σ → τ and Γ T R ∆ 2 : σ; 4. if Γ T R ∆ 1 , ∆ 2 : ρ, then there is σ, τ such that ρ ≡ σ ∩ τ and Γ T R ∆ 1 : σ and Γ T R ∆ 2 : τ and ∆ 1 R ∆ 2 ; 5. if Γ T R pr 1 ∆ : σ, then there is τ such that Γ T R ∆ : σ ∩ τ ; 6. if Γ T R pr 2 ∆ : τ , then there is σ such that Γ T R ∆ : σ ∩ τ ; 7. if Γ T R u M : σ, then σ ≡ U;
8. if Γ T R ∆ τ : ρ, then ρ ≡ τ and there is σ such that σ T τ and Γ T R ∆ : σ.

Proof. The typing rules are uniquely syntax-directed, therefore we can immediately conclude.

The next lemma says that all subterms of a typable ∆-term are typable too.

Lemma 2.7 (Subterms typability). If Γ T R ∆ : σ, and ∆ is a subterm of ∆, then there exists Γ and τ such that Γ ⊇ Γ and Γ T R ∆ : τ . Proof. By induction on the derivation of Γ T R ∆ : σ. For instance, let's consider the case where the applied rule is (→ I). The other cases are similar. If the last applied rule is (→ I), then ∆ ≡ λx:σ 1 .∆ 1 and σ ≡ σ 1 → σ 2 for some σ 1 , σ 2 , and ∆ 1 . Moreover, ∆ is a subterm of ∆ 1 , and:

Γ, x:σ 1 ∆ 1 : σ 2
By induction hypothesis, we know that there is an extension Γ of Γ, x:σ 1 such that Γ T R ∆ : τ . As Γ is also an extension of Γ, we can conclude.

As expected, the weakening and strengthening properties on contexts are verified.

Lemma 2.8 (Free-variable properties).

1. If Γ T R ∆ : σ, and Γ ⊇ Γ, then Γ T R ∆ : σ; 2. if Γ T R ∆ : σ, then Fv(∆) ⊆ Dom(Γ); 3. if Γ T R ∆ : σ, Γ ⊆ Γ and Fv(∆) ⊆ Dom(Γ ), then Γ T R ∆ : σ.
Proof. By induction on the derivation of Γ T R ∆ : σ.

The next lemma also says that essence is closed under substitution.

Lemma 2.9 (Substitution).

1. ∆ 1 [∆ 2 /x] ≡ ∆ 1 [ ∆ 2 /x]; 2. If Γ, x:σ T R ∆ 1 : τ and Γ T R ∆ 2 : σ, then Γ T R ∆ 1 [∆ 2 /x] : τ . Proof.
1. by induction on the shape of ∆ 1 ; 2. by induction on the derivation. As an illustration, we show the case when the last applied rule is (∩I). In this case, we know that:

Γ, x:σ T R ∆ 1 , ∆ 1 : τ ∩ τ and Γ T R ∆ 2 : σ
By induction hypothesis, we have:

Γ T R ∆ 1 [∆ 2 /x] : τ and Γ T R ∆ 1 [∆ 2 /x] : τ
Moreover, thanks to point (1), we can show that:

∆ 1 [∆ 2 /x] R ∆ 1 [∆ 2 /x]
As a consequence:

Γ T R ∆ 1 [∆ 2 /x] : τ Γ T R ∆ 1 [∆ 2 /x] : τ ∆ 1 [∆ 2 /x] R ∆ 1 [∆ 2 /x] Γ T R ∆ 1 , ∆ 1 [∆ 2 /x] : τ ∩ τ (∩I)
In order to prove subject reduction, we need to prove that reducing ∆-terms preserve the side-condition ∆ 1 R ∆ 2 when typing the strong pair ∆ 1 , ∆ 2 . We prove this in the following lemma.

Lemma 2.10 (Essence reduction).

if Γ

T ≡ ∆ 1 : σ and ∆ 1 -→ ∆ 2 , then ∆ 1 = β ∆ 2 ; 2. for R ∈ {= β , = βη }, if Γ T R ∆ 1 : σ and ∆ 1 -→ ∆ 2 , then ∆ 1 R ∆ 2 ; 3. if Γ T = βη ∆ 1 : σ and ∆ 1 -→ η ∆ 2 , then ∆ 1 = η ∆ 2 . Proof. If ∆ 1 is a redex, then we have three cases: -if ∆ 1 ≡ (λx:σ.∆ 1 ) ∆ 1 and ∆ 2 is ∆ 1 [∆ 1 /x], then, thanks to Lemma 2.9(1) we have that ∆ 2 ≡ ∆ 1 [ ∆ 1 /x], therefore ∆ 1 = β ∆ 2 ; -if ∆ 1 ≡ pr i ∆ 1 , ∆ 2 and ∆ 2 is ∆ i , we know that ∆ 1 is typable in ∆ T R
, and thanks to Lemma 2.6(4), we have that

∆ 1 R ∆ 2 . As a consequence, ∆ 1 R ∆ 2 ; -if ∆ 1 ≡ λx:σ.∆ x with x ∈ Fv(∆ ), and ∆ 2 is ∆ , then ∆ 1 = η ∆ 2 .
For the contextual closure, we have that ∆ 1 ≡ ∆[∆ /x], where ∆ acts as an applicative context and ∆ is a redex, and

∆ 2 is ∆[∆ /x] where ∆ is the contractum of ∆ .
Then, as ∆ is a subterm of ∆ 1 , by Lemma 2.7 we deduce that ∆ is typable, therefore ∆ is also typable, and then we infer, using Lemma 2.9(1), that:

∆ 1 ≡ ∆ [ ∆ /x] and ∆ 2 ≡ ∆ [ ∆ /x]
Then we can conclude.

The next theorem states that all the typed systems ∆ T ≡ preserve synchronous βpr ireduction, and all the typed systems ∆ T = β and ∆ T = βη preserve βpr i -reduction.

Theorem 2.11 (Subject reduction for βpr i ).

1. If Γ T ≡ ∆ 1 : σ and ∆ 1 -→ ∆ 2 , then Γ T ≡ ∆ 2 : σ; 2. for R ∈ {= β , = βη }, if Γ T R ∆ 1 : σ and ∆ 1 -→ ∆ 2 , then Γ T R ∆ 2 : σ.
Proof. We proceed by looking at the cases where ∆ 1 is a redex and ∆ 2 its contractum, then we consider the contextual closure:

-

If ∆ 1 is a β-redex (λx:τ.∆) ∆ , and ∆ 2 ≡ ∆[∆ /x],
then by Lemma 2.6, the derivation tree of ∆ 1 ends with:

Γ, x:τ T R ∆ : τ → σ Γ T R λx:τ.∆ : τ → σ Γ T R ∆ : τ Γ T R (λx:τ.∆) ∆ : σ
We conclude that Γ T R ∆ 2 : σ by using Lemma 2.9(2);

-If ∆ 1 is a pr i -redex pr i ∆, ∆ , and ∆ 2 is ∆ (if i = 1) or ∆ (if i = 2)
, then by Lemma 2.6, the derivation tree of ∆ 1 ends with:

Γ T R ∆ : σ 1 Γ T R ∆ : σ 2 Γ T R ∆, ∆ : σ 1 ∩ σ 2 Γ T R pr i ∆, ∆ : σ i
Then we see immediately that Γ T R ∆ 2 : σ i ;

-For the contextual closure, we proceed by induction on the derivation: we illustrate the most important case, namely (∩I) where we have to check that the essence condition is preserved. According to R we distinguish two cases:

1. (Case where R is ≡). If Γ T ≡ ∆ 1 , ∆ 2 : σ ∩ τ and ∆ 1 , ∆ 2 -→ ∆ 1 , ∆ 2 , then ∆ 1 ≡ ∆ 2 and, by induction hypothesis, Γ T ≡ ∆ 1 : σ and Γ T ≡ ∆ 2 : τ , therefore Γ T ≡ ∆ 1 , ∆ 2 : σ ∩ τ ; 2. (Case where R ∈ {= β , = βη }). If Γ T R ∆ 1 , ∆ 2 : σ ∩ τ and ∆ 1 , ∆ 2 -→ ∆ 1 , ∆ 2 , then: -∆ 1 R ∆ 2 ; -by Lemma 2.10 we have that ∆ 1 R ∆ 1 and ∆ 2 R ∆ 2 ; -by induction hypothesis we have that Γ T R ∆ 1 : σ and Γ T R ∆ 2 : τ ; therefore ∆ 1 R ∆ 2 and Γ T R ∆ 1 , ∆ 2 : σ ∩ τ .
The next theorem states that some of the typed systems on the back of the ∆-chair preserve η-reduction.

Theorem 2.12 (Subject reduction for η for

T CDV , T BCD ). Let T ∈ {T CDS , T BCD }. If Γ T = βη ∆ 1 : σ and ∆ 1 -→ η ∆ 2 , then Γ T = βη ∆ 2 : σ.
Proof. If ∆ 1 is a η-redex, then we proceed as usual using Lemmas 2.6 and 2.8. For the contextual closure the proof proceeds exactly as in Theorem 2.11.

Remark 2.1 (About subject expansion).

We know that some of the intersection type assignment systems à la Curry (viz. λ BCD ∩ and λ CDS ∩ ) satisfy the subject β-expansion property: one may ask whether this property can also be meaningful in typed systems à la Church. It is not surprising to see that the answer is negative because type-decorations of bound variables are hard-coded in the λ-abstraction and cannot be forgotten. As a trivial example of the failure of the subject-expansion in all the typed systems, consider the following reduction:

(λx:σ.x) (λx:σ.x) -→ (λx:σ.x) Obviously we can type T R (λx:σ.x) : σ → σ but T R (λx:σ.x) (λx:σ.x) : σ → σ.

Synchronous reduction

We want to define synchronous β-reduction -→ β such that, whenever

∆ 1 -→ β ∆ 2 , we have ∆ 1 -→ β ∆ 2 .
In order to do that, we extend the generic ∆-calculus and the λ-calculus with an underlining that book-keeps all the reductions that have to be done synchronously. This technique is adapted from the one used in Section 2.3 of [10].

We define the syntax of the λ-calculus and ∆-calculus as follows:

M ::= x | λx.M | (λx.M 1 ) M 2 | M 1 M 2 ∆ ::= x | λx:σ.∆ | (λx:σ.∆ 1 ) ∆ 2 | ∆ 1 ∆ 2 | ∆ 1 , ∆ 2 | pr 1 ∆ | pr 2 ∆ | in σ 1 ∆ | in σ 2 ∆ | u M | ∆ σ
Note that there is no underlining in u M , because there is no reduction inside the index of u M . The essence function for the ∆-calculus is the same as for the ∆-calculus, with the following extra rule:

λx:σ.∆ def = λx. ∆
We define the notion of β-reduction for λ-calculus and ∆-calculus:

(λx.M ) N → β M [N /x] (λx:σ.∆ 1 ) ∆ 2 → β ∆ 1 [∆ 2 /x]
Then the syntactical closure of → β is noted -→ β , and the transitive reflexive closure of

-→ β is noted -→ -→ β . Definition 2.12. If M (resp. ∆) is a λ-term (resp. ∆-term), then |M | (resp. |∆|) is
obtained by leaving out all the underlinings.

We define a partial function Sync(∆, M ) which, given a ∆-term ∆ (without underlinings) and a λ-term M , either fails or return a ∆-term whose underlinings correspond to the underlinings of M .

The most important rule is:

Sync((λx:σ.∆ 1 ) ∆ 2 , (λx.M 1 ) M 2 ) def = (λx:σ.Sync(∆ 1 , M 1 )) Sync(∆ 2 , M 2 )
The other rules are structural:

Sync(∆, M ) def = ∆ if M has no underlining and ∆ ≡ M Sync(∆ 1 ∆ 2 , M 1 M 2 ) def = Sync(∆ 1 , M 1 ) Sync(∆ 2 , M 2 ) if M 1 M 2 is not a β-redex Sync(λx:σ.∆, λx.M ) def = λx:σ.Sync(∆, M ) Sync( ∆ 1 , ∆ 2 , M ) def = Sync(∆ 1 , M ), Sync(∆ 2 , M ) Sync(pr i ∆, M ) def = pr i Sync(∆, M ) Sync(in σ i ∆, M ) def = in σ i Sync(∆, M ) Sync(∆ σ , M ) def = (Sync(∆, M )) σ Sync(∆, M ) def = fail otherwise
We define the reduction mapping ϕ from ∆-terms to ∆-terms, which reduces all underlined redexes. It is an extension of Definition 2.3.11 of [10].

Definition 2.13 (Reduction mapping).

ϕ(x) def = x ϕ(λx:σ.∆) def = λx:σ.ϕ(∆) ϕ((λx:σ.∆ 1 ) ∆ 2 ) def = ϕ(∆ 1 )[ϕ(∆ 2 )/x] ϕ(∆ 1 ∆ 2 ) def = ϕ(∆ 1 ) ϕ(∆ 2 ) if ∆ 1 ∆ 2 is not a β-redex ϕ( ∆ 1 , ∆ 2 ) def = ϕ(∆ 1 ), ϕ(∆ 2 ) ϕ(pr i ∆) def = pr i ϕ(∆) ϕ(in σ i ∆) def = in σ i ϕ(∆) ϕ(u M ) def = u M ϕ(∆ σ ) def = ϕ(∆) σ
We now define synchronous β-reduction, which, as we will prove in Theorem 2.15, keeps a synchronicity with the β-reduction in the essence.

Definition 2.14 (Synchronous β-reduction).

Let ∆ and M with exactly one underlining such that |M | ≡ ∆ and Sync(∆, M ) is defined. We define synchronous β-reduction as:

∆ -→ β ϕ(Sync(∆, M ))
The reflexive and transitive closure of

-→ β is noted -→ -→ β .
The following two lemmas establish the basic properties of synchronizations and βreduction.

Lemma 2.13.

1. Sync(∆, M ) ≡ M ; 2. |Sync(∆, M )| ≡ ∆.
Proof. By induction on ∆.

Lemma 2.14.

1. If M -→ β N , then |M | -→ β |N |; 2. If ∆ 1 -→ β ∆ 2 , then |∆ 1 | -→ β |∆ 2 |; 3. ∆ -→ -→ β ϕ(∆); 4. If ∆ 1 -→ β ∆ 2 , then either ∆ 1 -→ β ∆ 2 , or ∆ 1 ≡ ∆ 2 .
Proof.

2. 3. Easy;

4. By induction on ∆ 1 .

The next theorem shows that synchronous relation behave correctly in typed and untyped reductions.

Theorem 2.15.

If ∆ 1 -→ β ∆ 2 , then:

1. ∆ 1 -→ -→ β ∆ 2 ; 2. ∆ 1 -→ β ∆ 2 .
Proof. We know that there is some λ-term M with only one underlining such that

|M | ≡ ∆ 1 and ϕ(Sync(∆ 1 , M )) ≡ ∆ 2 .
1. We know, by Lemma 2.13 that

∆ 1 ≡ |Sync(∆ 1 , M )|. Moreover, by Lemma 2.14, we know that Sync(∆ 1 , M ) -→ β ϕ(Sync(∆ 1 , M )), therefore ∆ 1 -→ -→ β |ϕ(Sync(∆ 1 , M ))|.
However, the function ϕ returns a ∆-term without underlining, therefore:

|ϕ(Sync(∆ 1 , M ))| ≡ ϕ(Sync(∆ 1 , M ))
As a conclusion, we have that

∆ 1 -→ -→ β ∆ 2 ; 2. We know that Sync(∆ 1 , M )-→ -→ β ∆ 2 , therefore, as Sync(∆ 1 , M ) ≡ M , we have that M -→ -→ β ∆ 2 .
However, M has only one underlining, and ∆ 2 has none, therefore this is the single-step reduction M -→ β ∆ 2 . Moreover, |M | ≡ ∆ 1 , so we conclude, using Lemma 2.14, that

∆ 1 -→ β ∆ 2 .
The following is a technical lemma used to prove confluence.

Lemma 2.16.

For any ∆ and M , if

Sync(∆, M ) is defined, then ∆-→ -→ β ϕ(Sync(∆, M )).
Proof. Reduce the redexes in ∆ in the same order as is done by the function ϕ in Sync(∆, M ).

The above lemma justifies the following definition:

Definition 2.15 (Labelled synchronous reductions).

1. We note We can prove that labeled synchronous reduction is confluent, more precisely, that if

∆ 1 M -→ ∆ 2 if ∆-→ -→ β ϕ(Sync(∆, M )); 2. We note M N if |M | ≡ |N |
∆ 1 M -→ ∆ 2 , and ∆ 1 N -→ ∆ 3 , then if we note ∆ 4 such that ∆ 1 M N -→ ∆ 4 ,
then ∆ 2 and ∆ 3 reduce to ∆ 4 under a labeled synchronous reduction. First, we need a technical lemma.

Lemma 2.17.

If ∆ M 1 -→ ∆ 1 and ∆ M 2 -→ ∆ 2 , with M 1 M 2
, then there exists some N such that

∆ 1 N -→ ∆ 2 .
More precisely, we obtain N by applying in M 2 the β-reductions that appear in M 1 .

Proof. By induction on the shape of ∆, we can see that ∆ 1 N -→ ∆ 2 . The most interesting case is when ∆ is some redex (λx:σ.∆ ) ∆ , and M 2 is an underlined redex (λx.M 2 ) M 2 .

We pose ∆ 2 and ∆ 2 such that ∆

M 2 -→ ∆ 2 and ∆ M 2 -→ ∆ 2 . Moreover, ∆ 2 def = ∆ 2 [∆ 2 /x].
We have to subcases:

1. if M 1 is also an underlined redex (λx.M 1 ) M 1 , then ∆ 1 ≡ ∆ 1 [∆ 1 /x], where ∆ M 1 -→ ∆ 1 and ∆ M 1 -→ ∆ 1 .
By induction hypothesis, we have that there is some N and We now prove the confluence property for label-led synchronous reductions.

N such that ∆ 1 N -→ ∆ 2 and ∆ 1 N -→ ∆ 2 ,

and we pose

N def = N [N /x]; 2. if M 1 is a redex (λx.M 1 ) M 1 , then ∆ 1 ≡ (λx:σ.∆ 1 ) ∆ 2 , where ∆ M 1 -→ ∆ 1 and ∆ M 1 -→ ∆ 1 . By induction hypothesis, we have that there is some N and N such that ∆ 1 N -→ ∆ 2 and ∆ 1 N -→ ∆ 2 ,
Lemma 2.18 (Confluence for labelled synchronous reduction).

If ∆ 1 M 1 -→ ∆ 2 and ∆ 1 M 2 -→ ∆ 3 , then we pose ∆ 4 such that ∆ 1 M 1 M 2 -→ ∆ 4 .
There is some

M 3 and M 4 such that ∆ 2 M 3 -→ ∆ 4 and ∆ 3 M 4 -→ ∆ 4 . ∆ 3 ∆ 4 ∆ 1 ∆ 2 M 1 M 2 M 3 M 4
Proof. By Lemma 2.17.

We can finally prove confluence.

Theorem 2.19 (Confluence for -→ β ). If ∆ 1 -→ -→ β ∆ 2 and ∆ 1 -→ -→ β ∆ 3 , then there is some ∆ 4 , such that ∆ 2 -→ -→ β ∆ 4 and ∆ 3 -→ -→ β ∆ 4 .
Proof.

By Definition 2.14, one-step synchronous reduction corresponds to a labeled synchronous reduction, and by Lemma 2.16, labeled synchronous reduction corresponds to multistep synchronous reduction, therefore we can conclude with the usual diagram chase using Lemma 2.18, as suggested below:

∆ 1 • ∆ 3 • • • • • • ∆ 2 • ∆ 4 M 1 M 2 M 3 M 4 M 5 M 6 M 8 M 10 M 12 M 14 M 16 M 7 M 13 M 9 M 15 M 11 M 17

Strong normalization of the generic ∆-calculus

The idea of the strong normalization proof of the generic ∆-calculus is to embed typable terms of the generic ∆-calculus into Church-style terms of a target system, which is the simply-typed λ-calculus with pairs, in a structure-preserving way (and forgetting all the essence side-conditions). The translation is sufficiently faithful so as to preserve the number of reductions, and so strong normalization for the generic ∆-calculus follows from strong normalization for simply-typed λ-calculus with pairs. A similar technique has been used in [START_REF] Harper | A framework for defining logics[END_REF] to prove the strong normalization property of LF and in [START_REF] Bucciarelli | Intersection types and λdefinability[END_REF] to prove the strong normalization property of a subset of λ CD ∩ . The target system has one atomic type called •, a special constant term u • of type • and an infinite number of constants c σ of type σ for any type of the target system. We denote by Γ × M : σ a typing judgment in the target system. -On intersection types.

|a i | def = • ∀a i ∈ A |σ ∩ τ | def = |σ| × |τ | |σ → τ | def = |σ| → |τ | -On ∆-terms. |x| Γ def = x |u M | Γ def = u • |λx:σ.∆| Γ def = λx.|∆| Γ,x:σ |∆ 1 ∆ 2 | Γ def = |∆ 1 | Γ |∆ 2 | Γ | ∆ 1 , ∆ 2 | Γ def = (|∆ 1 | Γ , |∆ 2 | Γ ) |pr i ∆| Γ def = pr i |∆| Γ |∆ τ | Γ def = c |σ|→|τ | |∆| Γ if Γ T R ∆ : σ -
The map can be easily extended to basis Γ.

The following technical lemma states some properties of the forgetful function.

Lemma 2.20.

1. If Γ T R ∆ : σ, then |∆| Γ is defined, and, for all Γ ⊇ Γ, |∆| Γ ≡ |∆| Γ ; 2. |∆ 1 [∆ 2 /x]| Γ ≡ |∆ 1 | Γ [|∆ 2 | Γ /x]; 3. If ∆ 1 -→ ∆ 2 , then |∆ 1 | Γ -→ |∆ 2 | Γ ; 4. If Γ T R ∆ : σ then |Γ| × |∆| Γ : |σ|. Proof.

by induction on the derivation;

2. by induction on ∆ 1 . The only interesting part is ∆ 1 ≡ λy:σ.∆ 1 : by induction hypothesis, we have:

|∆ 1 [∆ 2 /x]| Γ,x:σ ≡ |∆ 1 | Γ,x:σ [|∆ 2 | Γ,x:σ /x]
Therefore, we see that:

|(λy:σ.∆ 1 )[∆ 2 /x]| Γ ≡ λy:σ.|∆ 1 [∆ 2 /x]| Γ,x:σ ≡ λy:σ.|∆ 1 | Γ,x:σ [|∆ 2 | Γ,x:σ /x]
However, from point (1), we know that:

|∆ 2 | Γ,x:σ ≡ |∆ 2 | Γ
and we conclude; Proof. Using Lemma 2.20 and the strong normalization of the simply typed λ-calculus with cartesian pairs.

Church-style vs. Curry-style λ-calculus

In this section, we will study the intriguing relation between the λ-calculi λ T ∩ and their corresponding ∆-calculi ∆ T R .

Relation between type assignment systems λ T

∩ and typed systems ∆ T R It is interesting to state some relations between type assignment systems à la Church and typed systems à la Curry. An interesting property is the one of isomorphism, namely the fact that whenever we assign a type σ to a pure λ-term M , the same type can be assigned to a ∆-term such that the essence of ∆ is M . Conversely, for every assignment of σ to a ∆-term, a valid type assignment judgment of the same type for the essence of ∆ can be derived.

Soundness, completeness and isomorphism between instances of the generic ∆-calculus and the corresponding intersection type assignment systems for the λ-calculus are defined as follows: Definition 2.17 (Soundness, completeness and isomorphism). Let ∆ T R and λ T ∩ .

(Soundness, ∆

T R λ T ∩ ). Γ T R ∆ : σ implies Γ T ∩ ∆ : σ; 2. (Completeness, ∆ T R λ T ∩ ). Γ T ∩ M : σ implies there exists ∆ such that M ≡ ∆ and Γ T R ∆ : σ; 3. (Isomorphism, ∆ T R ∼ λ T ∩ ). ∆ T R λ T ∩ and ∆ T R λ T ∩ .
The following properties and relations between typed and type assignment systems can be verified.

Theorem 2.22 (Soundness, completeness and isomorphism). The following properties between ∆-calculi and type assignment systems λ T

∩ can be verified.

∆ T R ∆ T R λ T ∩ ∆ T R λ T ∩ ∆ CD ≡ √ √ ∆ CDV ≡ √ √ ∆ CDS ≡ √ √ ∆ BCD ≡ √ √ ∆ CD = β × √ ∆ CDV = β × √ ∆ CDS = β √ √ ∆ BCD = β √ √ ∆ CDV = βη × √ ∆ BCD = βη × √ Proof.
( ) (a) Soundness for ∆ T ≡ . Let ∆ be such that Γ T ≡ ∆ : σ. We proceed by induction on the derivation. All cases proceed straightforwardly since all rules of the type and subtype system T ≡ correspond exactly to the rules of the same name in the corresponding type assignment system T ∩ and in the same type theory T . Therefore M ≡ ∆ can be easily be defined and derived with type σ.

(b) Soundness for ∆ {CDS,BCD} = β
. Let T ∈ {T CDS , T BCD }. We know, thanks to [START_REF] Barendregt | Lambda calculus with types[END_REF] (Figure 14.2), that the following rule is admissible for λ T ∩ :

Γ T ∩ M : σ Γ T ∩ N : τ M = β N Γ T ∩ M : σ ∩ τ (∩I) adm
Then the proof proceeds by induction on the derivation of Γ T = β ∆ : σ. The most important case is when the last used rule is (∩I): by induction we get Γ T ∩ ∆ 1 : σ, and Γ T ∩ ∆ 2 : τ , and ∆ 1 = β ∆ 2 , and, by the essence definition, ∆ 1 , ∆ 2 = β ∆ 1 . Apply rule (∩I) adm and conclude with

Γ T ∩ ∆ 1 : σ ∩ τ . ( ) Loss of soundness for ∆ CD = β and ∆ CDV = β . Let T ∈ {T CD , T CDV }. Let S def = λx.λy.λz.x z (y z) and K def = λx.λy.x. Let ∆ def = (λx:(σ → τ → ρ) → ((σ → τ ) → σ → ρ) → σ → τ → ρ.λy:(σ → τ → ρ) → (σ → τ ) → σ → ρ.λz:σ → τ → ρ.x z (y z))(λx:σ → τ → ρ.λy:(σ → τ ) → σ → ρ.x)(λx:σ → τ → ρ.λy:σ → τ.λz:σ.x z (y z)). ∆ is a simply-typed term of type (σ → τ → ρ) → (σ → τ → ρ)
, and its essence is ∆ ≡ S K S. Consider the following counter-example: . . .

T = β ∆ : (σ → τ → ρ) → (σ → τ → ρ) x:σ T = β x : σ T = β λx:σ.x : σ → σ S K S = β λx.x T = β ∆, λx:σ.x : ((σ → τ → ρ) → (σ → τ → ρ)) ∩ (σ → σ) T = β pr 2 ∆, λx:σ.x : σ → σ
The essence of the above term is S K S, but, if σ is an atomic type:

T ∩ S K S : σ → σ
Loss of soundness in ∆ CDV = βη is proved via the following counterexample, where

Γ def = {x:(σ → τ ) ∩ ρ}. Γ, y:σ T CDV = βη x : (σ → τ ) ∩ ρ Γ, y:σ T CDV = βη pr 1 x : σ → τ Γ, y:σ T CDV = βη y : σ Γ, y:σ T CDV = βη (pr 1 x) y : τ Γ T CDV = βη λy:σ.(pr 1 x) y : σ → τ Γ T CDV = βη x : (σ → τ ) ∩ ρ Γ T CDV = βη pr 2 x : ρ λy.x y = βη x Γ T CDV = βη λy:σ.(pr 1 x) y, pr 2 x : (σ → τ ) ∩ ρ Γ T CDV = βη pr 2 λy:σ.(pr 1 x) y, pr 2 x : ρ
The essence of pr 2 λy:σ.(pr 1 x) y, pr 2 x is λy.x y, but, if ρ is an atomic type:

x:(σ → τ ) ∩ ρ T CDV ∩ λy.x y : ρ
Loss of soundness in ∆ BCD = βη is proved via the following counterexample:

x:σ, y:

U T BCD = βη x : σ σ T U → U x:σ, y:U T BCD = βη x U→U : U → U x:σ, y:U T BCD = βη y : U x:σ, y:U T BCD = βη x U→U y : U x:σ T BCD = βη λy:U.x U→U y : U → U x:σ T BCD = βη x : σ λy.x y = βη x x:σ T BCD = βη λy:U.x U→U y, x : (U → U) ∩ σ x:σ T BCD = βη pr 2 λy:U.x U→U y, x : σ
The essence of pr 2 λy:U.x U→U y, x is λy.x y, but, if σ is an atomic type (different than U):

x:σ T BCD ∩ λy.x y : σ ( ) Let M be such that Γ T ∩ M : σ for a given Γ. We proceed by induction on the derivation. All cases proceed straightforwardly since all rules of the type and subtype assignment system T ∩ correspond exactly to the rules of the same name in the corresponding typed system T R and in the same type theory T . Therefore a ∆-term can be easily be constructed and derived with type σ.

The last theorem characterizes the class of strongly normalizing ∆-terms.

Theorem 2.23 (Characterization). Every strongly normalizing λ-term can be typeannotated so as to be the essence of a typable ∆-term.

Proof. We know that every strongly normalizing λ-term M is typable in λ T ∩ . By Theorem 2.22 we have that ∆ T R λ T ∩ , therefore there exists some typable ∆, such that M ≡ ∆ .

We can finally state decidability of type checking (TC) and type reconstruction (TR).

Theorem 2.24 (Decidability of type checking and type reconstruction).

∆ T R TC/TR ∆ CD ≡ √ ∆ CDV ≡ √ ∆ CDS ≡ √ ∆ BCD ≡ √ ∆ CD = β √ ∆ CDV = β √ ∆ CDS = β × ∆ BCD = β × ∆ CDV = βη √ ∆ BCD = βη × Proof.
Both type checking and type reconstruction can be proved by induction on the structure of ∆, using the decidability of T BCD proved by Hindley [START_REF] Hindley | The simple semantics for Coppo-Dezani-Sallé types[END_REF] (see also [START_REF] Liquori | A decidable subtyping logic for intersection and union types[END_REF]). By Theorem 2.22, the essences of all the ∆-terms, which are typable in

∆ CD = β , ∆ CDV = β , or ∆ CDV = βη , are typable in λ CD
∩ or λ CDV ∩ , therefore they are strongly normalizing. As a consequence, the side-condition

∆ 1 R ∆ 2 is decidable for ∆ CD = β , ∆ CDV = β
, and ∆ CDV = βη and so type reconstruction and type checking are decidable too.

Type reconstruction and type checking are not decidable in ∆ CDS = β , ∆ BCD = β , and ∆ BCD = βη , because u M , u N is typable if and only if M = β N (resp. M = βη N ). However, M and N are arbitrary pure λ-terms, and both β-equality and βη-equality are undecidable.

Subtyping and explicit coercions

Γ T R ∆ : σ σ T τ Γ T R ∆ τ : τ ( T )
is translated into the following (coercion-free) derivation

Γ T R σ T τ : σ → τ Γ T R ∆ Γ : σ Γ T R σ T τ ∆ Γ : τ (→E)
where R is a suitable relation such that R R . Note that changing of the type theory is necessary to guarantee well-typedness in the translation of strong pairs. Summarizing, we provide a type preserving translation of a ∆-term into a coercion-free ∆-term such that ∆ = βη ∆ .

The following example illustrates some trivial compilations of axioms and rule schemes of (refl) the judgment x:σ T R x, x σ : σ ∩ σ is translated to a coercion-free judgment

x:σ T = β x, (λy:σ.y) x : σ ∩ σ (incl) the judgment x:σ ∩τ T R x, x τ : (σ ∩τ )∩τ is translated to a coercion-free judgment

x:σ ∩ τ T = β x, (λy:σ ∩ τ.pr 2 y) x : (σ ∩ τ ) ∩ τ (glb) the judgment x:σ T R x, x σ∩σ : σ ∩ (σ ∩ σ) is translated to a coercion-free judgment x:σ T = β x, (λy:σ. y, y ) x : σ ∩ (σ ∩ σ) (U top ) the judgment x:σ T R x, x U : σ ∩ U is translated to a coercion-free judgment x:σ T = β x, (λy:σ.u y ) x : σ ∩ U (U → ) the judgment x:U T R x, x σ→U : U∩(σ → U) is translated to a coercion-free judgment x:U T = βη x, (λf :U.λy:σ.u (f y) ) x : U ∩ (σ → U) (→∩) the judgment x:(σ → τ ) ∩ (σ → ρ) T R x σ→τ ∩ρ : σ → τ ∩ ρ is translated to a coercion-free judgment x:σ T = βη (λf :σ .λy:σ. (pr 1 f ) y, (pr 2 f ) y ) x : σ → τ ∩ ρ where σ = (σ → τ ) ∩ (σ → ρ) (→) the judgment x:σ → τ ∩ ρ T R x, x σ∩ρ→τ : (σ → τ ∩ ρ) ∩ (σ ∩ ρ → τ ) is translated to a coercion-free judgment x:σ → τ ∩ ρ T = βη x, (λf :σ → τ ∩ ρ.λy:σ ∩ ρ.pr 1 (f (pr 1 y))) x : σ where σ = (σ → τ ∩ ρ) ∩ (σ ∩ ρ → τ ) (trans) the judgment x:σ T R x, (x U ) σ→U : σ ∩ (σ → U) is translated to a coercion-free judgment x:σ T = βη x, (λf :U.λy:σ.u (f y) ) ((λy:σ.u y ) x) : σ ∩ (σ → U)
The next definition introduces two maps translating subtype judgments into explicit coercions functions and ∆-terms into coercion-free ∆-terms. (refl)

σ T σ def = T = β λx:σ.x : σ → σ (incl 1 ) σ ∩ τ T σ def = T = β λx:σ ∩ τ.pr 1 x : σ ∩ τ → σ (incl 2 ) σ ∩ τ T τ def = T = β λx:σ ∩ τ.pr 2 x : σ ∩ τ → τ (glb) ρ T σ ρ T τ ρ T σ ∩ τ def = T = β λx:ρ. ρ T σ x, ρ T τ x : ρ → σ ∩ τ (trans) σ T τ τ T ρ σ T ρ def = T = β λx:σ. τ T ρ ( σ T τ x) : σ → ρ (U top ) σ T U def = T = β λx:σ.u x : σ → U (U → ) U T σ → U def = T = βη λf :U.λx:σ.u (f x) : U → (σ → U) Let ξ 1 def = (σ → τ ) ∩ (σ → ρ) and ξ 2 def = σ → τ ∩ ρ (→∩) ξ 1 T ξ 2 def = T = βη λf :ξ 1 .λx:σ. (pr 1 f ) x, (pr 2 f ) x : ξ 1 → ξ 2 Let ξ 1 def = σ 1 → τ 1 and ξ 2 def = σ 2 → τ 2 (→) σ 2 T σ 1 τ 1 T τ 2 σ 1 → τ 1 T σ 2 → τ 2 def = T = βη λf :ξ 1 .λx:σ 2 . τ 1 T τ 2 (f ( σ 2 T σ 1 x)) : ξ 1 → ξ 2 2.
The translation -Γ is defined on ∆ as follows:

u M Γ def = u M x Γ def = x λx:σ.∆ Γ def = λx:σ. ∆ Γ,x:σ ∆ 1 ∆ 2 Γ def = ∆ 1 Γ ∆ 2 Γ ∆ 1 , ∆ 2 Γ def = ∆ 1 Γ , ∆ 2 Γ pr i ∆ Γ def = pr i ∆ Γ i ∈ {1, 2} ∆ τ Γ def = σ T τ ∆ Γ if Γ T R ∆ : σ.
By looking at the above translation functions we can see that if Γ T R ∆ : σ, then ∆ Γ is defined and it is coercion-free.

The following lemma states that a coercion function is always typable in ∆ T = βη , that it is essentially the identity and that, without using the rule schemes (→∩), (U → ), and (→) the translation can even be derivable in ∆ T = β .

Lemma 2.25 (Essence of a coercion is an identity). Proof. The proofs proceed in both parts by induction on the derivation of σ T τ . For instance, in case of (glb), we can verify that T = β λx:ρ. ρ T σ x, ρ T τ x : ρ → σ∩τ using the induction hypotheses that ρ T σ (resp. ρ T τ ) has type ρ → σ (resp. ρ → τ ) and has an essence convertible to λx.x.

1. If σ T τ , then T = βη σ T τ : σ → τ and σ T τ = βη λx.x; Source Target ∆ CD ≡ ∆ CD = β ∆ CDV ≡ ∆ CDV = βη ∆ CDS ≡ ∆ CDS = β ∆ BCD ≡ ∆ BCD = βη ∆ CD = β ∆ CD = β ∆ CDV = β ∆ CDV = βη ∆ CDS = β ∆ CDS = β ∆ BCD = β ∆ BCD = βη ∆ CDV = βη ∆ CDV = βη ∆ BCD = βη ∆ BCD = βη
We can now prove the coherence of the translation as follows: Proof. By induction on the derivation. We illustrate the most important case, namely when the last type rule is ( T ). In this case ∆ τ Γ is translated to σ T τ ∆ Γ . By induction hypothesis we have that Γ T R ∆ : σ, and by Lemma 2.25 we have that

Γ T R σ T τ : σ → τ ; therefore Γ T R ∆ τ Γ : τ . Moreover, we know that σ T τ R λx.
x, and this gives ∆ τ Γ R ∆ Γ . Again by induction hypothesis we have that ∆ Γ R ∆ , and this gives the thesis

∆ τ Γ R ∆ τ .
Chapter 3

Adding union types

This chapter is a contribution to the study of typed λ-calculi à la Church in presence of intersection and union types. We inspect the relationship between pure λ-calculus and its corresponding ∆-calculus. We present and explore the relationships between the following three formal systems:

λ BDdL , the type assignment system with intersection and union types for pure λcalculus with subtyping with the type theory Ξ, as defined in [7]: type assignment judgments have the shape Γ M : σ;

λ@ BDdL , an extension of the typed λ-calculus with strong pairs and strong sums, as defined in [START_REF] Daniel | Logic and computation in a lambda calculus with intersection and union types[END_REF], with subtyping and explicit coercions: type judgments have the shape Γ M @∆ : σ, where ∆ is a typed λ-term enriched with strong pairs and strong sums;

-∆ BDdL , an extension of the ∆ BCD ≡ of Chapter 2 with ad hoc formulae and inference rules for subtyping and explicit coercions: type judgments have the shape Γ ∆ : σ.

Intuitively, ∆ denotes a proof for a type assignment derivation for M ; from an operational point of view, reductions in pure M and typed ∆ must be synchronized by suitable synchronous reduction rules in order to preserve the reduction of subjects. From a typing point of view, the type rules of λ@ BDdL should encode the proof-functional nature of strong intersection and strong union, i.e. the fact that in a strong pair (or strong sums) the two ∆ relate to the same M . Thanks to an erasing functiontranslating typed ∆ into pure M , we could reason only on ∆ BDdL assigning types to ∆.

In summary, this chapter extends Chapter 2 with union types. The important points of this chapter are as follows:

-we define ∆ BDdL obtained by extending the generic ∆-calculus with union types and by fixing a single type theory T and equivalence relation R, while keeping decidability of type checking, and showing the isomorphism with the type assignment system λ BDdL of [7]. As such, ∆-terms are typed λ-terms enriched with both strong pairs and and strong sums;

-we define the typed λ-calculus λ@ BDdL which is a decorated version of ∆ BDdL . Terms of λ@ BDdL have the form M @∆ where M is a pure λ-term; -we prove the isomorphism property between ∆ BDdL and λ@ BDdL (Theorem 3.1), as well as the other usual properties, such as subject reduction, Church-Rosser, strong normalization, unicity of typing, and decidability of type reconstruction and of type checking (Theorem 3.2).

Γ M : U (U) Γ M : σ σ τ Γ M : τ ( ) x:σ ∈ Γ Γ x : σ (Var) Γ, x:σ 1 M : σ 2 Γ λx.M : σ 1 → σ 2 (→I) Γ M : σ 1 → σ 2 Γ N : σ 1 Γ M N : σ 2 (→E) Γ M : σ 1 Γ M : σ 2 Γ M : σ 1 ∩ σ 2 (∩I) Γ M : σ 1 ∩ σ 2 i = 1, 2 Γ M : σ i (∩E i ) Γ M : σ i i = 1, 2 Γ M : σ 1 ∪ σ 2 (∪I i ) Γ, x:σ 1 M : σ 3 Γ, x:σ 2 M : σ 3 Γ N : σ 1 ∪ σ 2 Γ M [N/x] : σ 3 (∪E)
This chapter is organized as follows: in Section 3.1, we present the syntax and semantics of ∆ BDdL and λ@ BDdL . In Section 3.2, we study the metatheory of ∆ BDdL and λ@ BDdL .

Syntax and semantics of ∆ BDdL and λ@ BDdL

The syntax of σ, M , ∆, and the derived M @∆ are defined using a set of atomic types A ∞ and the following three syntactic categories:

σ ::= U | φ | σ → σ | σ ∩ σ | σ ∪ σ M ::= x | λx.M | M M ∆ ::= u M | x | λx:σ.∆ | ∆ ∆ | ∆, ∆ | [∆, ∆] | pr 1 ∆ | pr 2 ∆ | in σ 1 ∆ | in σ 2 ∆ | ∆ σ
where φ denotes atomic types belonging in A ∞ , and U denotes a special type that is inhabited by all pure λ-terms and all constants u M . The ∆-expression ∆, ∆ denotes the strong pair, while [∆, ∆] denotes the strong sum, with the respective projections and injections, respectively. Finally, ∆ σ denotes the explicit coercion of ∆ with the type σ.

The untyped reduction semantics for the calculus à la Curry λ BDdL corresponds to ordinary β-reduction, even if subject reduction holds only in presence of the "Gross-Knuth" parallel reduction (see Definition 13.2.7 in [START_REF] Barendregt | The Lambda Calculus: Its Syntax and Semantics[END_REF]), where all redexes in M are contracted simultaneously. Reduction for the calculus à la Church λ@ BDdL is delicate because it must keep synchronized the untyped reduction of M with the typed reduction of ∆: it is defined in Section 5 of [START_REF] Daniel | Logic and computation in a lambda calculus with intersection and union types[END_REF]. Reductions in ∆ BDdL are defined from these three notions of reductions:

(λx:σ.∆ 1 ) ∆ 2 → β ∆ 1 [∆ 2 /x] (β) pr i ∆ 1 , ∆ 2 → pr i ∆ i (pr i ) [λx:σ 1 .∆ 1 , λx:σ 2 .∆ 2 ] in τ i ∆ 3 → in i ∆ i [∆ 3 /x] i ∈ {1, 2} (in i ) (∪I i ) Γ M @∆ : σ σ τ Γ M @∆ τ : τ ( ) Γ, x:σ 1 M @∆ 1 : σ 3 Γ, x:σ 2 M @∆ 2 : σ 3 Γ N @∆ 3 : σ 1 ∪ σ 2 Γ M [N/x]@[λx:σ 1 .∆ 1 , λx:σ 2 .∆ 2 ] ∆ 3 : σ 3 (∪E) Figure 3.2: Typed calculus λ@ BDdL [40]
We write -→ βpr i in i for the contextual closure of the (β), (pr i ) and (in i ) notions of reduction. We write -→ -→ βpr i in i as the reflexive and transitive closure of -→ βpr i in i . We mostly consider βpr i in i -reductions, thus to ease the notation, we will often omit the subscript in βpr i in i -reductions. We note -→ -→ for the synchronous reduction, i.e. the reduction relation where the transitive closure for strong pairs and strong sums are the following rules:

∆ 1 → ∆ ∆ 1 ∆ 2 → ∆ ∆ 2 ∆ 1 ≡ ∆ 2 ∆ 1 , ∆ 2 → ∆ ∆ 1 , ∆ 2 (Congr ∩ ) ∆ 1 → ∆ ∆ 1 ∆ 2 → ∆ ∆ 2 ∆ 1 ≡ ∆ 2 [∆ 1 , ∆ 2 ] → ∆ [∆ 1 , ∆ 2 ] (Congr ∪ )
Figure 3.1 presents the main rules of the type assignment system of [7]: note that type inference is not syntax-directed, and undecidable. Figure 3.2 presents the main rules of the typed calculus λ@ BDdL of [START_REF] Daniel | Logic and computation in a lambda calculus with intersection and union types[END_REF]; note that this type system is completely syntax directed and decidable.

The next definition clarifies what we intend with isomorphism between an untyped M and a typed ∆: the essence function shows the syntactic relation between pure λ-terms and ∆-terms. Essence maps typed ∆-terms into untyped λ-terms: intuitively, two typed ∆-terms proves the same formula if they have the same essence. The essence function between pure and typed λ-terms is defined as follows:

Definition 3.1 (Proof Essence). u M def = M x def = x λx:σ.∆ def = λx. ∆ ∆ 1 ∆ 2 def = ∆ 1 ∆ 2 ∆ σ def = ∆ pr i ∆ def = ∆ in σ i ∆ def = ∆ ∆ 1 , ∆ 2 def = ∆ 1 [λx:σ 1 .∆ 1 , λx:σ 2 .∆ 2 )] ∆ 3 def = ∆ 1 [ ∆ 3 /x] Γ u M : U (U) Γ ∆ : σ σ τ Γ ∆ τ : τ ( ) x:σ ∈ Γ Γ x : σ (Var) Γ, x:σ 1 ∆ : σ 2 Γ λx:σ 1 .∆ : σ 1 → σ 2 (→I) Γ ∆ 1 : σ 1 → σ 2 Γ ∆ 2 : σ 1 Γ ∆ 1 ∆ 2 : σ 2 (→E) Γ ∆ 1 : σ 1 Γ ∆ 2 : σ 2 ∆ 1 ≡ ∆ 2 Γ ∆ 1 , ∆ 2 : σ 1 ∩ σ 2 (∩I) Γ ∆ : σ 1 ∩ σ 2 i ∈ {1, 2} Γ pr i ∆ : σ i (∩E i ) Γ ∆ : σ i {i, j} = {1, 2} Γ in σ j i ∆ : σ 1 ∪ σ 2 (∪I i ) Γ, x:σ 1 ∆ 1 : σ 3 ∆ 1 = β ∆ 2 Γ, x:σ 2 ∆ 2 : σ 3 Γ ∆ 3 : σ 1 ∪ σ 2 Γ [λx:σ 1 .∆ 1 , λx:σ 2 .∆ 2 ] ∆ 3 : σ 3 (∪E) Figure 3.3: ∆-calculus ∆ BDdL
The essence function is basically an erasing function that forgets all typing information and the second component of strong pairs and strong sums.

Figure 3.3 presents the main rules of ∆ BDdL of [START_REF] Daniel | A realizability interpretation for intersection and union types[END_REF]: this system can be seen as a prooffunctional logic, in the sense of Pottinger [START_REF] Pottinger | A type assignment for the strongly normalizable λ-terms[END_REF] and López-Escobar [START_REF] Edgar | Proof functional connectives[END_REF]: formulae encode, using the Curry-Howard isomorphism, derivations D : Γ M : σ in the type assignment system λ BDdL which are, in turn, isomorphic to typed judgments Γ M @∆ : σ of λ@ BDdL . It is worth noticing that if we drop the restriction concerning the essence in rules (∩I) and (∪E) in the system ∆ BDdL , replace σ ∩ τ by σ × τ , and σ ∪ τ by σ + τ , then we get a simply typed λ-calculus with product and sums, namely the usual intuitionistic propositional NJ logic with implication, conjunction, and disjunction in disguise: the resulting system loses its proof-functionality.

All the introduced typed systems also use a subtyping relation, written σ τ . Subtyping is defined from a type theory, which is a collection of inequalities between types satisfying natural closure conditions. Definition 3.2 (Type theory Ξ). The type theory Ξ (see Definition 3.6 of [7]), is an extension of the type theory T BCD of Figure 2.3, and is defined by the following subtyping axioms and inference rules:

(1) σ σ ∩ σ (8) σ 1 σ 2 , τ 1 τ 2 ⇒ σ 1 ∪ τ 1 σ 2 ∪ τ 2 (2) σ ∪ σ σ (9) σ τ, τ ρ ⇒ σ ρ (3) σ ∩ τ σ, σ ∩ τ τ (10) σ ∩ (τ ∪ ρ) (σ ∩ τ ) ∪ (σ ∩ ρ) (4) σ σ ∪ τ, τ σ ∪ τ (11) (σ → τ ) ∩ (σ → ρ) σ → (τ ∩ ρ) (5) σ U (12) (σ → ρ) ∩ (τ → ρ) (σ ∪ τ ) → ρ (6) σ σ (13) U U → U (7) σ 1 σ 2 , τ 1 τ 2 ⇒ σ 1 ∩ τ 1 σ 2 ∩ τ 2 (14) σ 2 σ 1 , τ 1 τ 2 ⇒ σ 1 → τ 1 σ 2 → τ 2
The theory Ξ suggests the interpretation of U as the set universe, of ∩ as the set intersection, of ∪ as the set union, and of as a subset relation, respectively, in the spirit of [START_REF] Frisch | Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types[END_REF].

In the following, we write σ ∼ τ if, and only if, σ τ and τ σ. We note that distributivity of union over intersection and intersection over union, i.e. σ ∪ (τ ∩ ρ) ∼ (σ ∪ τ ) ∩ (σ ∪ ρ), and σ ∩ (τ ∪ ρ) ∼ (σ ∩ τ ) ∪ (σ ∩ ρ) are derivable (see, e.g. derivation in [7], page 9).

Once the subtyping preorder has been defined, a classical subsumption rule and two explicit coercion rule can be defined as follows:

Γ M : σ σ τ Γ M : τ ( ) Γ M @∆ : σ σ τ Γ M @∆ τ : τ ( ) Γ ∆ : σ σ τ Γ ∆ τ : τ ( )
In a nutshell, the first rule is a subsumption, while the two others are explicit coercions, because of the type decoration.

Metatheory of ∆ BDdL and λ@ BDdL

The next theorem relates the three systems: the key concept is the essence function that allows to interpret union, intersection, and explicit coercions as proof-functional connectives.

Theorem 3.1 (Isomorphism). Let M , ∆, Γ, and σ. Then:

1. Γ M : σ iff Γ ∆ : σ and ∆ ≡ M ; 2. Γ M @∆ : σ iff Γ ∆ : σ; 3. Γ M : σ iff Γ M @∆ : σ.
Proof.

1. by adding union types to the proof of Theorem 2.22;

2. by induction on the structure of derivations;

3. by parts 1 and 2.

The next theorem states that adding union types does not break the properties of the new typed systems.

Theorem 3.2 (Conservativity).

The typed systems λ@ BDdL and ∆ BDdL preserve subject reduction (for the synchronous β-reduction), Church-Rosser, strong normalization, unicity of typing, and decidability of type reconstruction and of type checking.

Proof. For proving properties of λ@ BDdL we proceeds by upgrading results of Theorems 2.4, 2.11, 2.21, 2.19, and Lemma 2.5. Properties of λ@ BDdL are mostly inherited by ∆ BDdL using Theorem 3.1 or, as for case of subject reduction for βpr i in i -reductions, is proved by induction on the structure of the derivation.

Chapter 4 On Mints' realizability

This chapter deals with finding a realizability interpretation of union and intersection types using Mints' realizers [START_REF] Mints | The completeness of provable realizability[END_REF]. Intuitively, a Mints' realizer r σ [M ] is a logical proposition stating that M has type σ.

Similarly to the system of intersection types, the type assignment system λ BDdL has no trivial set-theoretic interpretation (see [7]). It is noteworthy that some similar systems have a clear set-theoretic interpretation (see e.g. Frisch, Castagna, and Benzaken [START_REF] Frisch | Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types[END_REF]).

This chapter provides both a intuitive semantics for union types and a logical foundation for ∆ BDdL . We do this by interpreting the union type assignment system into the intuitionistic first order logic NJ(β) with Mints' provable realizability of intersection types extended with union. Then, we prove that the terms of ∆ BDdL correspond to logical derivations in NJ(β).

From Theorem 3.1, we know that if Γ M @∆ : σ, then there is a tight relation among ∆ and M , namely ∆ ≡ M . In ∆ BDdL , ∆ can also be seen as a simply-typed term: if we drop the restriction concerning the essence in rules (∩I) and (∪E) in ∆ BDdL replacing σ ∩ τ by σ × τ and σ ∪ τ by σ + τ , then we get a simply typed λ-calculus with product and sums, namely the intuitionistic propositional logic with implication, conjunction, and disjunction in disguise.

We could provide a logical foundation for ∆ BDdL by interpreting it into an extension of Mints' provable realizability. However, when proving a formula r σ [M ], we have two kinds of realizers: the former is the pure λ-term M , while the latter is the ∆-term that turn out to be realizers in the ordinary sense of intuitionistic logic.

Therefore, we prove in Theorem 5.4 that, if Γ ∆ :

σ is derivable in ∆ BDdL , then ∆ realizes the NJ(β) judgment G Γ NJ(β) r σ [ ∆ ].
However, the converse is not true, as is shown in Section 4.3.

For this aim, we use and extend Mints' approach of provable realizability [START_REF] Mints | The completeness of provable realizability[END_REF]3,8]. We interpret the statement M @∆ : σ as "∆ is a construction of M : σ"; on the other hand M : σ is the meaning of the formula r σ [M ], provided that we extend the notion to cope with union types; the latter formula reads as "M is a method to assess σ", following the terminology of [START_REF] Edgar | Proof functional connectives[END_REF]8]; now, the meaning of ∆ is that it is a constructive proof of r σ [M ], and hence it is a realizer of this formula. In short, we have two kinds of realizers on two levels: the realizer M , which is a Mints' realizer of σ, and the realizer ∆ which is an ordinary realizer, in the sense of standard Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic, of the statement r σ [M ]: in simpler words, ∆ represents an encoding of the logical derivation of

r σ [M ].
This chapter is organized as follows: in Section 4.1, we present the logic NJ(β) along

A ∈ G G NJ(β) A (Ax) G Γ NJ(β) P φ (M ) M = β N G Γ NJ(β) P φ (N ) (β) G NJ(β) ( I) G NJ(β) ⊥ G NJ(β) A (⊥E) G NJ(β) A G NJ(β) B G NJ(β) A ∧ B (∧I) G NJ(β) A 1 ∧ A 2 i = 1, 2 G NJ(β) A i (∧E i ) G NJ(β) A i i = 1, 2 G NJ(β) A 1 ∨ A 2 (∨I i ) G, A NJ(β) C G, B NJ(β) C G NJ(β) A ∨ B G NJ(β) C (∨E) G, A NJ(β) B G NJ(β) A ⊃ B (⊃ I) G NJ(β) A ⊃ B G NJ(β) A G NJ(β) B (⊃ E) G NJ(β) A x ∈ Fv(G) G NJ(β) ∀x.A (∀I) G NJ(β) ∀x.A G NJ(β) A[t/x] (∀E) G NJ(β) A[t/x] G NJ(β) ∃x.A (∃I) G NJ(β) ∃x.A G, A[c/x] NJ(β) C c ∈ Fv(G) G NJ(β) C (∃E)

Presentation of NJ(β)

The next definition introduces formally the NJ(β) logic1 .

Definition 4.1. (Logic NJ(β)).

1. let P φ (x) be a unary predicate for each atomic type φ: the natural deduction system for first-order intuitionistic logic NJ(β) extends NJ with untyped λ-terms and predicates P φ (x), and the rule (β). The full description of NJ(β) can be found in Figure 4.1. Note that ⊃ denotes logical implication, and ⊥ denote truth and falsehood, while ∧ and ∨ are the logical connectives for conjunction and disjunction respectively, that must be kept distinct from ∩ and ∪;

for a given context

Γ def = {x 1 :σ 1 , . . . , x n :σ n } of ∆ BDdL , we define a logical context G Γ def = r σ 1 [x 1 ], . . . , r σn [x n ] of NJ(β).
It is clear that G Γ,x:σ ≡ G Γ , r σ [x] and x ∈ Fv(G Γ ), since x ∈ Dom(Γ), by context definition. In the rest of this chapter, we will define Mints' realizability for ∆ BDdL .

We now give a precise definition of the notion of realizer, as first introduced for intersection types by Mints [START_REF] Mints | The completeness of provable realizability[END_REF], and extended in [START_REF] Daniel | A realizability interpretation for intersection and union types[END_REF]. Definition 4.2 (Mints' realizers in NJ(β) [START_REF] Daniel | A realizability interpretation for intersection and union types[END_REF]). Let P φ (-) be a unary predicate for each atomic type φ. We define the predicates r σ [-] for each type σ by induction over σ, as follows:

r φ [M ] def = P φ (M ) r σ 1 →σ 2 [M ] def = ∀y.r σ 1 [y] ⊃ r σ 2 [M y] r U [M ] def = r σ 1 ∪σ 2 [M ] def = r σ 1 [M ] ∨ r σ 2 [M ] r σ 1 ∩σ 2 [M ] def = r σ 1 [M ] ∧ r σ 2 [M ]
Formulae have the shape r σ [M ], whose intended meaning is that M has type σ in the intersection-union type discipline with subtyping.

Intuitively, we write r σ [M ] to denote a formula in NJ(β), realized by the pure λ-term M of type σ in λ BDdL .

Soundness of NJ(β)

This section states that ∆ BDdL is sound w.r.t. Mints' realizers in NJ(β). We first start with a few technical lemmas.

G Γ NJ(β) r σ [N ] M = β N G Γ NJ(β) r σ [M ] (Eqβ)
Proof. By induction over σ.

Lemma 4.2 (Admissibility in NJ(β)).

The following rules are admissible in NJ(β):

G Γ , r σ 1 [x] NJ(β) r σ 2 [M ] G Γ NJ(β) r σ 1 →σ 2 [λx.M ] (→ I) G Γ NJ(β) r σ 1 →σ 2 [M ] G Γ NJ(β) r σ 1 [N ] G Γ NJ(β) r σ 2 [M N ] (→ E) G Γ NJ(β) r σ 1 [M ] G Γ NJ(β) r σ 2 [M ] G Γ NJ(β) r σ 1 ∩σ 2 [M ] (∩I) G Γ NJ(β) r σ 1 ∩σ 2 [M ] i ∈ {1, 2} G Γ NJ(β) r σ i [M ] (∩E) G Γ NJ(β) r σ i [M ] i ∈ {1, 2} G Γ NJ(β) r σ 1 ∪σ 2 [M ] (∪I) G Γ NJ(β) r σ [M ] σ τ G Γ NJ(β) r τ [M ] ( ) G Γ , r σ 1 [x] NJ(β) r σ 3 [M ] G Γ , r σ 2 [x] NJ(β) r σ 3 [M ] G Γ NJ(β) r σ 1 ∪σ 2 [N ] G Γ NJ(β) r σ 3 [M [N/x]] (∪E)
Proof. We can see that:

-rules (∩I), (∩E), and (∪I) correspond respectively to rules (∧I), (∧E), and (∨I);

-rule (∪E) is derivable from rule (∨E) and a classical substitution lemma;

-rule (→ I) and (→ E) are derivable:

G Γ , r σ 1 [x] NJ(β) r σ 2 [M ] G Γ , r σ 1 [x] NJ(β) r σ 2 [(λx.M ) x] (Eqβ) G Γ NJ(β) r σ 1 [x] ⊃ r σ 2 [(λx.M ) x] (⊃ I) G Γ NJ(β) ∀x.r σ 1 [x] ⊃ r σ 2 [(λx.M ) x] (∀I)
and:

G Γ NJ(β) r σ→τ [M ] G Γ NJ(β) r σ [N ] ⊃ r τ [M N ] (∀E) G Γ NJ(β) r σ [N ] G Γ NJ(β) r τ [M N ] (⊃ E)
-it can be showed that all the subtyping rules are derivable in NJ(β), therefore ( ) is derivable.

We can now prove relations between λ BDdL (and λ@ BDdL , and ∆ BDdL ) and NJ(β).

Lemma 4.3 (λ BDdL vs. NJ(β)). If Γ M : σ then G Γ NJ(β) r σ [M ].
Proof. By structural induction on the derivation tree of Γ M : σ: all the rules can be replaced with rules of the same name (using Lemma 4.2), except rule (Var) which is replaced by rule (Ax).

Lemma 4.4.

If Γ M @∆ : σ in λ@ BDdL then G Γ NJ(β) r σ [M ].
Proof. Because of Lemma 4.3 and because λ@ BDdL and λ BDdL are equivalent by Theorem 3.1.

Theorem 4.5 (Soundness). If Γ ∆ : σ is derivable in ∆ BDdL , then G Γ NJ(β) r σ [ ∆ ].
Proof. By Theorem 3.1 if Γ ∆ : σ is derivable then Γ ∆ @∆ : σ. The thesis follows by Lemma 4.4.

Remark 4.1. The type assignment system λ BDdL of [7] was based on the type theory Ξ (see Definition 3.6 of [7]): the paper also introduced a stronger type theory, called Π, by adding the extra axiom:

(15)

P(σ) ⇒ σ → τ ∪ ρ (σ → τ ) ∪ (σ → ρ),
where P(σ) is true if σ syntactically corresponds to an Harrop formula. However, in NJ(β), the judgment

r σ→(τ ∪ρ) [x] NJ(β) r (σ→τ )∪(σ→ρ) [x] is not derivable because the judgment A ⊃ (B ∨ C) NJ(β) (A ⊃ B) ∨ (A ⊃ C) is not derivable in NJ.
As such, the type theory Π cannot be overlapped with an interpretation of types as sets, as the following example show. The identity function λx.x inhabits the function set {a, b} → {a} ∪ {b} but, by axiom [START_REF] Bertot | Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions[END_REF], it should also inhabit {a, b} → {a} or {a, b} → {b}, which is clearly not the case.

Completeness of NJ(β)

One may wonder why there is no theorem stating ∆ BDdL can realize every derivation of NJ(β). The conjecture that we would like to prove is the following:

Conjecture 4.1 (Completeness). If G Γ NJ(β) r σ [M ]
then there exists N = β M and ∆ such that Γ N @∆ : σ in λ@ BDdL and therefore Γ ∆ : σ in ∆ BDdL .

Note that the condition N = β M is necessary because λ BDdL does not enjoy subject conversion, while Lemma 4.1 enforces subject conversion. However, this conjecture has still not been proven (or disproven) yet.

Failure of completeness of NJ(β) without subtyping

It seems that subtyping is an essential component of the conjectured completeness result. Intuitively, if we naively interpret types as sets, it is clear that the set

(σ ∪ τ ) ∩ (σ ∪ ρ) is a subset of σ ∪ (τ ∩ ρ)
, and it appears that we can prove in NJ(β) that the identity function has type

(σ ∪ τ ) ∩ (σ ∪ ρ) → σ ∪ (τ ∩ ρ), as is shown in Subsection 4.3.2. However, in λ BDdL , the λ-term λx.x cannot have type (σ ∪ τ ) ∩ (σ ∪ ρ) → σ ∪ (τ ∩ ρ) if we don't consider subtyping.

Counter-example

We show that NJ(β) r (σ∪τ )∩(σ∪ρ)→σ∪(τ ∩ρ) [λx.x] is derivable in NJ(β).

D 1 (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rσ[y] NJ(β) rσ[(λx.x)y] ∨ (rτ [(λx.x)y] ∧ rρ[(λx.x)y]) D 2 (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y] NJ(β) rσ[(λx.x)y] ∨ (rτ [(λx.x)y] ∧ rρ[(λx.x)y]) D 6 (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]) NJ(β) rσ[y] ∨ rτ [y] (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]) NJ(β) rσ[(λx.x)y] ∨ (rτ [(λx.x)y] ∧ rρ[(λx.x)y]) (∨E) NJ(β) (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]) ⊃ rσ[(λx.x)y] ∨ (rτ [(λx.x)y] ∧ rρ[(λx.x)y]) (⊃ I) NJ(β) r (σ∪τ )∩(σ∪ρ) [y] ⊃ r σ∪(τ ∩ρ) [(λx.x)y] (≡) NJ(β) ∀y.r (σ∪τ )∩(σ∪ρ) [y] ⊃ r σ∪(τ ∩ρ) [(λx.x)y] (∀I) NJ(β) r (σ∪τ )∩(σ∪ρ)→σ∪(τ ∩ρ) [λx.x] (≡)
where D 1 is:

(rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rσ[y] NJ(β) rσ[y] (Ax) y = βη (λx.x)y (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rσ[y] NJ(β) rσ[(λx.x)y] (Axβη) (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rσ[y] NJ(β) rσ[(λx.x)y] ∨ (rτ [(λx.x)y] ∧ rρ[(λx.x)y]) (∨I)
and D 2 is:

D 3 (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y], rσ[y] NJ(β) rσ[(λx.x)y] ∨ (rτ [(λx.x)y] ∧ rρ[(λx.x)y]) D 4 (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y], rρ[y] NJ(β) rσ[(λx.x)y] ∨ (rτ [(λx.x)y] ∧ rρ[(λx.x)y]) D 5 (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y] NJ(β) rσ[y] ∨ rρ[y] (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y] NJ(β) rσ[(λx.x)y] ∨ (rτ [(λx.x)y] ∧ rρ[(λx.x)y]) (∨E)
and D 3 is:

(rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y], rσ[y] NJ(β) rσ[y] (Ax) y = βη (λx.x)y (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y], rσ[y] NJ(β) rσ[(λx.x)y] (Axβη) (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y], rσ[y] NJ(β) rσ[(λx.x)y] ∨ (rτ [(λx.x)y] ∧ rρ[(λx.x)y])
and D 4 is:

(rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y], rρ[y] NJ(β) rτ [y] (Ax) y = βη (λx.x)y (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y], rρ[y] NJ(β) rτ [(λx.x)y] (Axβη) (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y], rρ[y] NJ(β) rρ[y] (Ax) y = βη (λx.x)y (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y], rρ[y] NJ(β) rρ[(λx.x)y] (Axβη) (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y], rρ[y] NJ(β) rτ [(λx.x)y] ∧ rρ[(λx.x)y] (∧I) (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y], rρ[y] NJ(β) rσ[(λx.x)y] ∨ (rτ [(λx.x)y] ∧ rρ[(λx.x)y]) (∨I)
and D 5 is:

(rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y] NJ(β) (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]) (Ax) (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]), rτ [y] NJ(β) rσ[y] ∨ rρ[y] (∧E)
and D 6 is:

(rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]) NJ(β) (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]) (Ax) (rσ[y] ∨ rτ [y]) ∧ (rσ[y] ∨ rρ[y]) NJ(β) rσ[y] ∨ rτ [y] (∧E)
Chapter 5

Subtyping algorithm

This chapter presents a subtyping algorithm for a type system with intersection, union and the universal type U. In the literature, there is already a subtyping algorithm for intersection types with U [54], but without union types. The correction and completeness of such an algorithm is not trivial, even though it is a crucial part of the proof of the decidability of type reconstruction and type checking. Modern theorem provers such as Coq allow us to design and certify such algorithms1 . We have designed and certified on paper an algorithm that I have thereafter certified in Coq, in the spirit of Bessai's Coq implementation of the subtyping algorithm without unions [START_REF] Bessai | Extracting a formally verified Subtyping Algorithm for Intersection Types from Ideals and Filters[END_REF]. The full source code of the Coq implementation can be found at https://github.com/cstolze/Bull-Subtyping. The certification of the algorithm occurs in two steps:

1. first, we define the subtyping relation and prove some basic properties; 2. then we implement the subtyping algorithm and show it is sound and complete w.r.t.

the subtyping relation.

This chapter is organized as follows: in Section 5.1, we shortly present the subtyping algorithm. In Section 5.2, we explain the details of the Coq implementation of the theory. In Section 5.3, we show the implementation of the subtyping algorithm in Coq and show the intricacies of certified programming. In Section 5.4, we show how to extract the Coq code into valid OCaml code. In Section 5.5, we detail the preorder tactic we have developed in order to ease the certification of the subtyping algorithm.

The algorithm, shortly explained

The types have the following BNF syntax:

σ, τ, ρ ::= α | σ ∩ σ | σ ∪ σ | σ → σ | U
Subtyping is defined as the theory Ξ from [7], as recalled in Figure 5.1. The subtyping algorithm rewrites the types in some normal form, then proceeds on the syntactical structure of these normal forms. We thus define the Arrow Normal Form (ANF) as follows : -it is a type variable;

σ σ ∩ σ (1) σ 1 σ 2 τ 1 τ 2 σ 1 ∪ τ 1 σ 2 ∪ τ 2 (8) σ ∪ σ σ (2) σ τ τ ρ σ ρ (9) i ∈ {1, 2} σ 1 ∩ σ 2 σ i (3) σ ∩ (τ ∪ ρ) (σ ∩ τ ) ∪ (σ ∩ ρ) (10) i ∈ {1, 2} σ i σ 1 ∪ σ 2 (4) (σ → τ ) ∩ (σ → ρ) σ → (τ ∩ ρ) (11) σ U (5) (σ → ρ) ∩ (τ → ρ) (σ ∪ τ ) → ρ (12) σ σ (6) U U → U ( 13
)
σ 1 σ 2 τ 1 τ 2 σ 1 ∩ τ 1 σ 2 ∩ τ 2 (7) σ 2 σ 1 τ 1 τ 2 σ 1 → τ 1 σ 2 → τ 2 (14)
-it is a type σ → τ , where σ is an intersection of ANFs (or U) and τ is an union of ANFs.

Note that U is not an ANF.

Definition 5.2 (CANF and DANF).

These normal forms are similar to the usual Conjunctive and Disjunctive Normal Forms (CNF and DNF) found in boolean algebras.

-An intersection of unions of ANFs is called a Conjunctive Arrow Normal Form (CANF);

-An union of intersections of ANFs is called a Disjunctive Arrow Normal Form (DANF).

The type U is considered to be a CANF and a DANF.

We use four rewriting subroutines, R 1 , R 2 , R 3 , and R 4 , in order to rewrite types in normal form. The first routine R 1 removes all useless occurrences of U.

Definition 5.3. (Subroutine R 1 )
The term rewriting system R 1 (called deleteOmega in the Coq code) is defined as follows:

-U ∩ σ and σ ∩ U rewrite to σ;

-U ∪ σ and σ ∪ U rewrite to U;

-σ → U rewrites to U.
It is easy to verify that R 1 terminates and his complexity is linear. The subroutines R 2 and R 3 rewrite a term in conjunctive and disjunctive normal form, respectively. Definition 5.4. (Subroutines R 2 and R 3 ) -The term rewriting system R 2 rewrites a type in its CNF; it is defined as follows:

-σ ∪ (τ ∩ ρ) rewrites to (σ ∪ τ ) ∩ (σ ∪ ρ); -(σ ∩ τ ) ∪ ρ rewrites to (σ ∪ ρ) ∩ (τ ∪ ρ);
-The term rewriting system R 3 rewrites a type in its DNF; it is defined as follows:

-σ ∩ (τ ∪ ρ) rewrites to (σ ∩ τ ) ∪ (σ ∩ ρ); -(σ ∪ τ ) ∩ ρ rewrites to (σ ∩ ρ) ∪ (τ ∪ ρ).
It is well-known that R 2 and R 3 terminate and that the complexity of those algorithms is exponential.

Subroutine R 4 rewrites a type as an intersection of ANFs.

Definition 5.5. (Subroutine R 4 ) The term rewriting system R 4 rewrites an arrow type into an intersection of ANFs, it is defined as follows:

-

σ → τ rewrites to R 3 (σ) → R 2 (τ ); -∪ i σ i → ∩ h τ h rewrites to ∩ i (∩ h (σ i → τ h )).
Since R 2 and R 3 terminate, it follows that R 4 terminates and its complexity is exponential. Note that in the Coq implementation, we found it easier to directly write functions that rewrite terms in CANF and DANF (these are respectively called _CANF and _DANF).

We could finally introduce the main algorithm A as follows:

Definition 5.

(Algorithm A)

The main algorithm A takes as inputs two types σ in DANF and τ in CANF, and decides whether σ τ by structural induction as follows:

-if σ and τ are two type variables α and β, then σ τ if, and only if, α ≡ β; -for all other cases, σ τ .

-if τ ≡ U, then σ τ ; -if σ ≡ U and τ ≡ U, then σ τ ; -if σ ≡ σ 1 ∪ σ 2 ,
The next section gives a short explanation of the proof of soundness and correctness of the algorithm, which has been formally implemented in Coq.

Soundness and correctness of the algorithm

Lemma 5.1. For all the term rewriting systems R 1,2,3,4 we have that R(σ) ∼ σ.

Proof. Each rewriting rule rewrites a term into an equivalent (∼) term.

The previous lemma has been also proved in Coq using a strong specification. A strong specification is a type that fully specify the desired behavior of a function. For instance, the function deleteOmega will have type ∀ σ : term, {τ | τ ∼ σ ∧ (Omega_free τ ∨ τ = U)}, which means that deleteOmega (i.e. R 1 ) takes as input an expression σ, and return an expression τ such that τ ∼ σ and τ has the property Omega_free τ ∨ τ = U, which means there are no useless occurrences of U inside τ .

Lemma 5.2.

1. σ ∪ τ ρ iff σ ρ and τ ρ;

2. σ τ ∩ ρ iff σ τ and σ ρ.

Proof. The two parts can be proved by examining the subtyping rules of the type theory Ξ.

Lemma 5.3. If all the σ i and τ j are ANFs, then:

1. If ∃j, ∩ i σ i τ j , then ∩ i σ i ∪ j τ j ; 2. If ∃i, σ i ∪τ j , then ∩ i σ i ∪ j τ j .
Proof. The two parts can be proved by induction on the subtyping rules of the type theory Ξ using the ANF definition.

Lemma 5.3 is quite complicated to encode in Coq: we have chosen to define filters (i.e. a set of all the types bigger than a given type) for intersection of ANFs, and ideals (i.e. a set of all the types smaller than a given type) for union of ANFs, then we prove that the definition of filters and ideals are sound and complete w.r.t. subtyping. You can see the previous lemma as the interesting part of the completeness proof of ideals and filters. The soundness and completeness proofs are then straightforward.

Theorem 5.4 (Soundness of A).

Let σ (resp. τ ) be in DANF (resp. CANF). If A(σ, τ ), then σ τ .

Proof. The proof follows the algorithm, therefore it proceeds by structural induction, using Lemmas 5.2 and 5.3.

Theorem 5.5 (Completeness of A).

Let σ (resp. τ ) be in DANF (resp. CANF), such that σ τ . We have that A(σ, τ ).

Proof. The proof proceeds by mutual induction, using Lemmas 5.2 and 5.3.

Soundness and completess of A (called main_algo in the Coq source) is mechanically proven through strong specification. The function main_algo takes as input two types σ and τ , a proof that σ is in DANF and τ in CANF, and returns either a proof that σ τ , or a proof that σ τ .

Coq implementation of the theory Ξ

This section documents the Coq implementation of the theory Ξ, as well as the the important lemmas used to certify the subtyping algorithm. We start with the parameter module, which contains the alphabet of variables, is called V, and has two important fields:

-V.t, which is the type of variables;

-eq_dec, which is a proof that equality is decidable.

The types for which we define a subtyping algorithm only have atoms, arrows, intersections, union, and the universal type U. The syntax of types is defined using a simple inductive type:

Inductive term : Set := | Var : V.t -> term | Arrow : term -> term -> term | Inter : term -> term -> term | Union : term -> term -> term | Omega : term.
Infix "→ " := (Arrow) (at level 60, right associativity). Notation "(→ )" := Arrow (only parsing).

Infix "∩ " := (Inter) (at level 35, right associativity). Notation "(∩ )" := (Inter) (only parsing).

Infix "∪ " := (Union) (at level 30, right associativity). Notation "(∪ )" := (Union) (only parsing). Notation "'U'" := (Omega).

The subtyping relation is the theory Ξ defined in [7], and is defined inductively in Coq as follows:

Inductive Subtype : term -> term -> Prop := | R_InterMeetLeft : ∀ σ τ , σ ∩ τ σ | R_InterMeetRight : ∀ σ τ , σ ∩ τ τ | R_InterIdem : ∀ τ , τ τ ∩ τ | R_UnionMeetLeft : ∀ σ τ , σ σ ∪ τ | R_UnionMeetRight : ∀ σ τ , τ σ ∪ τ | R_UnionIdem : ∀ τ , τ ∪ τ τ | R_InterDistrib : ∀ σ τ ρ, (σ → ρ) ∩ (σ → τ ) σ → ρ ∩ τ | R_UnionDistrib : ∀ σ τ ρ, (σ → ρ) ∩ (τ → ρ) σ ∪ τ → ρ | R_InterSubtyDistrib: ∀ σ σ' τ τ ', σ σ' -> τ τ ' -> σ ∩ τ σ' ∩ τ ' | R_UnionSubtyDistrib: ∀ σ σ' τ τ ', σ σ' -> τ τ ' -> σ ∪ τ σ' ∪ τ ' | R_InterUnionDistrib: ∀ σ τ ρ, σ ∩ (τ ∪ ρ) (σ ∩ τ ) ∪ (σ ∩ ρ) | R_CoContra : ∀ σ σ' τ τ ', σ σ' -> τ τ ' -> σ' → τ σ → τ ' | R_OmegaTop : ∀ σ, σ U | R_OmegaArrow : U U → U | R_Reflexive : ∀ σ, σ σ | R_Transitive : ∀ σ τ ρ, σ τ -> τ ρ -> σ ρ
where "σ τ " := (Subtype σ τ ). Notation "( )" := (Subtype) (only parsing).

We say that two types σ and τ are equivalent if they are subtype of one another:

Definition equiv (σ τ : term) : Prop := (σ τ ) ∧ (τ σ). Notation "σ ∼ τ " := (equiv σ τ ).

The subtyping relation is obviously a preorder relation, thanks to the R_Reflexive and

R_Transitive rules. There are special Coq tactics, such as the reflexivity tactic, for reflexive relations, or transitivity for transitive relations, and we have defined a tactic for dealing with preorders (see Section 5.5). In order to use these tactics, Coq has to know our subtyping relation has the corresponding properties, and to do so we use Coq typeclasses: Coq has an automatic proof search engine. We can declare which theorems, or constructors the search engine can use on its own, the art is to guide it so the proofs are concise, and the engine does not take too much time. These declarations are called hints, and are stored in a hint database. For instance, the following code creates a hint database SubtypeHints, which contains all the subtyping rules, and also allows the unfolding of the definition of the equivalence relation:

Create HintDb SubtypeHints. Hint Constructors Subtype : SubtypeHints. Hint Unfold equiv : SubtypeHints.

The proof that the equivalence relation is reflexive is then trivial, and can be added to the hint database:

Instance equiv_Reflexive: Reflexive (∼ ).

Proof. auto with SubtypeHints. Qed. Hint Immediate equiv_Reflexive : SubtypeHints.

Then we can prove simple facts on the subtyping relation, then add these facts to the hint database when it is clear they make any proof progress:

Fact Inter_inf : ∀ σ τ ρ, σ τ -> σ ρ -> σ τ ∩ ρ.
Proof with auto with SubtypeHints.

intros. transitivity (σ ∩ σ)... Qed. Hint Resolve Inter_inf : SubtypeHints.

However, the converse of Inter_inf, called Inter_inf', should not be added to the hint database, or else the search engine would uselessly loop by applying Inter_inf and then

Inter_inf': Fact Inter_inf' : ∀ σ τ ρ, σ τ ∩ ρ -> (σ τ ) ∧ (σ ρ).
Proof with auto with SubtypeHints. intros; split; etransitivity; try eassumption... Qed.

The search engine can automatically simplify hypotheses if we told it so. For instance, if we know that σ τ ∩ ρ, then we know automatically that σ τ and σ ρ. We can tell that to the search engine like this:

Hint Extern 1 (_ _) ⇒ lazymatch goal with | H : ?σ ?τ ∩ ?ρ |-_ ⇒ apply Inter_inf' in H; destruct H end : SubtypeHints.

The search engine gives a weight to each action in its search, so Hint Extern 1 (_ _) states that this hint weighs 1 and should be used when we have to prove a subtyping relation.

Definition of normal forms

In order to talk about arbitrary intersection (or unions) of ANFs in Coq, we define the type Generalize: Inductive Generalize (c : term -> term -> term) (P : term -> Prop) : term -> Prop := | G_nil : ∀ σ, P σ -> Generalize c P σ | G_cons : ∀ σ τ , Generalize c P σ -> Generalize c P τ -> Generalize c P (c σ τ ). Hint Constructors Generalize : SubtypeHints. Notation "[ P ]" := (Generalize (∩ ) P). Notation "[ P ]" := (Generalize (∪ ) P).

Hence, the concept of ANF can easily be declared in Coq:

Inductive ANF : term -> Prop := | VarisANF : ∀ α, ANF (Var α) | ArrowisANF : ∀ σ τ , [ ANF] σ -> [ ANF] τ -> ANF (σ → τ ) | ArrowisANF' : ∀ τ , [ ANF] τ -> ANF (U → τ ).
Hint Constructors ANF : SubtypeHints.

We define Conjunctive Arrow Normal Forms (CANF) and Disjunctive Arrow Normal Forms (DANF):

Definition CANF (σ : term) :

Prop := [ [ ANF]] σ ∨ σ = U. Definition DANF (σ : term) : Prop := [ [ ANF]] σ ∨ σ = U.
Hint Unfold CANF : SubtypeHints. Hint Unfold DANF : SubtypeHints.

It is clear from the Coq definition that a term is in CANF if it is the intersection of unions of ANFs (or the type U), and that a term is in DANF if it is the union of intersection of ANFs (or the type U). We also define quasi-U-free types (or Omega_free is the Coq source), which are types where there is no useless occurrence of U, i.e. the only accepted occurrences are lone occurrences of U on the left-hand side of an arrow.

Inductive Omega_free : term -> Prop := | Of_Var : ∀ α, Omega_free (Var α) | Of_Union : ∀ σ τ , Omega_free σ -> Omega_free τ -> Omega_free (σ ∪ τ ) | Of_Inter : ∀ σ τ , Omega_free σ -> Omega_free τ -> Omega_free (σ ∩ τ ) | Of_Arrow1 : ∀ σ, Omega_free σ -> Omega_free (U → σ) | Of_Arrow2 : ∀ σ τ , Omega_free σ -> Omega_free τ -> Omega_free (σ → τ ).
Hint Constructors Omega_free : SubtypeHints.

Of course, we can automatically decompose hypotheses stating that some non-atomic type is quasi-U-free, and the hypothesis that U is quasi-U-free is automatically absurd:

| F_Refl : ∀ σ : term, isFilter σ -> ↑[σ] σ | F_Inter : ∀ σ τ ρ : term, ↑[σ] τ -> ↑[σ] ρ -> ↑[σ] τ ∩ ρ | F_Union1 : ∀ σ τ ρ : term, ↑[σ] τ -> ↑[σ] τ ∪ ρ | F_Union2 : ∀ σ τ ρ : term, ↑[σ] ρ -> ↑[σ] τ ∪ ρ | F_Arrow1 : ∀ σ1 σ2 τ 1 τ 2 : term, σ2 σ1 -> τ 1 τ 2 -> ↑[σ1 → τ 1] σ2 → τ 2 | F_Arrow2 : ∀ σ1 σ2 τ 1 τ 2 ρ1 ρ2 : term, ↑[σ1 ∩ σ2] τ 1 → ρ1 -> τ 2 τ 1 -> ρ1 ρ2 -> ↑[σ1 ∩ σ2] τ 2 → ρ2 | F_OmegaTopV : ∀ (α : V.t) (τ : term), ↑[U] τ -> ↑[Var α] τ | F_OmegaTopA : ∀ σ1 σ2 τ : term, ↑[U] τ -> ↑[σ1 → σ2] τ | F_OmegaTopI : ∀ σ1 σ2 τ : term, isFilter (σ1 ∩ σ2) -> ↑[U] τ -> ↑[σ1 ∩ σ2] τ | F_Omega : ∀ σ τ : term, ↑[U] τ -> ↑[U] σ → τ | F_Inter1 : ∀ σ1 σ2 τ : term, isFilter σ2 -> ↑[σ1] τ -> ↑[σ1 ∩ σ2] τ | F_Inter2 : ∀ σ1 σ2 τ : term, isFilter σ1 -> ↑[σ2] τ -> ↑[σ1 ∩ σ2] τ | F_ArrowInter : ∀ σ1 σ2 τ ρ1 ρ2 : term, ↑[σ1 ∩ σ2] (τ → ρ1) ∩ (τ → ρ2) -> ↑[σ1 ∩ σ2] τ → ρ1 ∩ ρ2 | F_ArrowUnion : ∀ σ1 σ2 τ 1 τ 2 ρ : term, ↑[σ1 ∩ σ2] (τ 1 → ρ) ∩ (τ 2 → ρ) -> ↑[σ1 ∩ σ2] τ 1 ∪ τ 2 → ρ where "↑[σ ] τ " := (Filter σ τ ). Hint Constructors Filter : SubtypeHints. Inductive Ideal : term -> term -> Prop := | I_Refl : ∀ σ : term, [ ANF] σ -> ↓[σ] σ | I_Inter1 : ∀ σ τ ρ : term, ↓[σ] τ -> ↓[σ] τ ∩ ρ | I_Inter2 : ∀ σ τ ρ : term, ↓[σ] ρ -> ↓[σ] τ ∩ ρ | I_Union : ∀ σ τ ρ : term, ↓[σ] τ -> ↓[σ] ρ -> ↓[σ] τ ∪ ρ | I_Arrow1 : ∀ σ1 σ2 τ 1 τ 2 : term, [ ANF] σ1 -> ↑[σ1] σ2 -> ↓[τ 1] τ 2 -> ↓[σ1 → τ 1] σ2 → τ 2 | I_Arrow2 : ∀ σ τ 1 τ 2 : term, ↑[U] σ -> ↓[τ 1] τ 2 -> ↓[U → τ 1] σ → τ 2 | I_Union1 : ∀ σ1 σ2 τ : term, [ ANF] σ2 -> ↓[σ1] τ -> ↓[σ1 ∪ σ2] τ | I_Union2 : ∀ σ1 σ2 τ : term, [ ANF] σ1 -> ↓[σ2] τ -> ↓[σ1 ∪ σ2] τ
where "↓ [σ ] τ " := (Ideal σ τ ). Hint Constructors Ideal : SubtypeHints.

Induction scheme for filters and ideals

When we reason about a filter ↑ [σ], we usually do an induction on the predicate isFilter σ, so that we only consider the case where σ is syntactically a type for which we have defined filters. Coq usually automatically generates an induction scheme for declared inductive types. For isFilter, the induction scheme would be:

isFilter_ind : ∀ P : term -> Prop, P U -> (∀ α : V.t, P (Var α)) -> (∀ σ τ : term, P (σ → τ )) -> (∀ σ τ : term, isFilter σ -> P σ -> isFilter τ -> P τ -> P (σ ∩ τ )) -> ∀ σ : term, isFilter σ -> P σ.
However, this induction scheme has a small problem. If we want to prove P σ with the hypothesis H1 : ↑[σ] τ , we can deduce that σ verify the property isFilter σ, therefore we do an induction on this predicate, as there are four constructors, we get four subcases. The problem arises in the second subcase:

-the first case is OmegaisFilter: we have to prove P U under the hypothesis H1 : ↑[U] τ ;

-the second case is VarisFilter: we have to prove P (Var α under the hypothesis H1 : ↑[Var α] τ . Here we can apply the tactic inversion H1, which generate as many subcases as there are possible constructors for H1. Among these constructors, there is

F_OmegaTopV : ∀ (α : V.t) (τ : term), ↑[U] τ -> ↑[Var α] τ
, in which case the hypothesis H1 becomes H1 : ↑[U] τ . From the case OmegaisFilter, we know that P U, but Coq has not remembered it. In order not to rewrite the proof of P U, It would be natural to consider that P U is a kind of induction hypothesis.

Coq allows us to define our own induction scheme for isFilter, by preventing it from automatically generate the induction scheme2 , and by proving a lemma having the name isFilter_ind.

Lemma isFilter_ind :

∀ P : term -> Prop, P U -> (∀ α : V.t, P U -> P (Var α)) -> (∀ σ τ : term, P U -> P (σ → τ )) -> (∀ σ τ : term, isFilter σ -> P σ -> isFilter τ -> P τ -> P U -> P (σ ∩ τ )) -> ∀ σ : term, isFilter σ -> P σ.
Ideals are defined for unions of ANFs, which is, per se, not an inductive type, but we may want nonetheless to have an induction scheme for it:

Lemma Uanf_ind : ∀ P : term -> Prop, (∀ α, P (Var α)) -> (∀ σ τ , P σ -> P τ -> P (σ ∪ τ )) -> (∀ σ τ , P τ -> P (σ → τ )) -> (∀ σ, [ ANF] σ -> P σ).
However, the induction tactic will not call the Uanf_ind lemma, because the type Uanf does not exist. We bypass this issue with a handmade tactic which has approximately the same behavior:

:= distrArrow σ2 τ _ _ in exist _ (σ1 ∩ σ2) _ | _ ⇒ λ _, (fix distrArrow' σ τ (pfσ:[ ANF] σ ∨ σ = U) (pfτ :[ [ ANF]] τ ) : {σ' | σ' ∼ σ → τ ∧ [ ANF] σ'} := match τ as x return τ = x -> _ with | τ 1 ∩ τ 2 ⇒ λ _, let (τ 1,pfτ 1) := distrArrow' σ τ 1 _ _ in let (τ 2,pfτ 2) := distrArrow' σ τ 2 _ _ in exist _ (τ 1 ∩ τ 2) _ | _ ⇒ λ _, exist _ (σ → τ ) _ end eq_refl) σ τ _ pfτ end eq_refl); subst; (destruct pfσ; [|try discriminate]); simpl in * ; auto with SubtypeHints. Defined. Fixpoint distrUnion (σ τ : term) (pfσ : [ [ ANF]] σ) (pfτ : [ [ ANF]] τ ) : {σ' | σ' ∼ σ ∪ τ ∧ [ [ ANF]] σ'}. refine(match σ as x return σ = x -> _ with | σ1 ∩ σ2 ⇒ λ _, let (σ1,pfσ1) := distrUnion σ1 τ _ _ in let (σ2,pfσ2) := distrUnion σ2 τ _ _ in exist _ (σ1 ∩ σ2) _ | _ ⇒ λ _, (fix distrUnion' σ τ (pfσ:[ ANF] σ) (pfτ :[ [ ANF]] τ ) : {σ' | σ' ∼ σ ∪ τ ∧ [ [ ANF]] σ'} := match τ as x return τ = x -> _ with | τ 1 ∩ τ 2 ⇒ λ _, let (τ 1,pfτ 1) := distrUnion' σ τ 1 _ _ in let (τ 2,pfτ 2) := distrUnion' σ τ 2 _ _ in exist _ (τ 1 ∩ τ 2) _ | _ ⇒ λ _, exist _ (σ ∪ τ ) _ end eq_refl) σ τ _ pfτ end eq_refl); subst; simpl in * ; auto with SubtypeHints. Defined. Fixpoint distrInter (σ τ : term) (pfσ : [ [ ANF]] σ) (pfτ : [ [ ANF]] τ ) : {σ' | σ' ∼ σ ∩ τ ∧ [ [ ANF]] σ'}. refine(match σ as x return σ = x -> _ with | σ1 ∪ σ2 ⇒ λ _, let (σ1,pfσ1) := distrInter σ1 τ _ _ in let (σ2,pfσ2) := distrInter σ2 τ _ _ in exist _ (σ1 ∪ σ2) _ | _ ⇒ λ _, (fix distrInter' σ τ (pfσ:[ ANF] σ) (pfτ :[ [ ANF]] τ ) : {σ' | σ' ∼ σ ∩ τ ∧ [ [ ANF]] σ'} := match τ as x return τ = x -> _ with | τ 1 ∪ τ 2 ⇒ λ _, let (τ 1,pfτ 1) := distrInter' σ τ 1 _ _ in let (τ 2,pfτ 2) := distrInter' σ τ 2 _ _ in exist _ (τ 1 ∪ τ 2) _ | _ ⇒ λ _, exist _ (σ ∩ τ ) _ end eq_refl) σ τ _
pfτ end eq_refl); subst; simpl in * ; auto with SubtypeHints. Defined. Now, we can implement the functions that rewrite a term in CANF or DANF. These functions are mutually recursive:

Fixpoint _CANF (σ : term) : (Omega_free σ ∨ σ = U) -> {τ | τ ∼ σ ∧ CANF τ } with _DANF (σ : term) : (Omega_free σ ∨ σ = U) -> {τ | τ ∼ σ ∧ DANF τ }. Proof.
refine(match σ with The algorithm A (called main_algo in the Coq source) is difficult to implement: recursive functions in Coq may call themselves recursively only if some argument is structurally decreasing, but this has to be the same argument for every recursive call. However, in this algorithm either the first or the second argument decreases during a recursive call.

| Var α ⇒ λ _, exist _ (Var α) _ | σ → τ ⇒ λ pf, let (σ,pfσ) := _DANF σ _ in let (τ ,pfτ ) := _CANF τ _ in let (σ',pfσ') := distrArrow σ τ _ _ in exist _ σ' _ | σ ∩ τ ⇒ λ pf, let (σ,pfσ) := _CANF σ _ in let (τ ,pfτ ) := _CANF τ _ in exist _ (σ ∩ τ ) _ | σ ∪ τ ⇒ λ pf, let (σ,pfσ) := _CANF σ _ in let (τ ,pfτ ) := _CANF τ _ in let (σ',pfσ') := distrUnion σ τ _ _ in exist _ σ' _ | U ⇒ λ _, exist _ U _ end); try (destruct pf; [|discriminate]); simpl in * ; match goal with | |-_ ∨ _ ⇒ auto with SubtypeHints | |-_ ∧ _ ⇒ split; [trivial|] | _ ⇒
| Var α ⇒ λ _, exist _ (Var α) _ | σ → τ ⇒ λ pf, let (σ,pfσ) := _DANF σ _ in let (τ ,pfτ ) := _CANF τ _ in let (σ',pfσ') := distrArrow σ τ _ _ in exist _ σ' _ | σ ∪ τ ⇒ λ pf, let (σ,pfσ) := _DANF σ _ in let (τ ,pfτ ) := _DANF τ _ in exist _ (σ ∪ τ ) _ | σ ∩ τ ⇒ λ pf, let (σ,pfσ) := _DANF σ _ in let (τ ,pfτ ) := _DANF τ _ in let (σ',pfσ') := distrInter σ τ _ _ in exist _ σ' _ | U ⇒ λ _, exist _ U _ end); try (destruct pf; [|discriminate]); simpl in * ; match goal with | |-_ ∨ _ ⇒ auto with SubtypeHints | |-_ ∧ _ ⇒ split; [trivial|] | _ ⇒
The usual workaround is to add an extra argument to the function that will structurally decrease. Hopefully, the Coq standard library has some functions already implemented to help us. We define a measure on the types, and prove this measure cannot infinitely decrease: The final part is straightforward: we compose the previous algorithms without any difficulty:

| |-_ _ ∩ _ ⇒ auto with SubtypeHints | |-_ ∪ _ _ ⇒ auto with SubtypeHints | |-_ ∩ _ _ ⇒ apply Inter_inf_dual; auto | |-_ _ ∪ _ ⇒ apply Union_sup_dual; auto | |-_ → _ _ → _ ⇒

Extracting the subtyping algorithm in OCaml

The extraction system of Coq is rather straightforward. We can replace the default extraction of inductive types with the Extract Inductive command. For instance, the Coq cartesian product prod can be replaced with the OCaml product. Non-inductive terms can be instantiated with Extract Constant. For instance, eq_dec, which is an uninstantiated parameter in the source code, can be instantiated with the OCaml equality function. Moreover, there is no need to explicitly create a function eq_dec in OCaml, so we can tell Coq to inline it, with Extraction Inline BDdL.eq_dec. Here is the full ExtractOcaml.v source file:

Require Import Filter. Require Extraction.

Module BDdL := VariableAlphabet <+ Types.

Extract Inductive prod ⇒ "(*)" [ "(,)" ]. Extract Constant fst ⇒ "fst". Extract Constant snd ⇒ "snd". Extract Inductive sumbool ⇒ "bool" [ "true" "false" ]. Extract Inductive sig ⇒ "" [ "" ]. Extract Constant BDdL.t ⇒ "int". Extract Constant BDdL.eq_dec ⇒ "(fun x y -> x = y)". Extraction Inline BDdL.eq_dec. Extraction Language Ocaml. Extraction "BDdL.ml" BDdL.SubtypeRelation.

The preorder tactic

We explain how we have implemented a heuristic tactic solving automatically goals involving preorders. The tactic proceeds by reflection, mainly using techniques given in [START_REF] Chlipala | Certified Programming with Dependent Types -A Pragmatic Introduction to the Coq Proof Assistant[END_REF]. Reflection has two components:

-Reification: the goal is converted into a data structure. This component is done with the Ltac language of Coq;

-Denotation: the data structure is converted back into a goal. This component is done with the Gallina language of Coq.

The denotation of the reification of a goal should be the original goal itself. In our case, we have a tactic quote_formula which change the goal into a term denote_formula R c f, where R is the preorder relation, f is the reification of the goal, and c is a vector which helps reconstruct the original goal. A function preorder_heuristic processes recursively the argument f and returns either a proof of denote_formula R c f or nothing. Then the preorder tactic:

Ltac preorder := intros; match goal with | |-?R _ _ ⇒ quote_formula R; match goal with | |-denote_formula R ?c ?f ⇒ exact (partialOut (preorder_heuristic _ c f)) end | _ ⇒ fail "preorder tactic unsuccessful" end.

Denotation

Let's assume we have a preorder relation <, some terms t 1 , . . . , t n , u 1 , . . . , u n and a goal of the form:

Γ;

H 1 : t 1 < u 1 ; H 2 : t 2 < u 2 t n < u n
The goal may have extra hypotheses that are irrelevant. The goal is then transformed into:

Γ t 1 < u 1 → t 2 < u 2 → . . . → t n < u n
We then store all the t i and u i in a vector (i.e. a sized list) v of size n, and reify the following formula as a list of pairs of indices:

t 1 < u 1 → t 2 < u 2 → . . . → t n < u n
The indices are the position of the terms in v. With the vector v and the list of pairs of indices, we can reconstruct the original formula. We need to easily get a term in the vector from an index, but we don't want any undefined behavior in case the index is out-of-bound. Therefore, we implement vectors the following way:

Inductive vector (A : Type) : nat -> Type := | vnil : vector A 0 | vcons : forall n : nat, A -> vector A n -> vector A (S n).
An index is a natural number m along with a proof that m is smaller than the size of the vector.

Definition index (n : nat) := {m : nat | m < n}.
We consider that two indices are equivalent if they correspond to the same natural number:

Definition index_to_nat {n : nat} (i : index n) : nat := match i with | exist _ i _ ⇒ i end.
(* Decidable proof-irrelevant equality for indexes *) Definition index_eq {n : nat} (i j : index n) := index_to_nat i = index_to_nat j.

Local Notation "i == j" := (index_eq i j) (at level 70). Definition index_eq_dec {n : nat} : forall i j : index n, {i == j} + {~i == j}. Proof. intros; unfold index_eq. decide equality. Defined.

The function _get takes as input a vector v of size n, an natural number i and a proof that i < n, and returns the element of the vector at position n.

Fixpoint _get {A : Type} {n : nat} (v :

vector A n) {i : nat} {struct v} : i < n -> A. refine (match v in vector _ n' return i < n' -> A with | vnil _ ⇒ fun p : i < 0 ⇒ _ | vcons x v' ⇒ match i as x return x < _ -> A with | 0 ⇒ fun _ ⇒ x | S j ⇒ fun p : _ ⇒ _get A _ v' j _ end end).
The refiner manages to fill all the wildcards, except two of them, which become goals we have to solve on our own:

-case vnil _, where the vector is empty: since we have a proof p : i < 0, we can conclude by contradiction;

-case S j, where the vector is not empty and we do not want the element at position 0: this is the recursive case, but we need an arithmetical proof that the updated index is still valid.

These two logical steps are done interactively using Ltac:

exfalso; inversion p.

apply Lt.lt_S_n; assumption. Defined.

Now we can write a simple and safe function get, such that get v i returns the term at index i in the vector v:

Definition get {A : Type} {n : nat} (v :

vector A n) (i : index n) : A := match i with | exist _ _ p ⇒ _get v p end.
Of course, if two indices i and j are equivalent, then for any vector v, get v i = get v j:

Lemma get_irrelevant : forall A n (v : vector A n) (i j : index n), i == j -> get v i = get v j.
A formula is reified as a list of pairs of indices for the hypotheses, along with a pair of indices for the conclusion:

Definition formula (n : nat) :

Set := (list (index n * index n)) * (index n * index n).
The denotation of a formula is straightforward: we get back every term and reconstruct the original formula.

Definition denote_formula {n : nat} (v :

vector A n) (f : formula n) : Prop := match f with | (l, (i, j)) ⇒ (fix loop l := match l with | nil ⇒ get v i < get v j | cons (i,j) l' ⇒ get v i < get v j -> loop l' end) l end.

Implementation of the heuristic function

As the heuristic function returns either a proof or nothing, we need a type [ A] which intuitively means "either a proof of A or nothing" and a function partialOut to extract the proof. The function partialOut cannot have type ∀ A : Prop, [ A] -> A, because a proof of A may not exist, so partialOut returns a proof of True if we don't have any proof of A. The following helper lemma allows us to partially denote a formula, which is very useful before using an induction hypothesis:

Lemma denote_cons : forall n (v: vector _ n) i j l a b, denote_formula v (cons (i,j) l, (a,b)) = (get v i < get v j -> denote_formula v (l,(a,b))).
Before giving the implementation of preorder_heuristic, we present its behaviour: if we want to prove that a < b under the list of hypotheses l, we examine three cases:

1. there is no hypothesis: a < b if, and only if, a and b are the same indices, and we conclude by reflexivity of the preorder;

2. the first hypothesis is useless: we can try to conclude by induction on the list of hypotheses, by simply discarding the first hypothesis;

3. the first two cases do not apply: the first hypothesis is i < j, so we can try to prove by induction on the list of hypotheses that a < i and j < b, then we conclude by transitivity. The transitivity property is given by the following lemma:

Lemma denote_trans : forall {n} {v : vector _ n} {l x} y {z}, denote_formula v (l,(x,y)) -> denote_formula v (l,(y,z)) -> denote_formula v (l,(x,z)).

We also need to prove that i < j by hypothesis:

Lemma denote_hyp : forall n (v : vector _ n) l a b, get v a < get v b -> denote_formula v (l,(a,b)).
The function preorder_heuristic computes a result (Yes or No), which contains a proof. As usual, the computational part is given by the refine tactic: apply (denote_trans i); trivial. apply (denote_trans j); trivial. apply denote_hyp; trivial. Defined.

Definition preorder_heuristic : forall (n : nat) (v : vector A n) (f : formula n), [ denote_formula v f ]. intros ? ? [l (

Reification

Now that we know how to solve reified goals, we only need to write tactics that automatically reify them. We need tactics to create the vector. We want to avoid duplicates, so we have a tactic that check if a term x is already in the vector v:

Ltac is_in_vector x v := lazymatch v with | vnil _ ⇒ false | vcons x _ ⇒ true | vcons _ ?v' ⇒ is_in_vector x v' end.
We can see that Ltac's pattern-matching acts in a different way than Gallina's patternmatching. There are three kinds of terms in Coq: Gallina's pattern-matching only matches linear patterns on inductive structures, and it silently performs computations on terms. Ltac's pattern-matching matches arbitrary Gallina terms. Moreover, the patternmatching is first-order 3 , which means that it does not apply any conversion rule: for instance, one can match 1 + _ with 1 + 1, but one cannot match 1 + 1 with 2 or 2 with 1 + 1. There is also a difference between variables and meta-variables. For instance, in the code of is_in_vector:

-in the pattern vcons x _, the variable x is the substitution of the first argument of the tactic, it only matches something which is syntactically the same term;

-in the pattern vcons _ ?v', the meta-variable ?v' can match anything, and then Ltac instantiate a new variable v' on the right-hand-side of the match clause.

In short, the tactic is_in_vector x v checks if the term x is syntactically a subterm of v.

It does not care whether there is a term which is computationally convertible to x. We now can implement a function that add a term in a vector without doing any duplication:

Ltac add_in_vector x v := lazymatch is_in_vector x v with | true ⇒ v | false ⇒ constr:(vcons x v) end.
In the code above, the badly documented "constr:" keyword is needed because Ltac is implemented in such a way that a tactic vcons can coexist with a Gallina term vcons (these two terms would be stored in two different namespaces in the Coq internals 4 ). When we apply vcons, we have to explicitly state it lies in the constr namespace.

For getting the position of a term in a vector, we also need a tactic:

Ltac lookup_vector x v := lazymatch v with | vcons x _ ⇒ O | vcons _ ?v' ⇒ let n := lookup_vector x v' in constr:(S n) end.
However, this tactic does return a natural number, we need a proof that this natural number is not out-of-bound. We use the function lt_dec to do so, and we have to explicitly tell Ltac to evaluate the function, using the eval tactic:

Ltac nat_to_index i n := (* lt_dec: forall n m : nat, {n < m} + {~n < m} *) lazymatch eval lazy in (lt_dec i n) with | left _ ?p ⇒ constr:(exist (fun x ⇒ x < n) i p) end.
We can create the vector and the formula corresponding to the reification of the goal: Chapter 6

Dependent types

This chapter provides a unifying framework for two hitherto unreconciled understandings of types: i.e. types-as-predicates à la Curry and types-as-propositions à la Church. The key to our unification consists in introducing strong proof-functional connectives [START_REF] Pottinger | A type assignment for the strongly normalizable λ-terms[END_REF]7,8] in a dependent type theory such as the Edinburgh Logical Framework (LF) [START_REF] Harper | A framework for defining logics[END_REF]. Both Logical Frameworks and Proof-Functional Logic consider proofs as first-class citizens, albeit differently.

Strong proof-functional connectives take seriously into account the shape of logical proofs, thus allowing for polymorphic features of proofs to be made explicit in formulae. Hence they provide a finer semantics than classical/intuitionistic connectives, where the meaning of a compound formula depends only on the truth value or the provability of its subformulae. However, existing approaches to strong proof-functional connectives are all quite idiosyncratic in mentioning proofs. Existing Logical Frameworks, on the other hand, provide a uniform approach to proof terms in object logics, but they do not fully capitalize on subtyping.

This situation calls for a natural combination of the two understandings of types, which should benefit both worlds. On the side of Logical Frameworks, the expressive power of the metalanguage would be enhanced thus allowing for shallower encodings of logics, a more principled use of subtypes [START_REF] Pfenning | Refinement types for logical frameworks[END_REF], and new possibilities for formal reasoning in existing interactive theorem provers. On the side of type disciplines for programming languages, a principled framework for proofs would be provided, thus supporting a uniform approach to "proof reuse" practices based on type theory [START_REF] Di | Isomorphisms of types: from λ-calculus to information retrieval and language design[END_REF][START_REF] Pierce | Programming with intersection types, union types, and bounded polymorphism[END_REF][START_REF] Caplan | A logical framework for software proof reuse[END_REF][START_REF] Felty | Generalization and reuse of tactic proofs[END_REF][START_REF] Boite | Proof reuse with extended inductive types[END_REF].

Therefore, in this chapter, we extend LF with the connectives of strong intersection (corresponding to the intersection type), strong union (corresponding to the union type), and minimal relevant implication of Proof-Functional Logic [START_REF] Pottinger | A type assignment for the strongly normalizable λ-terms[END_REF]8]. We call this extension the ∆-framework (LF ∆ ), since it builds on the ∆-calculus [START_REF] Liquori | The Delta-calculus: Syntax and types[END_REF]. Moreover, we illustrate by way of examples, that LF ∆ subsumes many expressive type disciplines in the literature [START_REF] Pfenning | Refinement types for logical frameworks[END_REF]7,8,[START_REF] Pierce | Programming with intersection types, union types, and bounded polymorphism[END_REF][START_REF] Caplan | A logical framework for software proof reuse[END_REF].

It is not immediate to extend the Curry-Howard isomorphism to logics supporting strong proof-functional connectives, since these connectives need to compare the shapes of derivations and do not just take into account the provability of propositions, i.e. the inhabitation of the corresponding type. In order to capture successfully strong logical connectives such as ∩ or ∪, we need to be able to express the rules:

D 1 : A D 2 : B D 1 ≡ D 2 A ∩ B (∩I) D 1 : A ⊃ C D 2 : B ⊃ C A ∪ B D 1 ≡ D 2 C (∪E)
where ≡ is a suitable equivalence between logical proofs. Notice that the above rules suggest immediately intriguing applications in polymorphic constructions, i.e. the same evidence can be used as a proof for different statements.

Pottinger [START_REF] Pottinger | A type assignment for the strongly normalizable λ-terms[END_REF] was the first to study the strong connective ∩. He contrasted it to the intuitionistic connective ∧ as follows: "The intuitive meaning of ∩ can be explained by saying that to assert A ∩ B is to assert that one has a reason for asserting A which is also a reason for asserting B [while] to assert A ∧ B is to assert that one has a pair of reasons, the first of which is a reason for asserting A and the second of which is a reason for asserting B".

A logical theorem involving intuitionistic conjunction which does not hold for strong conjunction is (A ⊃ A) ∧ (A ⊃ B ⊃ A), otherwise there should exist a closed λ-term having simultaneously both one and two abstractions. López-Escobar [START_REF] Edgar | Proof functional connectives[END_REF] and Mints [START_REF] Mints | The completeness of provable realizability[END_REF] investigated extensively logics featuring both strong and intuitionistic connectives especially in the context of realizability interpretations.

Dually, it is in the ∪-elimination rule that proof equality needs to be checked. Following Pottinger, we could say that asserting (A ∪ B) ⊃ C is to assert that one has a reason for (A ∪ B) ⊃ C, which is also a reason to assert A ⊃ C and B ⊃ C. The two connectives differ since the intuitionistic theorem ((A ⊃ B) ∨ B) ⊃ A ⊃ B is not derivable for ∪, otherwise there would exist a term which behaves both as I and as K.

Following Barbanera and Martini [8], minimal relevant implication, denoted by ⊃ r , can be viewed as a special case of implication whose related function space is the simplest possible one, namely the one containing only the identity function. The operators ⊃ and ⊃ r differ, since A ⊃ r B ⊃ r A is not derivable. Relevant implication allows for a natural introduction of subtyping, in that A ⊃ r B morally means A B. Relevant implication amounts to a notion of "proof-reuse". Combining the remarks in [8,7], minimal relevant implication, strong intersection and strong union correspond respectively to the implication, conjunction and disjunction operators of Meyer and Routley's Minimal Relevant Logic B + [START_REF] Meyer | Algebraic analysis of entailment I[END_REF]. A terminological comment is in order. We refer to (⊃ r ) as relevant implication in order to be faithful to the original logical literature, since this constructor satisfies the logical properties of implication in the minimal relevant logical system introduced in [START_REF] Meyer | Algebraic analysis of entailment I[END_REF]. And precisely in this sense it was used later in [8]. This use of the word "relevant" is therefore more constrained than, but not totally unrelated to, the one arising in the context of λI-calculus and linear logic, where it expresses the requirement that the variable "is used at least once" in the function, in contrast to affine "at most one use" and linear "exactly one use".

Strong connectives arise naturally in investigating the propositions-as-types analogy for intersection and union type assignment systems. From a logical point of view, there are many proposals to find a suitable logic to fit intersection: among them we cite [START_REF] Mints | The completeness of provable realizability[END_REF][START_REF] Pfenning | Refinement types for logical frameworks[END_REF][START_REF] Venneri | Intersection types as logical formulae[END_REF][START_REF] Ronchi | Intersection logic[END_REF][START_REF] Miquel | The implicit calculus of constructions[END_REF][START_REF] Capitani | Hyperformulae, Parallel Deductions and Intersection Types[END_REF][START_REF] Bono | A typed lambda calculus with intersection types[END_REF][START_REF] Pimentel | Intersection types from a proof-theoretic perspective[END_REF].

The LF ∆ logical framework introduced in this chapter extends [START_REF] Liquori | The Delta-calculus: Syntax and types[END_REF] with union types, dependent types and minimal relevant implication. The novelty of LF ∆ in the context of Logical Frameworks, lies in the full-fledged use of strong proof-functional connectives, which to our knowledge has never been explored before. Clearly, all ∆-terms have a computational counterpart.

Pfenning's work on Refinement Types [START_REF] Pfenning | Refinement types for logical frameworks[END_REF] pioneered an extension of the Edinburgh Logical Framework with subtyping and intersection types. His approach capitalizes on an interesting and essentially ad hoc notion of subtyping. However, subtyping in LF ∆ arises naturally as a derived notion from the more fundamental concept of minimal relevant Chapter 7 and Bull and Bull-Subtyping in [START_REF] Stolze | [END_REF]). This chapter is organized as follows: in Section 6.1, we introduce LF ∆ . In Section 6.2 we outline its metatheory, together with a discussion of the main design decisions. In Section 6.3, we discuss the relation between subtyping and the relevant arrow operator. In Section 6.4, we give a Pure Type System presentation of LF ∆ . In Section 6.5, we outline the future work.

∆• r ∆ | relevant application ∆, ∆ | intersection objects [∆, ∆] | union objects pr 1 ∆ | pr 2 ∆ | projections objects in σ 1 ∆ | in σ 2 ∆ injections objects

The ∆-framework: LF with proof-functional operators

The syntax of LF ∆ pseudo-terms is given in Figure 6.2. For the sake of simplicity, we suppose that α-convertible terms are equal. Signatures and contexts are defined as finite sequence of declarations, like in LF. Observe that we could formulate LF ∆ in the style of [START_REF] Harper | Mechanizing metatheory in a logical framework[END_REF], using only canonical forms and without reductions, but we prefer to use the standard LF format to support better intuition. There are three proof-functional objects, namely strong conjunction (typed with σ ∩ τ ) with two corresponding projections, strong disjunction (typed with σ ∪ τ ) with two corresponding injections, and strong (or relevant) λ-abstraction (typed with → r ). Indeed, a relevant implication is not a dependent one because the essence of the inhabitants of type σ → r τ is essentially the identity function as enforced in the typing rules. Note that injections in i need to be decorated with the One could argue that the choice of ∆ 1 in the definition of strong pairs/sums is arbitrary and could have been replaced with ∆ 2 : however, the typing rules will ensure that, if

∆ 1 , ∆ 2 def = ∆ 1 λ r x:σ.∆ def = λx. ∆ λx:σ.∆ def = λx. ∆ [∆ 1 , ∆ 2 ] def = ∆ 1 ∆ 1 ∆ 2 def = ∆ 1 ∆ 2 ∆ 1 • r ∆ 2 def = ∆ 2 pr i ∆ def = ∆ in σ i ∆ def = ∆ c def = c x def = x
(λx:σ.∆ 1 ) ∆ 2 -→ β ∆ 1 [∆ 2 /x] pr 1 ∆ 1 , ∆ 2 -→ pr 1 ∆ 1 pr 2 ∆ 1 , ∆ 2 -→ pr 2 ∆ 2 [∆ 1 , ∆ 2 ] in σ 1 ∆ 3 -→ in 1 ∆ 1 ∆ 3 [∆ 1 , ∆ 2 ] in σ 2 ∆ 3 -→ in 2 ∆ 2 ∆ 3 (λ r x:σ.∆ 1 )• r ∆ 2 -→ βr ∆ 1 [∆ 2 /x] ∆ 1 → ∆ ∆ 1 ∆ 2 → ∆ ∆ 2 ∆ 1 = η ∆ 2 ∆ 1 , ∆ 2 → ∆ ∆ 1 , ∆ 2 (Congr ∩ ) ∆ 1 → ∆ ∆ 1 ∆ 2 → ∆ ∆ 2 ∆ 1 = η ∆ 2 [∆ 1 , ∆ 2 ] → ∆ [∆ 1 , ∆ 2 ] (Congr ∪ )
∆ 1 , ∆ 2 (resp. [∆ 1 , ∆ 2 ]
) is typable, then we have that ∆ 1 = η ∆ 2 . Thus, strong pairs/sums are constrained. The rule for the essence of a relevant application is justified by the fact that the operator amounts to just a type decoration.

The six basic reductions for LF ∆ objects appear in Figure 6.4. Congruence rules are as usual, except for the two cases dealing with strong pairs and sums. Here redexes need to be reduced "in parallel" in order to preserve identity of essences in the components. We denote by = ∆ the symmetric, reflexive, and transitive closure of → ∆ , i.e. the compatible closure of the reduction induced by the first six rules, with the addition of the last two congruence rules in the same figure. In order to make this definition truly functional as well as to be able to prove a simple subject reduction result, we need to constrain strong pairs and sums, i.e. objects of the form ∆ i , ∆ j and [∆ i , ∆ j ] to have congruent components up-to erasure of type annotations. This is achieved by imposing ∆ i = η ∆ j in both constructs. We do not consider the relations because they are undecidable. We will therefore assume that such strong pairs and sums are simply not well defined terms, if the components have a different "infrastructure". The effects of this choice are reflected in the congruence rules in the reduction relation, in order to ensure that reductions can only be carried out in parallel along the two components.

∆ i = β ∆ j or ∆ i = βη ∆ j Valid Signatures • sig ( Σ) Σ sig Σ K a ∈ Dom(Σ) Σ, a:K sig (KΣ) Σ sig Σ σ : Type c ∈ Dom(Σ) Σ, c:σ sig (σΣ) Valid Contexts Σ sig Σ • ( Γ) Σ Γ Γ Σ σ : Type x ∈ Dom(Γ) Σ Γ, x:σ (σΓ)
The restriction on reductions in strong pairs/sums and the new constructs do not cause any problems in showing that → ∆ is confluent: Theorem 6.1 (Confluence). LF ∆ is confluent, i.e.:

1. If K 1 -→ * ∆ K 2 and K 1 -→ * ∆ K 3 , then ∃K 4 such that K 2 -→ * ∆ K 4 and K 3 -→ * ∆ K 4 ; 2. If σ 1 -→ * ∆ σ 2 and σ 1 -→ * ∆ σ 3 , then ∃σ 4 such that σ 2 -→ * ∆ σ 4 and σ 3 -→ * ∆ σ 4 ; 3. If ∆ 1 -→ * ∆ ∆ 2 and ∆ 1 -→ * ∆ ∆ 3 , then ∃∆ 4 such that ∆ 2 -→ * ∆ ∆ 4 and ∆ 3 -→ * ∆ ∆ 4 .
Proof. Using the same technique as in Theorem 2.19.

The extended type theory LF ∆ is a formal system for deriving judgments of the forms: The set of rules for object formation is defined in Figure 6.7, while the sets of rules for signatures, contexts, kinds and families are defined as in [START_REF] Harper | A framework for defining logics[END_REF], and all typing rules (except the (Conv) rules) are syntax-directed. Note that proof-functionality is enforced by the essence side-conditions in rules (→ r I), (∩I), and (∪E).

Σ Σ is a valid signature Σ Γ Γ is a valid context in Σ Γ Σ K K is a kind in Γ
In the rule (Conv) we rely on the external notion of equality = ∆ . An option could have be to add an internal notion of equality directly in the type system (Γ Σ σ = ∆ τ ), and prove that the external and the internal definitions of equality are equivalent, as was proved for semi-full Pure Type Systems [START_REF] Siles | Equality is typable in semi-full pure type systems[END_REF]. Yet another possibility could be to compare type essences σ = ∆ τ , for a suitable extension of essence to types and kinds. Unfortunately, this would lead to undecidability of type checking, in connection with relevant implication, as the following example shows. Consider two constants c 1 of type σ → r (Πy:σ.σ) and c 2 of type (Πy:σ.σ) → r σ: the ∆-term in Figure 6.8 is typable

∆ Ω def = (λx:σ.c 1 • r x x) (c 2 • r (λx:σ.c 1 • r x x))
∆ Ω ≡ Ω x (y z) (y z), Figure 6.9: Pierce's one-step reduction counter-example as those that equate σ and σ → σ. As a consequence, β-equality of essences becomes undecidable. Thus, we rule out such options in relating relevant implications in LF ∆ to subtypes in the type assignment system λ BDdL of [7].

Relating LF ∆ to λ BDdL

We compare and contrast certain design decisions of LF ∆ to the type assignment system λ BDdL of [7]. The proof of strong normalization for LF ∆ will rely, in fact, on a forgetful mapping from LF ∆ to λ BDdL . As pointed out in [7], the elimination rule for union types in λ BDdL breaks subject reduction for one-step β-reduction, but this can be recovered using a suitable parallel β-reduction. The well-known counter-example for one-step reduction, due to Pierce, is in Figure 6.9 (where I is the identity).

In the typing context

B def = x:(σ 1 → σ 1 → τ ) ∩ (σ 2 → σ 2 → τ ), y:ρ → (σ 1 ∪ σ 2
), z:ρ, the first and the last terms can be typed with τ , while the terms in the fork cannot. The reason is that the subject in the conclusion of the (∪E) rule uses a context which can have more than one hole, as in the present case. It is interesting to note that the problem would not arise if (∪E) is replaced by the following rule schema:

Γ, x 1 :σ, . . . , x n :σ M : ρ Γ, x 1 :τ, . . . , x n :τ M : ρ Γ N i : σ ∪ τ N i = β N j i, j = 1 . . . n Γ M [N 1 /x 1 , . . . , N n /x n ] : ρ (∪E )
However, removing the non-static clause on the N i 's would yield a more permissive type system than λ BDdL .

In LF ∆ , the formulation of the (∪E) rule takes a different route which does not trigger the counterexample. Indeed, we have introduction and elimination constructs in 1 , in 2 and [-, -] which allow to reduce the term only if we know that the argument, stripped of the introduction construct, has one of the types of the disjunction. Pierce's counter-example can be expressed and typed in LF ∆ with the following judgment (the full derivation is in Subsection 6.2.1): We recall the following result, proved in [7], will be useful in the following section. The following lemmas are proved by straightforward structural induction, and using Lemma 6.5. Lemma 6.6.

Γ Σ [(λx 1 :σ 1 .(pr 1 x) x 1 x 1 ) ∆ 1 , (λx 2 :σ 2 .(pr 2 x) x 2 x 2 ) ∆ 2 ] ( (λx 3 :ρ → σ 1 ∪ σ 2 .x 3 )
|| Type || = (a special constant) || σ → r τ || = || σ ||→|| τ || || Πx:σ.K || = || σ ||→|| K || || σ ∆ || = || σ || || a || = a || σ ∩ τ || = || σ || ∩ || τ || || Πx:σ.τ || = || σ ||→|| τ || || σ ∪ τ || = || σ || ∪ || τ || | a | = a | σ → r τ | = c × | σ | | τ | | c | = c | σ ∩ τ | = c × | σ | | τ | | x | = x | σ ∪ τ | = c × | σ | | τ | | σ ∆ | = | σ | | ∆ | | ∆ 1 , ∆ 2 | = | ∆ 1 | | ∆ 1 ∆ 2 | = | ∆ 1 | | ∆ 2 | | [∆ 1 , ∆ 2 ] | = | ∆ 1 | | ∆ 1 • r ∆ 2 | = | ∆ 1 | | ∆ 2 | | λx:σ.∆ | = (λy.λx. | ∆ |) | σ | y ∈ Fv(∆) | pr 1 ∆ | = | ∆ | | λ r x:σ.∆ | = (λy.λx. | ∆ |) | σ | y ∈ Fv(∆) | pr 2 ∆ | = | ∆ | | in σ 1 ∆ | = (λx. | ∆ |) | σ | x ∈ Fv(∆) | Πx:σ.τ | = c ||σ|| | σ | (λx. | τ |) | in σ 2 ∆ | = (λx. | ∆ |) | σ | x ∈ Fv(∆)
1. If σ = ∆ τ , then || σ ||= β || τ ||; 2. If K 1 = ∆ K 2 , then || K 1 ||= β || K 2 ||. Lemma 6.7. 1. | ∆ 1 [∆ 2 /x] |= β | ∆ 1 | [| ∆ 2 | /x]; 2. | σ[∆/x] |= β | σ | [| ∆ | /x]. Lemma 6.8. 1. If Γ Σ σ : K, then || Γ || λ BDdL + | σ | : || K ||; 2. If Γ Σ ∆ : σ, then || Γ || λ BDdL + | ∆ | : || σ ||.
where λ BDdL + denotes the type system λ BDdL , augmented by c × : → → and the infinite set of axioms c ||σ|| : → (|| σ ||→ ) → , for each type σ.

Proof. By induction on the derivation, using Lemmas 6.6 and 6.7

Notice that the functionand | -| treat relevant implication differently. Lemma 6.9.

12. If Γ Σ in σ 2 ∆ : σ ∪ τ , then Γ Σ ∆ : τ and Γ Σ σ ∪ τ : Type. The following technical lemma will be useful to prove subject reduction. Lemma 6.12 (Subderivation). 6. Given a derivation of the judgment Γ Σ α, and a subterm occurring in the subject of this judgment, there exists a derivation of a judgment having this subterm as a subject.

Subject reduction can be proved by easy induction on the structure of the derivations. Finally, we can prove decidability of all the judgments of LF ∆ .

Theorem 6.14 (Decidability). All the type judgments of LF ∆ are recursively decidable.

Proof. We can easily check judgments in LF ∆ : because of Theorem 6.10 and because all the rules (except (Conv)) are syntax directed, we can compute a type or a kind for a term, and then test for definitional equality, i.e. = ∆ , against the given type or kind; this is achieved by reducing both to their unique normal forms, and, thanks to the confluence property (Theorem 6.1), we only have to check if the normal forms are syntactically equal.

Minimal relevant implications and type inclusion

Type inclusion and the rules of subtyping are related to the notion of minimal relevant implication, see [8,[START_REF] Daniel | A realizability interpretation for intersection and union types[END_REF]. The insight is quite subtle, but ultimately very simple. This is what makes it appealing. The apparently intricate rules of subtyping and type inclusion, which occur in many systems, and might even appear ad hoc at times, can all be explained away in our principled approach, by proving that the relevant implication type is inhabited by a term whose essence is essentially a variable.

In the following theorem we show how relevant implication subsumes the type-inclusion rules of the theory Ξ of [7], without rules ( 5) and ( 13) (dealing with U) and rule (10) (distributing ∩ over ∪) in Figure 6.1: we call Ξ such restricted type theory. Note that the reason to drop subtype rule (10) is due to the fact that we cannot inhabit the type Proof.

σ ∩ (τ ∪ ρ) → r (σ ∩ τ ) ∪ (σ ∩ ρ). (1) σ σ ∩ σ ∆ def = ∆, ∆ (2) σ ∪ σ σ ∆ def = [λx:σ.x, λx:σ.x] ∆ (3) σ 1 ∩ σ 2 σ i ∆ def = pr i ∆ (4) σ i σ 1 ∪ σ 2 ∆ def = in i ∆ (6) σ σ ∆ def = ∆ (7) σ 1 σ 2 τ 1 τ 2 σ 1 ∩ τ 1 σ 2 ∩ τ 2 ∆ def = σ 1 σ 2 (pr 1 ∆) , τ 1 τ 2 (pr 2 ∆) (8) σ 1 σ 2 τ 1 τ 2 σ 1 ∪ τ 1 σ 2 ∪ τ 2 ∆ def = [λx:σ 1 .in τ 2 1 σ 1 σ 2 x , λx:τ 1 .in σ 2 2 τ 1 τ 2 x ] ∆ (9) σ τ τ ρ σ ρ ∆ def = τ ρ ( σ τ ∆ ) (11) (σ → τ ) ∩ (σ → ρ) σ → (τ ∩ ρ) ∆ def = λx:σ. (pr 1 ∆) x, (pr 2 ∆) x (12) (σ → ρ) ∩ (τ → ρ) (σ ∪ τ ) → ρ ∆ def = λx:σ ∪ τ.[λy:σ.(pr 1 ∆) y, λy:τ.(pr 2 ∆) y] x (14) σ 2 σ 1 τ 1 τ 2 σ 1 → τ 1 σ 2 → τ 2 ∆ def = λx:σ 2 . τ 1 τ 2 (∆ σ 2 σ 1 x )
(if). Follows directly from Lemma 6.11;

(only if). It is possible to write a ∆-term whose essence is an η-expansion of the identity (λx.x) corresponding to each of the axioms and rules in Ξ . The ∆-term is obtained by defining a function σ τ ∆ , where σ τ is a subtyping derivation tree in the type theory Ξ , which coerce a ∆-term from type σ to type τ , as defined in Figure 6.11.

As far as the λ Π& system of refinement types introduced by Pfenning in [START_REF] Pfenning | Refinement types for logical frameworks[END_REF], we get the following example: Example 6.1 (Pfenning's refinement types [START_REF] Pfenning | Refinement types for logical frameworks[END_REF]). The judgment Σ σ τ in λ Π& can be encoded in LF ∆ by adding a constant of type σ → r τ to Σ , where the latter is the signature obtained from Σ by replacing each clause of the form a 1 :: a 2 or a 1 a 2 in Σ by a constant of type a 1 → r a 2 . Moreover, while Pfenning needs to add explicitly the rules of subtyping (i.e. the theory of ) in λ Π& , we inherit them naturally in LF ∆ from the rules for minimal relevant implication.

Let Γ def = {x 1 :σ 1 , . . . , x n :σ n } (i = j implies x i ≡ x j ), and Γ, x:σ

∆ ::= Type | Kind | c | x | λx:σ.∆ | ∆ ∆ | λ r x:∆.∆ | ∆• r ∆ | ∆, ∆ | [∆, ∆] | pr 1 ∆ | pr 2 ∆ | in ∆ 1 ∆ | in ∆ 2 ∆ | Πx:∆.∆ | ∆ → r ∆ | ∆ ∪ ∆ | ∆ ∩ ∆
We define R def = {(Type, Type), (Type, Kind)}. The typing rules are given in Figures 6.12 and 6.13.

We now define objects, families and kinds in LF PTS ∆ .

Definition 6.2 (Objects, families, and kinds). In a signature Σ, for any ∆:

1. if there is some Γ, σ, such that Γ Σ ∆ : σ and Γ Σ σ : Type, then we say that ∆ is an object in the signature Σ;

2. if there is some Γ, σ, such that Γ Σ ∆ : σ and Γ Σ σ : Kind, then we say that ∆ is a family in the signature Σ;

3. if there is some Γ, such that Γ Σ ∆ : Kind, then we say that ∆ is a kind in the signature Σ.

The next theorem states that all objects, families and kinds in LF ∆ remain respectively well-typed objects, families and kinds in LF PTS ∆ .

Theorem 6.16 (Preservation).

1. for any signature Σ, if Σ sig in LF ∆ , then Σ sig in LF PTS ∆ (assuming the alphabet for atom types and the alphabet for constants are the same); Figure 6.13: Pure Type System presentation of the ∆-framework (terms)

for any context

Γ, if Σ Γ in LF ∆ , then Σ Γ in LF PTS ∆ ; 3. for any kind K, if Γ Σ K in LF ∆ , then Γ Σ K : Kind in LF PTS ∆ ,

Future Work

There is still a lot of research to do in the domain of Church-style λ-calculus with intersection, union, and dependent types. Among some interesting questions, we could mention:

1. LF ∆ in Canonical Form: we presented LF ∆ in the standard LF format in order to support intuition, and in the PTS format for conciseness. It would be worthwhile however, to attempt to formulate LF ∆ in the style of Harper and Licata [START_REF] Harper | Mechanizing metatheory in a logical framework[END_REF], using only canonical forms without reductions, especially in view of proving adequacy results. The terms peculiar to LF ∆ would then introduce new clauses in the definition of canonical and atomic terms. The principle to follow in this task is that atomic terms synthesize their type, while canonical terms are checked against their type. We are currently exploring the following extension:

M ::= . . . | λ r x.M | M, M | [M, M ] | in 1 M | in 2 M R ::= . . . | pr 1 R | pr 2 R | R • r M
Notice the somewhat surprising treatment of the [ , ] constructor, which is not really an elimination construct but rather behaves as another form of abstraction. Accordingly hereditary substitution needs to be extended.

An intriguing issue1 is to explore the connections between strong implication and the singleton type of the identity function. This could lead also to an internalization of the essence function; Chapter 7

Implementation of the theorem prover Bull

This chapter presents the implementation of a prototype of an Interactive Theorem Prover (ITP) based on the ∆-framework. I have personally been writing this theorem prover from scratch for three years, and it is called Bull1 [START_REF] Stolze | Towards a logical framework with intersection and union types[END_REF][START_REF] Stolze | [END_REF]. We have a command-line interface program where the user can declare axioms, terms, and perform computations. These terms can be incomplete, therefore the typechecking algorithm uses unification to try to construct the missing subterms.

In Chapter 5, we have implemented the subtyping algorithm which extends the wellknown algorithm for intersection types, designed by Hindley [START_REF] Hindley | The simple semantics for Coppo-Dezani-Sallé types[END_REF], with union types. The subtyping algorithm has been mechanically proved correct in Coq, extending the mechanized proof of a subtyping algorithm for intersection types of Bessai [START_REF] Bessai | Extracting a formally verified Subtyping Algorithm for Intersection Types from Ideals and Filters[END_REF].

We have implemented several features. A Read-Eval-Print-Loop allows to define axioms and definitions, and performs some basic terminal-style features like error prettyprinting, subexpressions highlighting, and file loading. Moreover, it can typecheck a proof or normalize it. We use the syntax of Pure Type Systems [START_REF] Berardi | Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt's cube[END_REF] to improve the compactness and the modularity of the kernel. Abstract and concrete syntax are mostly aligned: the concrete syntax is similar to the concrete syntax of Coq.

We have designed a higher-order unification algorithm for terms, while typechecking and partial type inference are done by our bidirectional refinement algorithm, similar to the one found in [6]. The refinement can be split into two parts: the essence refinement and the typing refinement. The bidirectional refinement algorithm aims to have partial type inference, and to give as much information as possible to the unifier. For instance, if we want to find a ?y such that Σ λx:σ.x, λx:τ.?y : (σ → σ) ∩ (τ → τ ), we can infer that x:τ ?y : τ and that ?y = β x. This chapter is organized as follows: in Section 7.1, we explain the commonly-used de Bruijn indices. In Section 7.2, we introduce the language we have implemented. In Section 7.3, we define the reduction rules and explain the evaluation process. In Section 7.4, we present the subtyping algorithm. In Section 7.5, we present the unifier. In Section 7.6, we present the refiner which does partial typechecking and type reconstruction. In Section 7.7, we present the Read-Eval-Print-Loop. In Section 7.8, we present possible enhancements of the software.

de Bruijn indices in Bull

In this section, we review the de Bruijn indices technique [START_REF] De Bruijn | Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem[END_REF] as it is implemented in Bull, using the pure λ-calculus for simplicity.

The principle is to replace every variable x is by its de Bruijn index i, which is the number of binders we encounter when traversing the term until we meet the binder of x. Constants c are still allowed, and are not replaced by an integer. We get the following grammar:

M

::= c | i | λx.M | M M
The name x on the binder λx could seem superfluous, but it is convenient if we want to get back the names of the variables. N.G. de Bruijn counts from 1 in his historical paper, but we decided to count from 0 in the Bull implementation. We will use λx.((λy.λz.x y z (λt.y))(λu.x u)) as a running example which is translated as λx.((λy.λz.2 1 0 (λt.2))(λu.1 0)). There is one β-redex, which consist of the function λy.λz.x y z(λt.y) applied to the argument λu.x u. This term reduces to: It is easier to read these terms by looking at their syntax tree, where variables are decorated with their de Bruijn index. Intuitively, we can see the de Bruijn indices as the distance between variables and their binders:

λx λy λz x 2 y 1 z 0 λt y 2 λu x 1 u 0 -→ β λx λz x 1 λu x 2 u 0 z 0 λt λu x 3 u 0
As you can see, β-reduction with de Bruijn indices requires a subtle update of the indices. Simply speaking, the β-reduction algorithm consists of a tree traversal where every de Bruijn index is compared to the depth of the consumed binder (λy in the example):

-if the de Bruijn index is strictly greater than the depth of the consumed binder, it corresponds to a variable bound to a binder above the consumed binder (λx in the example). Therefore this de Bruijn index is decremented;

-if the de Bruijn index is strictly smaller than the depth of the consumed binder, it corresponds to a variable bound to a binder below the consumed binder (λz in the example). Therefore this de Bruijn index is unchanged;

-if the reference binder is the depth of the consumed binder, it corresponds to the variable to be substituted. We replace the node with an updated version of the argument. It has to be computed anew for each replacement (it is done twice in the example), and it is a tree traversal where the de Bruijn indices are modified:

The parser does not compute de Bruijn indices, it gives the variables as strings. The function fix_index replaces bound variables by de Bruijn indices. We still keep track of the string names of the variables, in case we have to print them back. Its converse function, fix_id, replaces the de Bruijn indices with the previous strings, possibly updating the string names in case of name clashes. For instance, the string printed to the user, showing the normalized form of (fun (x y : nat) ⇒ x) y, is fun y0 : nat ⇒ y : the bound variable y has been renamed y0. The meta-variables are generated by the typecheckers, and their identifier is an integer.

We have defined several helper functions to ease the process of terms: there is the most generic function visit_term f g h t, which looks at the children of the term t, and:

1. every child t1 outside of a binder is replaced with f t1;

2. every child t1 inside the binding of a variable whose name (a string) is s is replaced with g s t1, while s is replaced with h s t1. The functions g and h takes a string as an argument, for helping the implementation of the fix_index and fix_id functions.

The function map_term is a kind of mapping function: map_term k f t finds every variable Var(l, n) inside the term, and replaces it by f (k+offset) l n, where offset is the number of extra bindings.

let lift k n = map_term k (fun k l m → if m < k then Var (l, m) else Var (l, m+n))
The lift and map_term functions allow us to define a substitution in a clean way: Var (l, m-1) in map_term 0 subst t1

Environments

There are four kinds of environments, namely 1. the global environment (noted Σ). The global environment holds constants which are fully typechecked:

Σ ::= • | Σ, c:ς@σ | Σ, c := M @∆ : ς@σ
Intuitively, c:ς@σ is a declaration of a constant (or axiom), and c := M @∆ : ς@σ corresponds to a global definition. 3. the essence environment (noted Ψ). It is used for the second step of typechecking, and holds the essence of the local variables:

Ψ ::= • | Ψ, x | Ψ, x := M
Intuitively, x is a variable introduced by a λ-abstraction, and x := M is a local definition introduced by a let. Notice that the variable x in the BNF expression Ψ, x carries almost no information. However, since local variables are referred to by their de Bruijn indices, and these indices are actually their position in the environment, it follows that they have to appear in the environment, even when there is no additional information.

4. the meta-environment (noted Φ). It is used for unification, and records metavariables and their instantiation whenever the unification algorithm has found a solution:

Φ ::= • | Φ, sort(?x) | Φ, ?x := s | Φ, (Γ ?x : σ) | Φ, (Γ ?x := ∆ : σ) | Φ, Ψ ?x | Φ, Ψ ?x := M
Intuitively, since there are some meta-variables for which we know they have to be sorts, it follows that sort(?x) declares a meta-variable ?x which correspond either to Type or Kind, and ?x := s is the instantiation of a sort ?x. Also, Γ ?x : σ is the declaration of a meta-variable ?x of type σ which appeared in a local environment Γ, and Γ ?x := ∆ : σ is the instantiation of the meta-variable ?x. Concerning meta-variables inside essences, Ψ ?x is the declaration of a meta-variable ?x in an essence environment Ψ, and Ψ ?x := M is the instantiation of ?x.

Suspended substitution

We shortly introduce suspended substitution, as presented in [6]. Let's consider the following example: if we want to unify (λx:σ.?y) c 1 with c 1 , we could unify ?y with c 1 or with x, the latter being the preferred solution. However, if we normalize (λx:σ.?y) c 1 , we should record the fact that c 1 can be substituted by any occurrence of x appearing the term to be replaced by ?y. That is the purpose of suspended substitution: the term is actually noted (λx:σ.?y[x]) c 1 and reduces to ?y[c 1 ], noting that c 1 has replaced x.

Definition 7.1 (Type-erase function and suspended substitution).

1. the vector x 1 ; . . . ; x n is created using the type-erase function

The unification algorithm of Bull

Higher-order unification of two terms ∆ 1 and ∆ 2 aims at finding a most general substitution for meta-variables such that ∆ 1 and ∆ 2 becomes convertible. Classical references are the work of Huet [START_REF] Huet | A unification algorithm for typed lambda-calculus[END_REF], and Dowek, Kirchner, and Hardin [START_REF] Dowek | Higher order unification via explicit substitutions[END_REF]. Our higher-order unification algorithm was inspired by the Reed [START_REF] Reed | Higher-order constraint simplification in dependent type theory[END_REF] and Ziliani-Sozeau [START_REF] Ziliani | A unification algorithm for Coq featuring universe polymorphism and overloading[END_REF] papers. In [START_REF] Ziliani | A unification algorithm for Coq featuring universe polymorphism and overloading[END_REF], conversion of terms is quite involved because of the complexity of Coq. For simplicity, our algorithm supposes the terms to be in normal form.

The unification algorithm takes as input a meta-environment Φ, a global environment Σ, a local environment Γ, the two terms to unify ∆ 1 and ∆ 2 , and either fails or returns the updated meta-environment Φ. The structural rules are given in Figure 7.1. The rest of the unification algorithm implements Higher-Order Pattern Unification (HOPU) [START_REF] Reed | Higher-order constraint simplification in dependent type theory[END_REF]. In a nutshell, HOPU takes as an argument a unification problem ?f S ? = N , where all the terms in S are free variables and each variable occurs once. For instance, for the unification problem ?f y x z ? = x c y, it creates the solution ?f := λy:σ 2 .λx:σ 1 .λz:σ 3 .x c y. The expected type of x, y, and z can be found in the local environment, but capturing correctly the free variables x, y, and z is quite tricky because we have to permute their de Bruijn indices. If HOPU does not work, we try to recursively unify every subterm.

The refinement algorithm of Bull

The Bull typechecker was inspired by the work on the Matita ITP [6]. It is defined using bi-directionality, in the style of Harper-Licata [START_REF] Harper | Mechanizing metatheory in a logical framework[END_REF]. The bi-directional technique is a mix of typechecking and type reconstruction, in order to trigger the unification algorithm as soon as possible. Moreover, it gives more precise error messages than standard type reconstruction. For instance, if f : (bool -> nat -> bool) -> bool, then f (fun x y ⇒ y) is ill-typed. With a simple type inference algorithm, we would type f, then fun x y ⇒ y which would be given some type ?x -> ?y -> ?y, and finally we would try to unify bool -> nat -> bool with ?x -> ?y -> ?y, which fails. However, the failure is localized on the application, whereas it would better be localized inside the argument. More precisely, we would have the following error message: f (fun x y ⇒ y)

Êrror: the term "y" has type "nat" while it is expected to have type "bool".

Our typechecker is also a refiner : intuitively, a refiner takes as input an incomplete term, and possibly an incomplete type, and tries to infer as much information as possible in order to reconstruct a well-typed term. For example, let's assume we have in the global environment the following constants:

(eq : nat -> nat -> Type), (eq_refl : forall x : nat, eq x x)

Then refining the term eq_refl _ : eq _ 0 would create the following term: eq_refl 0 : eq 0 0 Refinement also enable untyped abstractions: the refiner may recover the type of bound variables, because untyped abstractions are incomplete terms. The typechecking is done 1. The function reconstruct takes as inputs a meta-environment Φ 1 , a global environment Σ, a local environment Γ, and a term ∆ 1 . It either fails or fills the holes in ∆ 1 , which becomes ∆ 2 , and returns ∆ 2 along with its type σ and the updated meta-environment Φ 2 . The corresponding judgment is the following:

Φ 1 ; Σ; Γ ∆ 1 ⇑ ∆ 2 : σ; Φ 2
The rules are described in Figures 7.2 and 7.3;

2. The function force_type takes as inputs a meta-environment Φ 1 , a global environment Σ, a local environment Γ, and a term σ 1 . It either fails or fills the holes in σ 1 , which becomes σ 2 while ensuring it is a type, i.e. its type is a sort s, and returns σ 2 along with s, and the updated meta-environment Φ 2 . The corresponding judgment is the following:

Φ 1 ; Σ; Γ σ 1 F σ 2 : τ ; Φ 2
The rules are described in Figure 7.4. Intuitively, the function reconstruct the type τ of σ 1 , then tries to unify τ with Type and Kind. If it can only do one unification, it keeps the successful one, if both unifications work, we choose unification with a sort meta-variable, so τ is convertible to a sort;

3. The function reconstruct_with_type takes as inputs a meta-environment Φ 1 , a global environment Σ, a local environment Γ, a term ∆ 1 , and its expected type σ. It either fails or fills the holes in ∆ 1 , which becomes ∆ 2 while ensuring its type is σ, and returns ∆ 2 along the updated meta-environment Φ 2 . The corresponding judgment is the following:

Φ 1 ; Σ; Γ ∆ 1 : σ ⇓ ∆ 2 ; Φ 2
The rules are described in Figure 7.5. There is a rule (Default) which applies only if none of the other rules work. The acute reader could remark two subtle things:

(a) we chose not to add any inference rule for coercions, because we believe it would make error messages clearer: more precisely, if we want to check that coe σ ∆ has type τ , there could be two errors happening concurrently: it is possible that the type of ∆ is not a subtype of σ, and at the same time σ is not unifiable with τ . We think that the error to be reported should be the first one, and in this case the (Default) rule is sufficient;

(b) the management of de Bruijn indices for the (Let) is tricky: if we want to check that let x:σ := ∆ 1 in ∆ 2 has type τ in some local context Γ, we recursively check that ∆ 2 has type τ in the local context Γ, x := ∆ 1 : σ for some ∆ 1 , but the de Bruijn indices for τ correspond to the position of the local variables in the local context, which has been updated. We therefore have to increment all the de Bruijn indices in τ , in order to report the fact that there is one extra element in the local context;

4. The function essence takes as inputs a meta-environment Φ 1 , a global environment Σ, an essence environment Ψ, and a term ∆. It either fails or construct its essence M , and returns M along with the updated meta-environment Φ 2 . The corresponding judgment is the following:

Φ 1 ; Σ; Ψ ∆ E ⇑ M ; Φ 2
3. Relevant arrow, as defined in Chapter 6, could be useful to add more expressivity to our system. Relevant implication allows for a natural introduction of subtyping, in that A ⊃ r B morally means A B. Relevant implication amounts to a notion of "proof-reuse". Combining the remarks in [8,7], minimal relevant implication, strong intersection and strong union correspond respectively to the implication, conjunction and disjunction operators of Meyer and Routley's Minimal Relevant Logic B + [START_REF] Meyer | Algebraic analysis of entailment I[END_REF]. This could lead to some implementation problem, because deciding β-equality for the essences in this extended system would be undecidable (see Figure 6.8);

4. A Tactic language, such as the one of Coq, should be useful. Currently, there is no such tactic language for Bull, conceiving such a language should be feasible even if it would be quite heavy.

= M 2 U Φ 3 Φ 1 ; Σ; Ψ M 1 @∆ E ⇓ Φ 3 (Default) Φ 1 ; Σ; Ψ M @∆ 1 E ⇓ Φ 2 Φ 2 ; Σ; Ψ M @∆ 1 E ⇓ Φ 3 Φ 1 ; Σ; Ψ M @ ∆ 1 , ∆ 2 E ⇓ Φ 3 (Spair ) Φ 1 ; Σ; Ψ M @∆ E ⇓ Φ 2 Φ 1 ; Σ; Ψ M @pr i ∆ E ⇓ Φ 2 (Proj ) Φ 1 ; Σ; Ψ σ E ⇑ ς; Φ 2 Φ 2 ; Σ; Ψ M @∆ E ⇓ ; Φ 3 Φ 1 ; Σ; Ψ M @in i σ ∆ E ⇓ Φ 3 (Inj ) Φ 1 ; Σ; Ψ σ E ⇑ ς; Φ 2 Φ 2 ; Σ; Ψ ∆ 1 E ⇑ M 1 ; Φ 3 Φ 3 ; Σ; Ψ, x := M 1 M @∆ 2 E ⇓ Φ 4 Φ 1 ; Σ; Ψ M @let x:σ := ∆ 1 in ∆ 2 E ⇓ Φ 4 (Let)
Φ 1 ; Σ; Ψ M = β Πx:ς 1 .ς 2 Φ 1 ; Σ; Ψ ς 1 @σ 1 E ⇓ Φ 2 Φ 2 ; Σ; Ψ, x ς 2 @σ 2

E ⇓ Φ 3
Φ 1 ; Σ; Ψ M @Πx:σ 1 .σ 2

E ⇓ Φ 3 (Prod ) Φ 1 ; Σ; Ψ M 1 = β λx.M 2 Φ 1 ; Σ; Ψ, x M 2 @∆ E ⇓ Φ 2 Φ 1 ; Σ; Ψ M 1 @λx:σ.∆ E ⇓ Φ 2 (Abs) Φ 1 ; Σ; Ψ M = β ς 1 ∩ ς 2 Φ 1 ; Σ; Ψ ς 1 @σ 1 E ⇓ Φ 2 Φ 2 ; Σ; Ψ ς 2 @σ 2 E ⇓ Φ 3 Φ 1 ; Σ; Ψ M @σ 1 ∩ σ 2 E ⇓ Φ 3 (∩) Φ 1 ; Σ; Ψ M = β ς 1 ∪ ς 2 Φ 1 ; Σ; Ψ ς 1 @σ 1 E ⇓ Φ 2 Φ 2 ; Σ; Ψ ς 2 @σ 2 E ⇓ Φ 3 Φ 1 ; Σ; Ψ M @σ 1 ∪ σ 2 E ⇓ Φ 3 (∪)

Examples in Bull

The point of this chapter is to give examples which show a uniform and approach to the encoding of a plethora of type disciplines and systems which ultimately stem or can capitalize from strong proof-functional connectives and subtyping. The framework LF ∆ , presented in Chapter 6, is the first to accommodate all the examples and counterexamples that have appeared in the literature. This chapter is organized as follows: in Section 8.1 we present some examples in LF ∆ along with their code in Bull, and in Section 8.2, we show some similar encodings done done in LF1 , in order to emphasize the benefits of LF ∆ . x : s ⇒ inj_r t x , x : t ⇒ inj_l s x end.

Axiom backchain : prog -> atom -> goal -> Type.

(* rules for solve *) Axiom solve_and : forall p g1 g2, solve p g1 -> solve p g2 -> solve p (and_1 g1 g2). Axiom solve_or1 : forall p g1 g2, solve p g1 -> solve p (or_1 g1 g2). Axiom solve_or2 : forall p g1 g2, solve p g2 -> solve p (or_1 g1 g2). Axiom solve_impl : forall p1 p2 g, solve (and_2 p1 p2) g -> solve p1 (impl_1 p2 g). Axiom solve_atom : forall p a g, backchain p a g -> solve p g -> solve p (inj_l non_atomic_goal a).

(* rules for backchain *) Axiom backchain_and1 : forall p1 p2 a g, backchain p1 a g -> backchain (and_2 p1 p2) a g. Axiom backchain_and2 : forall p1 p2 a g, backchain p1 a g -> backchain (and_2 p1 p2) a g. Axiom backchain_impl_atom : forall a g, backchain (impl_2 g (inj_l non_atomic_prog a)) a g. Axiom backchain_impl_impl : forall p a g g1 g2, backchain (impl_2 (and_1 g1 g2) p) a g -> backchain (impl_2 g1 (impl_2 g2 p)) a g. Axiom backchain_impl_and1 : forall p1 p2 a g g1, backchain (impl_2 g1 p1) a g -> backchain (impl_2 g1 (and_2 p1 p2)) a g. Axiom backchain_impl_and2 : forall p1 p2 a g g1, backchain (impl_2 g1 p2) a g -> backchain (impl_2 g1 (and_2 p1 p2)) a g.

Natural deductions in normal form

The second motivating example for intersection types given in [START_REF] Pfenning | Refinement types for logical frameworks[END_REF] is natural deductions in normal form. We recall that a natural deduction is in normal form if there are no applications of elimination rules of a logical connective immediately following their corresponding introduction, in the main branch of a subderivation. The encoding we give in LF ∆ is a slightly improved version of the one in [START_REF] Pfenning | Refinement types for logical frameworks[END_REF]: as Pfenning, we restrict to the purely implicational fragment. As in the previous example, we use union types to define normal forms Nf(A) either as pure elimination-deductions from hypotheses Elim(A) or normal form-deductions Nf 0 (A). As above we could have used also intersection types. This example is interesting in itself, being the prototype of the encoding of type systems using canonical and atomic syntactic categories [START_REF] Harper | Mechanizing metatheory in a logical framework[END_REF] and also of Fitch Set Theory [START_REF] Honsell | Implementing Cantor's paradise[END_REF]. The code of is0test has been generated by an Ltac script, the generated code is too huge to be humanly readable, as you can see in Figure 8.2.

Testdef=Figure 1 . 1 :

 11 Figure 1.1: Pierce's code

Figure 2 . 1 :

 21 Figure 2.1: Minimal type theory min , axioms and rule schemes (from Figure 13.2 and 13.3 of [12])

Figure 2 . 6 :

 26 Figure 2.6: The ∆-chair

T=

  β λx:τ.x : τ → τ T = β (λx:τ →τ.x) (λx:τ.x) : τ → τ λx.x = β (λx.x) (λx.x) T = β λx:σ.x, (λx:τ →τ.x) (λx:τ.x) : (σ → σ) ∩ (τ → τ ) Example 2.6 (Two examples in ∆ BCD ≡ and ∆ BCD = βη ). In λ BCD

  and the underlinings of M are also found in N ; 3. If |M | ≡ |N |, we note M N for the λ-term whose underlinings are the union of those from M and N . Thus M N is the least upper-bound for the relation.

  and we pose N def = (λx.N ) N .

CHAPTER 2 .

 2 A TYPED CALCULUS WITH INTERSECTION TYPES Definition 2.16 (Forgetful mapping).

3 .

 3 by induction on the context of the redex; 4. by induction on the derivation. s Strong normalization follows easily from the above lemmas.

Theorem 2 . 21 (

 221 Strong normalization).If Γ T R ∆ : σ, then ∆ is strongly normalizing.

  Figure 2.1.

Example 2 . 9 (

 29 Translation of axioms and rule schemes of Figure 2.1).

Definition 2 .

 2 18 (Translationsand -Γ ).

1 .

 1 The minimal type theory min and the extra axioms and schemes are translated as follows:

Figure 2 . 7 :

 27 Figure 2.7: On the left: source systems. On the right: target systems without the ( T ) rule

Theorem 2 .

 2 26 (Coherence). If Γ T R ∆ : σ, then Γ T R ∆ Γ : σ and ∆ Γ R ∆ , where ∆ T R and ∆ T R are respectively the source and target intersection typed systems given in Figure 2.7.

Figure 3 . 1 :

 31 Figure 3.1: Intersection and union type assignment system λ BDdL [7]

Figure 4 . 1 :

 41 Figure 4.1: The logic NJ(β)

Lemma 4 . 1 (

 41 Admissibility of (Eqβ) in NJ(β)).The following rule is admissible in NJ(β):

Figure 5 . 1 :

 51 Figure 5.1:The type theory Ξ of[7]

  Instance Subtypes_Reflexive : Reflexive ( ) := R_Reflexive. Instance Subtypes_Transitive : Transitive ( ) := R_Transitive. Instance Subtypes_Preorder : PreOrder ( ) := {| PreOrder_Reflexive := Subtypes_Reflexive; PreOrder_Transitive := Subtypes_Transitive |}.

(

  * measure on the types *) Fixpoint size (σ : term) : nat := match σ with | Var α ⇒ 0 | σ → τ ⇒ S((size σ) + (size τ )) | σ ∩ τ ⇒ S((size σ) + (size τ )) | σ ∪ τ ⇒ S((size σ) + (size τ )) | U ⇒ 0 end. Definition pair_size (x : term * term) : nat := let (s,t) := x in size s + size t. (* Well-founded principle for the main algorithm *) Definition main_algo_order : relation (term * term) := | |-main_algo_order _ _ ⇒ red; simpl; omega | |-?σ ?σ ⇒ reflexivity | H : ?x |-?x ⇒ assumption | |-CANF _ ⇒ auto with SubtypeHints | |-DANF _ ⇒ auto with SubtypeHints (* Correctness *) | |-_ U ⇒ auto with SubtypeHints

  Definition decide_subtype : ∀ σ τ , {σ τ } + {¬ σ τ }. Proof. intros. refine (let (σ1,pfσ) := deleteOmega σ in let (Hσ1,pfσ) := pfσ in let (τ 1,pfτ ) := deleteOmega τ in let (Hτ 1,pfτ ) := pfτ in let (σ2,pfσ) := _DANF σ1 pfσ in let (Hσ2,pfσ) := pfσ in let (τ 2,pfτ ) := _CANF τ 1 pfτ in let (Hτ 2,pfτ ) := pfτ in match main_algo (σ2,τ 2) pfσ pfτ with | left H ⇒ left _ | right H ⇒ right _ end); rewrite ← Hτ 1, ← Hσ1, ← Hτ 2, ← Hσ2; assumption. Defined.

  Inductive partial {A : Prop} : Set := | Yes : A -> partial | No : partial. Local Notation "[ A ]" := (@partial A). Definition partialOut {A : Prop} (p : [A]) : match p with | Yes _ ⇒ A | No ⇒ True end := match p with | Yes p ⇒ p | No ⇒ I end. Lemma denote_hyp : forall n (v : vector _ n) l a b, get v a < get v b -> denote_formula v (l,(a,b)).

  a, b)]; generalize a b; clear a b. (* Induction on the number of hypotheses *) induction l as [|(i,j) l is_less]; intros a b. -(* 1. Case with no hypothesis: a < b if a == b (same index) *) refine (if (index_eq_dec a b) then Yes _ else No); simpl. erewrite get_irrelevant; [reflexivity | assumption]. -(* 2. Inductive case: either induction or transitivity through the new hypothesis *) rewrite denote_cons. refine (match (is_less a b) with | Yes _ ⇒ Yes _ (* 3. Transitive case *) | No ⇒ match (is_less a i) with | Yes _ ⇒ match (is_less j b) with | Yes _ ⇒ Yes _ | No ⇒ No end | No ⇒ No end end); trivial; intros.

  Ltac create_vector R e := lazymatch e with | R ?x ?y -> ?e' ⇒ let v' := create_vector R e' in add_in_vector x ltac:(add_in_vector y v') | R ?x ?y ⇒ add_in_vector x constr:(vcons y (vnil _)) end. Ltac create_formula R e v := let n := lazymatch type of v with | vector _ ?n ⇒ n end in lazymatch e with | R ?x ?y -> ?e' ⇒ let x := nat_to_index ltac:(lookup_vector x v) n in let y := nat_to_index ltac:(lookup_vector y v) n in let f := create_formula R e' v in match f with | pair ?l ?h ⇒ constr:((cons (x,y) l, h)) end | R ?x ?y ⇒ let x := nat_to_index ltac:(lookup_vector x v) n in let y := nat_to_index ltac:(lookup_vector y v) n in constr:((@nil (index n * index n),(x,y))) end. The tactic quote_formula reify the goal, and does the appropriate change: Ltac quote_formula R := repeat lazymatch goal with | H : R _ _ |-_ ⇒ revert H end; lazymatch goal with | |-?e ⇒ let v := create_vector R e in let f := create_formula R e v in change (denote_formula R v f) end.

KindsK

  ::= Type | Πx:σ.K as in LF Families σ, τ ::= a | Πx:σ.τ | σ ∆ | as in LF σ → r τ | relevant family σ ∩ τ | intersection family σ ∪ τ union family Objects ∆ ::= c | x | λx:σ.∆ | ∆ ∆ | as in LF λ r x:σ.∆ | relevant abstraction

Figure 6 . 2 :

 62 Figure 6.2: The syntax of the ∆-framework

Figure 6 . 3 :

 63 Figure 6.3: The extended essence function

Figure 6 . 4 :

 64 Figure 6.4: The reduction semantics

Figure 6 . 5 :

 65 Figure 6.5: Valid signatures and contexts

  and Σ Γ Σ σ : K σ has kind K in Γ and Σ Γ Σ ∆ : σ ∆ has type σ in Γ and Σ Let Figure 6.5 denote Valid Signatures and Contexts and Figure 6.6 denote Valid Kinds and Families.

Figure 6 . 8 :

 68 Figure 6.8: Encoding of Ω

∆ 3 y

 3 z) : τ where Γ def = x:(Πx 1 :σ 1 .Πx 2 :σ 1 .τ ) ∩ (Πx 1 :σ 2 .Πx 2 :σ 2 .τ ), y:ρ → σ 1 ∪ σ 2 , z:ρ, and Σ def = τ :Type. Notice that there is only one redex, namely ∆ 3 y, and the reduction of this redex leads to [∆ 1 , ∆ 2 ] (y z), and no other intermediate (untypable) ∆-terms are possible.

Figure 6 . 10 :

 610 Figure 6.10: The forgetful mappings || -|| and | -|

1 .

 1 A derivation of Σ • has a subderivation of Σ sig; 2. A derivation of Σ, a:K sig has subderivations of Σ sig and Σ K; 3. A derivation of Σ, f :σ sig has subderivations of Σ sig and Σ σ:Type; 4. A derivation of Σ Γ, x:σ has subderivations of Σ sig, Σ Γ, and Γ Σ σ:Type; 5. A derivation of Γ Σ α has subderivations of Σ sig and Σ Γ;

Theorem 6 . 13 (

 613 Subject reduction of LF ∆ ). 1. If Γ Σ K, and K → ∆ K , then Γ Σ K ; 2. If Γ Σ σ : K, and σ → ∆ σ , then Γ Σ σ : K; 3. If Γ Σ ∆ : σ, and ∆ → ∆ ∆ , then Γ Σ ∆ : σ.

Figure 6 . 11 :

 611 Figure 6.11: The coercion function

=Figure 6 . 12 :

 612 Figure 6.12: Pure Type System presentation of the ∆-framework (signature and context)

2 .

 2 Adequacy, Canonical Forms, Exotic terms: in the presence of union types, we have to pay special attention to the exact formulation of adequacy results, as in the Harrop's formulae example of Chapter 8. Otherwise exotic terms arise, such as [λx:σ.C[x], λx:τ.D[x]] y, where C[-] and D[-] are distinct contexts (i.e. terms with holes), which cannot be naturally simplified even if C[-] ≡ D[-] . More work needs to be done to streamline how to exclude, or even capitalize, on exotic terms.

  λx.(λz.x (λu.x u) z (λt.λu.x u))It is translated using de Bruijn indices as: λx.(λz.1 (λu.2 0) 0 (λt.λu.3 0))

(

  * Transform (lambda x. t1) t2 into t1[t2/x] *) let beta_redex t1 t2 = let subst k l m = if m < k then Var (l, m) (* bound variable *) else if m = k then (* x *) lift 0 k t2 else (* the enclosing lambda goes away *)

2 .

 2 the local environment (noted Γ). It is used for the first step of typechecking, and looks like a standard environment: Γ ::= • | Γ, x:σ | Γ, x := ∆ : σ Intuitively, x:σ is a variable introduced by a λ-abstraction, and x := ∆ : σ is a local definition introduced by a let.

Figure 7 . 3 :

 73 Figure 7.3: Rules for ⇑ (2nd part)

Figure 7

 7 Figure 7.7: Rules for E ⇓

8. 1

 1 Encodings in LF ∆We start by showing the expressive power of LF ∆ in encoding classical features of typing disciplines with strong intersection and union. For these examples, we set Σ def = σ:Type, τ :Type.Auto application. The judgment λBDdL λx.x x : σ ∩ (σ → τ ) → τ in λ BDdL , is rendered in LF ∆ by the LF ∆ judgment Σ λx:σ ∩ (σ → τ ).(pr 2 x) (pr 1 x) : σ ∩ (σ → τ ) → τ . Polymorphic identity. The judgment λ BDdL λx.x : (σ → σ) ∩ (τ → τ ) in λ BDdL , is rendered in LF ∆ by the judgment Σ λx:σ.x, λx:τ.x : (σ → σ) ∩ (τ → τ ).Commutativity of union. The judgmentΣ λx.x : (σ ∪ τ ) → (τ ∪ σ) in λ BDdL, is rendered in LF ∆ by the judgment Σ λx:σ∪τ.[λy:σ.in τ 2 y, λy:τ.in σ 1 y] x : (σ ∪ τ ) → (τ ∪ σ). The Bull code corresponding to these examples is the following: Axiom (s t : Type). Definition auto_application (x : s & (s -> t)) := (proj_r x) (proj_l x). Definition poly_id : (s -> s) & (t -> t) := let id1 x := x in let id2 x := x in < id1, id2 >. Definition commut_union (x : s | t) := smatch x with

o

  : T ype ⊃: o → o → o Elim, Nf 0 : o → Type Nf ≡ λA:o.Nf 0 (A) ∪ Elim(A) ⊃ I : ΠA, B:o.(Elim(A) → Nf(B)) → Nf 0 (A ⊃ B) ⊃ E : ΠA, B:o.Elim(A ⊃ B) → Nf 0 (A) → Elim(B).The corresponding Bull code is the following:Axiom (o : Type) (impl : o -> o -> o) (Elim Nf0 : o -> Type). Definition Nf A := Nf0 A | Elim A. Axiom impl_I : forall A B, (Elim A -> Nf B) -> (Nf0 (impl A B)). Axiom impl_E : forall A B, Elim (impl A B) -> Nf0 A -> Elim B.

  Luigi Liquori and Claude Stolze. The Delta-calculus: Syntax and Types. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, pages 28:1-28:20. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, June 2019. [66] -Furio Honsell, Luigi Liquori, Ivan Scagnetto, and Claude Stolze. The Delta-framework. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, pages 37:1-37:21. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, December 2018. [57] -Luigi Liquori and Claude Stolze. A Decidable Subtyping Logic for Intersection and Union Types. In 2nd International Conference on Topics in Theoretical Computer Science, TTCS 2017, pages 74-90. Springer, September 2017. [65]

-Claude Stolze, Luigi Liquori, Furio Honsell, and Ivan Scagnetto. Towards a Logical Framework with Intersection and Union Types. In 11th International Workshop on Logical Frameworks and Meta-languages, LFMTP 2017, pages 1-9. ACM, September 2017. [88] -Daniel J. Dougherty, Ugo de'Liguoro, Luigi Liquori, and Claude Stolze. A Realizability Interpretation for Intersection and Union Types. In Programming Languages and Systems -14th Asian Symposium, APLAS 2016, pages 187-205. Springer, October 2016. [39]

  →∩), (U top ), (U→)[11] Figure 2.3: Type theories λ CD ∩ , λ CDS ∩ , λ CDV ∩ , and λ BCD ∩ . The "ref." column refers to the original articles these theories come from 3. (Intersection type theories T ). An intersection type theory T is a set of sentences of the form σ τ satisfying at least the axioms and rules of the minimal type theory min defined in Figure 2.1. The type theories T CD , T CDV , T CDS , and T BCD are the smallest type theories over A satisfying the axioms and rules given in Figure 2.3. We write T 1 T 2 if, for all σ, τ such that σ T 1 τ , we have that σ T 2 τ . In particular T CD T CDV T BCD and T CD T CDS T BCD . We will sometime note, for instance, BCD instead of T BCD ; 4. (Intersection type assignment systems λ T

  then, for some ∆ 1 , we have that ∆ 1 =⇒ ∆ 1 and ∆ ≡ (∆ 1 ) σ , therefore, by induction hypothesis, ∆ =⇒ (∆ * 1 ) σ ≡ ∆ * ; -if ∆ ≡ ∆ 1 , ∆ 2 , then, for some ∆ 1 and ∆ 2 , we have that ∆ 1 =⇒ ∆ 1 , ∆ 2 =⇒ ∆ 2 and ∆ ≡ ∆ 1 , ∆ 2 . By induction hypothesis, ∆ =⇒ ∆ * 1 , ∆ * 2 ≡ ∆ * ; -if ∆ ≡ λx:σ.∆ 1 , then, for some ∆ 1 , we have that ∆ 1 =⇒ ∆ 1 and ∆ ≡ λx:σ.∆ 1 . By induction hypothesis, λx:σ.∆ 1 =⇒ λx:σ.∆ * 1 ≡ ∆ * ; -if ∆ ≡ ∆ 1 ∆ 2 and ∆ is not a β-redex, then, for some ∆ 1 and ∆ 2 , we have that ∆ 1 =⇒ ∆ 1 , ∆ 2 =⇒ ∆ 2 and ∆ ≡ ∆ 1 ∆ 2 . By induction hypothesis, ∆ =⇒ ∆ * ≡ (λx:σ.∆ 1 ) ∆ 2 , then, for some ∆ 1 and ∆ 2 , we have that ∆ 1 =⇒ ∆ 1 , ∆ 2 =⇒ ∆ 2 ≡ pr i ∆ 1 and ∆ 1 is not a strong pair, then, for some ∆ 1 , we have that ∆ 1 =⇒ ∆ 1 and ∆ ≡ pr i ∆ 1 , therefore, by induction hypothesis, ∆ =⇒ pr i ∆ * 1 ≡ ∆ * ; -if ∆ ≡ pr i ∆ 1 , ∆ 2 , then, for some ∆ 1 and ∆ 2 , we have that ∆ 1 =⇒ ∆ 1 , ∆ 2 =⇒ ∆ 2 and we have 2 subcases: -∆ ≡ pr i ∆ 1 , ∆ 2 : by induction hypothesis, ∆ =⇒ ∆ * i ≡ ∆ * ; -∆ ≡ ∆ i : we also have, by induction hypothesis, ∆ =⇒ ∆ * i ≡ ∆ * . -→ -→∆ 2 and ∆ 1 -→ -→∆ 3 , then there exists ∆ 4 such that ∆ 2 -→ -→∆ 4 and ∆ 3 -→ -→∆ 4 .

	1 ∆ * 2 ≡
	∆ * ;
	-if ∆ and we have 2 subcases:
	-∆ ≡ (λx:σ.∆ 1 ) ∆ 2 : by induction hypothesis, ∆ =⇒ ∆ * 1 [∆ * 2 /x] ≡ ∆ * ;
	-∆ ≡ ∆ 1 [∆ 2 /x]: we also have ∆ =⇒ ∆ * 1 [∆ * 2 /x], thanks to point (3) of Lemma
	2.2;
	-if ∆ The Church-Rosser property follows from Lemma 2.3.
	Theorem 2.4 (Confluence).
	If ∆ 1

  and K is also a kind in LF PTS ∆ ;4. for any family σ, ifΓ Σ σ : K in LF ∆ , then Γ Σ σ : K in LF PTS ∆ ,and σ is a family in LF PTS ∆ ; 5. for any object ∆, if Γ Σ ∆ : σ in LF ∆ , then Γ Σ ∆ : σ in LF PTS ∆ , and ∆ is an object in LF PTS ∆ . Proof. All the parts are easily proved by mutual induction on the derivation tree.

  •, defined as x 1 : σ 1 ; . . . x n : σ n def = x 1 ; . . . ; x n 2. when we want to create a new meta-variable in a local context Γ = x 1 : σ 1 ; . . . x n : σ n , we create a meta-variable ?y[ Γ] ≡ ?y[x 1 ; . . . ; x n ]. The vector ∆ 1 ; . . . ; ∆ n inside ?y[∆ 1 ; . . . ; ∆ n ] is the suspended substitution of ?y. Substitutions for meta-variable and their suspended substitution are propagated as follows:

?y[∆ 1 ; . . .

; ∆ n ][∆/x] def = ?y[∆ 1 [∆/x]; . . . ; ∆ n [∆/x]] ?y[M 1 ; . . . ; M n ][N/x] def = ?y[M 1 [N/x]; . . . ; M n [N/x]]

in foo env ctx a b

  Φ 1 ; Σ; Γ σ 1 : Type ⇓ σ 1 ; Φ 2 Φ 2 ; Σ; Γ σ 2 : Type ⇓ σ 2 ; Φ 3 Φ 1 ; Σ; Γ σ 1 ∩ σ 2 ⇑ σ 1 ∩ σ 2 : Type; Φ 3 (∩) Φ 1 ; Σ; Γ σ 1 : Type ⇓ σ 1 ; Φ 2 Φ 2 ; Σ; Γ σ 2 : Type ⇓ σ 2 ; Φ 3 Φ 1 ; Σ; Γ σ 1 ∪ σ 2 ⇑ σ 1 ∪ σ 2 : Type; Φ 3 (∪) Φ 1 ; Σ; Γ ∆ 1 ⇑ ∆ 1 : σ 1 ; Φ 2 Φ 2 ; Σ; Γ ∆ 2 ⇑ ∆ 2 : σ 2 ; Φ 3 Φ 3 ; Σ; Γ σ 1 ∩ σ 2 : Type ⇓ Φ 4 Φ 1 ; Σ; Γ ∆ 1 , ∆ 2 ⇑ ∆ 1 , ∆ 2 : σ 1 ∩ σ 2 ; Φ 4 (Spair ) Φ 1 ; Σ; Γ ∆ ⇑ ∆ : σ; Φ 2 Φ 1 ; Σ; Γ σ = β σ 1 ∩ σ 2 Φ 1 ; Σ; Γ pr i ∆ ⇑ pr i ∆ : σ i ; Φ 2 (proj 1 )

Φ 1 ; Σ; Γ ∆ ⇑ ∆ : σ; Φ 2

Φ 2 , (Γ ?x 1 : Type), (Γ ?x 2 : Type); Σ; Γ σ

? =?x 1 [ Γ]∩?x 2 [ Γ] U Φ 3 Φ 1 ; Σ; Γ pr i ∆ ⇑ pr i ∆ :?x i [ Γ]; Φ 3 (proj 2 ) Φ 1 ; Σ; Γ ∆ ⇑ ∆ : σ ; Φ 2 Φ 2 ; Σ; Γ λx:τ 1 .τ 2 : Πx:σ → Type ⇓ λx:τ 1 .τ 2 ; Φ 3 Φ 3 ; Σ; Γ σ 1 : Type ⇓ σ 1 ; Φ 4 Φ 4 ; Σ; Γ σ 2 : Type ⇓ σ 2 ; Φ 5 Φ 5 ; Σ; Γ σ ? = σ 1 ∪ σ 2 U Φ 6 Φ 6 ; Σ; Γ, x:σ 1 ∆ 1 : τ 2 [in 1 σ 2 x/x] ⇓ ∆ 1 ; Φ 7 Φ 7 ; Σ; Γ, x:σ 2 ∆ 2 : τ 2 [in 2 σ 1 x/x] ⇓ ∆ 2 ; Φ 8 Φ 1 ; Σ; Γ smatch ∆ return λx:τ 1 .τ 2 with [x:σ 1 ⇒ ∆ 1 | x:σ 2 ⇒ ∆ 2 ] ⇑ smatch ∆ return τ with [x:σ 1 ⇒ ∆ 1 | x:σ 2 ⇒ ∆ 2 ] : τ 2 [∆ /x]; Φ 8 (Ssum) Φ 1 ; Σ; Γ σ F σ : s; Φ 2 Φ 2 ; Σ; Γ ∆ ⇑ ∆ : τ ; Φ 3 Σ; Γ τ σ Φ 1 ; Σ; Γ coe σ ∆ ⇑ coe σ ∆ : σ ; Φ 3 (Coe)

⇑

  Φ 3 Φ 2 ; Σ; Γ τ pr 2 ∆ ; Φ 3 (P roj 2 ) Φ 1 ; Σ; Γ τ = β τ 1 ∪ τ 2 Φ 1 ; Σ; Γ σ : Type ⇓ σ ; Φ 2 Φ 2 ; Σ; Γ σ M ; Φ 2 Φ 2 ; Σ; Ψ M @∆ 2 Φ 1 ; Σ; Ψ smatch ∆ return σ with [x:σ 1 ⇒ ∆ 1 | x:σ 2 ⇒ ∆ 2 ]

		Φ 1 ; Σ; Ψ	∆ 1 , ∆ 2	E ⇑	M ; Φ 3	E ⇓	Φ 3	(Spair )
	Φ 1 ; Σ; Γ σ	Φ 3 ; Σ; Ψ σ 1 Φ 1 ; Σ; Ψ ∆ Φ 1 ; Σ; Ψ ∆	Φ 1 ; Σ; Γ σ Φ 1 ; Σ; Γ σ E ⇑ ς 1 ; Φ 4 E ⇑ N ; Φ 2 Φ 1 ; Σ; Ψ ∆ F σ : τ ; Φ 3 Φ 4 ; Σ; Ψ, x ∆ 1 F σ : τ ; Φ 3 Φ 2 ; Σ; Ψ σ E ⇑ ς; Φ 3 E ⇑ M Φ 5 E ⇑ M ; Φ 2 Φ 1 ; Σ; Ψ pr i ∆ E ⇑ M ; Φ 2 (Proj ) E ⇑ M 2 ; Φ 2 Φ 2 ; Σ; Ψ M 1 ?	? = Kind ? = Kind	U Φ 3 U Φ 3	(Force 2 ) (Force 3 )
		Φ 5 ; Σ; Ψ σ 2	E ⇑	Figure 7.4: Rules for ς 2 ; Φ 6 Φ 6 ; Σ; Ψ, x M @∆ 2	E ⇓	Φ 7 (λx.M ) N ; Φ 7 E ⇑	(Ssum)
				Φ 1 ; Σ; Ψ ∆	E ⇑	M ; Φ 2 M ; Φ 2 E ⇑	(Inj )
				Φ 1 ; Σ; Ψ ∆	E ⇑	M ; Φ 2
						E ⇑	λx.M ; Φ 3	(Abs)
			Φ 1 ; Σ; Ψ ∆ Φ 1 ; Σ; Ψ ∆ () E ⇑ E ⇑ M ; Φ 2 M ; Φ 2	(App 1 )
		Φ 1 ; Σ; Ψ ∆ 1 S Φ 1 ; Σ; Ψ ∆ 1 (S; ∆ 2 ) E ⇑ M ; Φ 2 Φ 1 ; Σ; Ψ ∆ 2 M N ; Φ 3 E ⇑	E ⇑	N ; Φ 3	(App 2 )
		Φ 1 ; Σ; Ψ σ 1 Φ 1 ; Σ; Ψ σ 1 ∩ σ 2 E ⇑ ς 1 ; Φ 2 Φ 2 ; Σ; Ψ σ 2 ς 1 ∩ ς 2 ; Φ 3 E ⇑ E ⇑	ς 2 ; Φ 3	(∩)
		Φ 1 ; Σ; Γ in i σ∆ : τ Φ 1 ; Σ; Ψ σ 1 E ⇑ ς 1 ; Φ 2 Φ 2 ; Σ; Ψ σ 2 ⇓ in i σ ∆ ; Φ 3 E ⇑ Φ 1 ; Σ; Ψ σ 1 ∪ σ 2 ς 1 ∪ ς 2 ; Φ 3 E ⇑	ς 2 ; Φ 3	(∪)	? = τ i	U Φ 3	(Inj )
				Figure 7.6: Rules for	E ⇑

⇑ (2nd part)

Φ 1 ; Σ; Γ σ ⇑ σ : τ ; Φ 2 Φ 2 ; Σ; Γ τ ? = Type U Φ 3 Φ 2 ; Σ; Γ τ ? = Kind U Φ 3 Φ 2 , sort(?x); Σ τ ? = s U Φ 4 Φ 1 ; Σ; Γ σ F σ : τ ; Φ 4 (Force 1 ) Φ 1 ; Σ; Γ σ ⇑ σ : τ ; Φ 2 Φ 2 ; Σ; Γ τ ? = Type U Φ 3 Φ 2 ; Σ; Γ τ ⇑ σ : τ ; Φ 2 Φ 2 ; Σ; Γ τ ? = Type U F Φ 1 ; Σ; Γ ∆ ⇑ ∆ : σ; Φ 2 Φ 2 ; Σ; Γ σ ? = τ U Φ 3 Φ 1 ; Σ; Γ ∆ : τ ⇓ ∆ ; Φ 3 (Default) Φ 1 ; Σ; Γ σ F σ : s; Φ 2 Φ 2 ; Σ; Γ ∆ 1 : σ ⇓ ∆ 1 ; Φ 3 Φ 3 ; Σ; Γ, x := ∆ 1 : σ ∆ 2 : τ ⇓ ∆ 2 ; Φ 4 Φ 1 ; Σ; Γ let x:σ := ∆ 1 in ∆ 2 : τ ⇓ let x:σ := ∆ 1 in ∆ 2 ; Φ 4 (Let) Φ 1 ; Σ; Γ τ = β Πx : τ 1 .τ 2 Φ 1 ; Σ; Γ σ F σ ; Φ 2 Φ 2 ; Σ; Γ σ ? = τ 1 U Φ 3 Φ 3 ; Σ; Γ, x:σ ∆ : τ 2 ⇓ ∆ ; Φ 4 Φ 1 ; Σ; Γ λx : σ.∆ : τ ⇓ λx : σ .∆ ; Φ 4 (Abs) Φ 1 ; Σ; Γ σ = β σ 1 ∩ σ 2 Φ 1 ; Σ; Γ ∆ 1 : σ 1 ⇓ ∆ 1 ; Φ 2 Φ 2 ; Σ; Γ ∆ 2 : σ 2 ⇓ ∆ 2 ; Φ 3 Φ 1 ; Σ; Γ ∆ 1 , ∆ 2 : σ ⇓ ∆ 1 , ∆ 2 ; Φ 3 (Spair )

Φ 1 , (Γ ?x : Type); Σ; Γ σ∩?x : Type ⇓ τ ; Φ 2 Φ 2 ; Σ; Γ ∆ : σ∩?x ⇓ ∆ ; Φ 3

Φ 1 ; Σ; Γ pr 1 ∆ : σ ⇓ pr 1 ∆ ; Φ 3 (P roj 1 ) Φ 1 , (Γ ?x : Type); Σ; Γ ?x ∩ σ : Type ⇓ τ ; Φ 2 Φ 2 ; Σ; Γ ∆ :?x ∩ σ ⇓ ∆ ; Φ 3 Φ 1 ; Σ; Γ pr 2 ∆ : σ ⇓ Φ; Σ; Γ _ : σ ⇓ ?x[ Γ]; Φ, (Γ ?x : σ) (Wildcard ) Figure 7.5: Rules for ⇓ Φ 1 ; Σ; Ψ ∆ 1 E Φ 1 ; Σ; Ψ in i σ ∆ Φ 1 ; Σ; Ψ coe σ ∆ E ⇑ M ; Φ 2 (Coe) Φ 1 ; Σ; Ψ σ 1 E ⇑ ς 1 ; Φ 2 Φ 2 ; Σ; Ψ, x σ

2 E ⇑ ς 2 ; Φ 3 Φ 1 ; Σ; Ψ Πx:σ 1 .σ 2 E ⇑ Πx:ς 1 .ς 2 ; Φ 3 (Prod ) Φ 1 ; Σ; Ψ σ E ⇑ ς; Φ 2 Φ 2 ; Σ; Ψ, x ∆ E ⇑ M ; Φ 3 Φ 1 ; Σ; Ψ λx:σ.∆

  Definition is0test : OK F. apply (Copair _ _ _ (Abst _ _ (fun x : _ ⇒ App _ _ (Proj_r _ _ (Proj_r _ _ is_0)) x)) (Abst _ _ (fun x : _ ⇒ App _ _ (Proj_l _ _ is_0) x))). now apply Test. apply Eqabst. intros x y pf. apply Eqapp. assert (H : Eq _ _ is_0 (Proj_r (arrow Neg F) (inter (arrow Zero T) (arrow Pos F)) is_0)) by apply Eqproj_r. assert (H0 : Eq _ _ (Proj_r (arrow Neg F) (inter (arrow Zero T) (arrow Pos F)) is_0) (Proj_r (arrow Zero T) (arrow Pos F) (Proj_r (arrow Neg F) (inter (arrow Zero T) (arrow Pos F)) is_0))) by apply Eqproj_r. assert (H1 : Eq _ _ is_0 (Proj_l (arrow Neg F) (inter (arrow Zero T)

	(arrow Pos F)) is_0))
	by apply Eqproj_l.
	apply Eqsymm in H.
	apply Eqsymm in H0.
	eapply Eqtrans.
	apply H0.
	eapply Eqtrans.
	apply H.
	apply H1.
	-trivial.
	Defined.
	End Test.

Not to be confused with Principia Mathematica, which he wrote with Alfred Whitehead from 1910 to 1913.

In Section 78, simply called "The contradiction".

the second one is λ-abstraction, noted with the binder λ: the expression λx.M denotes a function taking x as an argument and returning the expression M (possibly containing occurrences of x).We can see λ-abstraction as a function constructor, and application as a function eliminator. Combining λ-abstraction and application gives two computational rules:(β) (λx.M ) N reduces to M [N/x],i.e. all the free occurrences of x in M are substituted by N . This is the elimination of the construction of a function, and it is called a β-reduction;(η) λx.M x reduces to M if x is not free in M . This is the construction of the elimination of a function, and it is called an η-reduction.We can also assign type to terms. Intuitively:-in the λ-calculus à la Curry: we assign a type to a pure λ-term. For the simply-typed λ-calculus, we get the following rules for λ-abstraction and application:Γ, x:σ M : τ Γ λx.M : σ → τ (→I) Γ M : σ → τ Γ N : σ Γ M N : τ (→E)As you can see, stating that M has σ → τ intuitively means that M is a function on σ to τ ;-in the λ-calculus à la Church: we decorate a λ-term with types, typically the λabstraction becomes λx:σ.M , where we explicitly state that x has type σ. For the simply-typed λ-calculus, we get the following rules for λ-abstraction and application:

Among the many type systems for the λ-calculi, intersection is an interesting connective (see Henk Barendregt, Wil Dekkers, and Richard Statman[START_REF] Barendregt | Lambda calculus with types[END_REF] : intuitively, if some term M has both type σ and type τ , then we say it is polymorphic and it has type σ ∩ τ , as the derivation rules show:Γ M : σ Γ M : τ Γ M : σ ∩ τ (∩I) Γ M : σ ∩ τ

(ax) Γ, x:σ T ∩ M : τ Γ T ∩ λx.M : σ → τ (→I) Γ T ∩ M : σ Γ T ∩ M : τ Γ T ∩ M : σ ∩ τ (∩I) Γ T ∩ M : σ → τ Γ T ∩ N : σ Γ T ∩ M N : τ (→E) Γ T ∩ M : σ ∩ τ Γ T ∩ M : σ (∩E 1 ) Γ T ∩ M : σ ∩ τ Γ T ∩ M : τ (∩E 2 ) U ∈ A Γ T ∩ M : U

The typing rule ( T ) in the general typed system introduces type coercions: once a type coercion is introduced, it cannot be eliminated, so de facto freezing a ∆-term inside an explicit coercion. Tannen et al.[START_REF] Tannen | Inheritance as implicit coercion[END_REF] showed a translation of a judgment derivation from a "Source" system with subtyping (Cardelli's Fun[START_REF] Cardelli | On understanding types, data abstraction, and polymorphism[END_REF]) into an equivalent judgment derivation in a "Target" system without subtyping (Girard system F with records and recursion). In the same spirit, we present a translation that removes all explicit coercions. Intuitively, the translation proceeds as follows: every derivation ending with rule:

Γ M @u M : U (U) x:σ ∈ Γ Γ x : σ (Var) Γ, x:σ 1 M @∆ : σ 2 Γ λx.M @λx:σ 1 .∆ : σ 1 → σ 2 (→I) Γ M @∆ 1 : σ 1 → σ 2 Γ N @∆ 2 : σ 1 Γ M N @∆ 1 ∆ 2 : σ 2 (→E) Γ M @∆ 1 : σ 1 Γ M @∆ 2 : σ 2 Γ M @ ∆ 1 , ∆ 2 : σ 1 ∩ σ 2 (∩I) Γ M @∆ : σ 1 ∩ σ 2 i ∈ {1, 2} Γ M @pr i ∆ : σ i (∩E i ) Γ M @∆ : σ i {i, j} = {1, 2} Γ M @in σ j i ∆ : σ 1 ∪ σ 2

the logic NJ has been named by Gentzen[START_REF] Gentzen | Untersuchungen über das logische Schließen I[END_REF] as an abbreviation for "Kalkül des natürlichen intuitionistischen Schließens", i.e. "calculus of the natural intuitionistic deduction". The letters I and J were often considered the same by the Germans, way back when they used Fraktur letters.

As long as we trust the metatheory and the implementation of the theorem prover.

Thanks to the command Unset Elimination Schemes.

Actually, in Coq, there is a special notation for second-order pattern-matching, but it is not useful here.

We can see an analogy with lisp-2 dialects such as Emacs Lisp which allows you to have the same name for both a function and a variable.

Valid KindsΣ Γ Γ Σ Type (T ype) Γ, x:σ Σ K Γ Σ Πx:σ.K (ΠK) Valid Families Σ Γ a:K ∈ Σ Γ Σ a : K (Const) Γ Σ σ : K 1 Γ Σ K 2 K 1 = ∆ K 2 Γ Σ σ : K 2 (Conv) Γ, x:σ Σ τ : Type Γ Σ Πx:σ.τ : Type (ΠI) Γ Σ σ : Πx:τ.K Γ Σ ∆ : τ Γ Σ σ ∆ : K[∆/x] (ΠE) Γ Σ σ : Type Γ Σ τ : Type Γ Σ σ → r τ : Type (→ r I) Γ Σ σ : Type Γ Σ τ : Type Γ Σ σ ∩ τ : Type (∩I) Γ Σ σ : Type Γ Σ τ : Type Γ Σ σ ∪ τ : Type (∪I)Figure 6.6: Valid kinds and families Valid ObjectsΣ Γ c:σ ∈ Σ Γ Σ c : σ (Const) Σ Γ x:σ ∈ Γ Γ Σ x : σ (Var) Γ, x:σ Σ ∆ : τ Γ Σ λx:σ.∆ : Πx:σ.τ (ΠI) Γ Σ ∆ 1 : Πx:σ.τ Γ Σ ∆ 2 : σ Γ Σ ∆ 1 ∆ 2 : τ [∆ 2 /x] (ΠE) Γ, x:σ Σ ∆ : τ ∆ = η x Γ Σ λ r x:σ.∆ : σ → r τ (→ r I) Γ Σ ∆ : σ ∩ τ Γ Σ pr 1 ∆ : σ (∩E l ) Γ Σ ∆ 1 : σ → r τ Γ Σ ∆ 2 : σ Γ Σ ∆ 1 • r ∆ 2 : τ (→ r E) Γ Σ ∆ : σ ∩ τ Γ Σ pr 2 ∆ : τ (∩E r ) Γ Σ ∆ 1 : σ Γ Σ ∆ 2 : τ ∆ 1 = η ∆ 2 Γ Σ ∆ 1 , ∆ 2 : σ ∩ τ (∩I) Γ Σ ∆ : σ Γ Σ τ : Type σ = ∆ τ Γ Σ ∆ : τ (Conv) Γ Σ ∆ : σ Γ Σ σ ∪ τ : Type Γ Σ in τ 1 ∆ : σ ∪ τ (∪I l ) Γ Σ ∆ : τ Γ Σ σ ∪ τ : Type Γ Σ in σ 2 ∆ : σ ∪ τ (∪I r ) Γ Σ ∆ 1 : Πy:σ.ρ[in τ 1 y/x] ∆ 1 = η ∆ 2

CHAPTER 6. DEPENDENT TYPESValid TermsΣ Γ Γ Σ Type : Kind (T ype)Γ Σ σ : s 1 Γ, x:σ Σ τ : s 2 (s 1 , s 2 ) ∈ R Γ Σ Πx:σ.τ : τ (sI) Σ Γ c:σ ∈ Σ Γ Σ c : σ (Const) Σ Γ x:σ ∈ Γ Γ Σ x : σ (Var) Γ Σ σ : Type Γ Σ τ : Type Γ Σ σ → r τ : Type (rI) Γ Σ ∆ : σ Γ Σ τ : s σ = ∆ τ Γ Σ ∆ : τ (Conv) Γ Σ σ : Type Γ Σ τ : Type Γ Σ σ ∩ τ : Type (∩I) Γ Σ σ : Type Γ Σ τ : Type Γ Σ σ ∪ τ : Type (∪I) Γ, x:σ Σ ∆ : τ Γ Σ Πx:σ.τ : s Γ Σ λx:σ.∆ : Πx:σ.τ (ΠI) Γ Σ ∆ 1 : Πx:σ.τ Γ Σ ∆ 2 : σ Γ Σ ∆ 1 ∆ 2 : τ [∆ 2 /x] (ΠE) ∆ = η x Γ, x:σ Σ ∆ : τ Γ Σ σ → r τ : Type Γ Σ λ r x:σ.∆ : σ → r τ (→ r I) Γ Σ ∆ 1 : σ → r τ Γ Σ ∆ 2 : σ Γ Σ ∆ 1 • r ∆ 2 : τ (→ r E) Γ Σ ∆ : σ ∩ τ Γ Σ pr 1 ∆ : σ (∩E l ) Γ Σ ∆ : σ ∩ τ Γ Σ pr 2 ∆ : τ (∩E r ) Γ Σ ∆ : σ Γ Σ σ ∪ τ : Type Γ Σ in τ 1 ∆ : σ ∪ τ (∪I l ) Γ Σ ∆ : τ Γ Σ σ ∪ τ : Type Γ Σ in σ 2 ∆ : σ ∪ τ (∪I r ) ∆ 1 = η ∆ 2 Γ Σ ∆ 1 : σ Γ Σ ∆ 2 : τ Γ Σ ∆ 1 , ∆ 2 : σ ∩ τ (∩I) Γ Σ ∆ 1 : Πy:σ.ρ[in τ 1 y/x] ∆ 1 = η ∆ 2 Γ Σ∆ 2 : Πy:τ.ρ[in σ 2 y/x] Γ, x:σ ∪ τ Σ ρ : Type Γ Σ [∆ 1 , ∆ 2 ] : Πx:σ ∪ τ.ρ (∪E)

Raised by one of the referees of[START_REF] Honsell | The Deltaframework[END_REF].

In reference to the Turin fountains.

Even though I could not decipher the Coq parser.

For convenience, we wrote and typechecked these examples in Coq, as LF is a sublanguage of the Calculus of Constructions.

Hint Extern 1 ⇒ match goal with

It is quite tedious to prove that a term is in ANF (or CANF, or DANF), because we usually have to decompose the hypotheses and the goal as much as possible before applying trivial tactics. That is why we have defined a ad hoc tactic that tries as much as possible to prove that a term is in normal form: This tactic operates in three steps:

-for performance reasons, we first check that there is some hypothesis we can work with;

-we then simplify such hypotheses as much as possible;

-finally, we simplify the goal as much as possible, and we try to conclude.

Filters and ideals

The filter generated by a type σ is the set of all types greater than σ. The ideal generated by a type σ is the set of all types greater than σ. We define filters and ideals syntactically, in order to get a decision procedure. However, we cannot give a syntactical definition of filters or ideals for every type. Therefore we only define ideals for unions of ANFs, and we define filters for terms which have the syntax defined by the following predicate: We can now define filters and ideals:

Reserved Notation "↑ [ σ ] τ " (at level 65).

Reserved Notation "↓ [ σ ] τ " (at level 65).

Inductive Filter : term -> term -> Prop :=

The tactic uanf_ind σ either finds the hypothesis HH : [ ANF] σ or creates it, and then reverts all the hypotheses containing σ back into the goal (including HH), in such a way that we get a goal of the form ∀ σ : term, [ ANF] σ -> A (where A is some Coq expression). By then applying refine (Uanf_ind _ _ _ _), Coq applies Lemma Uanf_ind and tries to fill the four wildcards. The first wildcard is a term P : term -> Prop such that P σ is convertible with A.

Of course, the Coq refiner does not create the constant function fun x : term ⇒ A, but captures all the free occurrences of σ in A and creates the most general function possible fun σ : term ⇒ A (where the free σ in A are captured by the abstraction). The three remaining wildcards are a term of type ∀ α, P (Var α), another term of type ∀ σ τ , P σ -> P τ -> P (σ ∪ τ ), and a third term of type ∀ σ τ , P τ -> P (σ → τ ), and the Coq refiner usually cannot create them automatically. These missing terms become new goals for the user. We then introduce as much hypotheses as possible, using the intros tactic. This refinement process is what Coq does normally whenever the user applies the induction tactic.

Properties of filters and ideals

We first prove that filters and ideals correspond to subtyping.

The proofs are done either by induction on the rules of filters, or by induction on the rules of ideals. We then prove that filters are only defined for types verifying the predicate isFilter, and ideals are only defined for unions of ANFs. The proofs are also done either by induction on the rules of filters, or by induction on the rules of ideals:

Then we can prove that intersection and unions can be nicely decomposed inside filters and ideals:

The proofs are done either by induction on the predicate isFilter (for filters), or by induction on the predicate [ ANF] (for ideals).

The following lemma is a trivial simplification of the construction rules of Filter for the case of arrows:

We can prove that ↑ [σ] τ → ρ' by contravariance of the domain and covariance of the codomain:

The proof is done by induction on the predicate isFilter. Now we prove that every filter contains at least the filter ↑[U], and ideals never contain

Lemma FilterOmega is proved by induction on the predicate isFilter, while Lemma IdealnoOmega is simply proved by induction on σ. Lemma IdealnoOmegaArrow is also proved by induction on σ, with one non-trivial case: if σ is some type σ 1 → σ 2 (corresponding to the rules I_Arrow1 or I_Arrow2), then, by induction hypothesis, we have that ↓[σ 2 ] U, which is absurd because of the IdealnoOmegaArrow lemma. We prove that filters are upward-closed:

The proof is done by induction on the subtyping rules. The interesting cases are the following:

Moreover, by induction hypothesis, we know that

We conclude by contravariance of the domain and covariance of the codomain, which is given by Lemma FilterArrow';

-Rules R_OmegaTop : ∀ σ, σ U and R_OmegaArrow : U U → U: we need to show that

For the other cases, we reason by induction on isFilter σ.

We can then deduce the completeness of filters, i.e. for any type σ verifying isFilter σ, we have that ↑ [σ] τ if σ τ :

The proof follows trivially by applying Lemma Filter_closed. Similarly, we prove that ideals are downward-closed:

The proof is done by induction on the fact that σ is an union of ANFs (using the uanf_ind tactic). We can then deduce that ideals are complete:

The proof follows trivially by applying Lemma Ideal_closed.

Coq implementation of the subtyping algorithm

We implement the subtyping algorithm by mixing executable code and proofs: each function takes as input some data and possibly some proof on the data, then returns some data along with the proof the data verify some specification. The code alone is then extracted in OCaml. This technique is called strong specification in [START_REF] Bertot | Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions[END_REF]. For instance, the function deleteOmega takes a type σ and returns a type τ along with a proof that τ is equivalent to σ while being either quasi-U-free or syntactically equal to U. The implementation of the function is done in two parts:

-first, the computational part of the algorithm is given inside the refine tactic. Most of the proofs are not given, instead we put a wildcard (_);

-finally, the Coq refiner tries to either fill the wildcards or to generate the corresponding goal, therefore all the proofs are postponed to the second part of the implementation. The proofs are then written the usual way. The algorithms that rewrite types in CANF and DANF are quite heavy, so we define helper functions for the arrow, union, and intersection cases. Now we can implement the algorithm, thanks to the Fix function. Among the generated goals, we have to prove that the measure on the argument indeed decreases (it is the |-main_algo_order _ _ case).

Definition main_algo : ∀ pair : term * term, DANF (fst pair) -> CANF (snd pair) -> {fst pair snd pair} + {¬ fst pair snd pair}. refine (Fix wf_main_algo _ _). intros [σ τ ] rec. refine (match (σ,τ )

.1: The type assignment system λ BDdL of [7] and the type theory Ξ implication, as illustrated in Section 6.1.

Miquel [START_REF] Miquel | The implicit calculus of constructions[END_REF] discusses an extension of the Calculus of Constructions with implicit typing, which subsumes a kind of proof-functional intersection. His approach has opposite motivations to ours. While LF ∆ provides a Church-style version of Curry-style type assignment systems, Miquel's Implicit Calculus of Constructions encompasses some features of Curry-style systems in an otherwise Church-style Calculus of Constructions. In LF ∆ we can discuss also ad hoc polymorphism, while in the Implicit Calculus only structural polymorphism is encoded. Indeed, he cannot assign the type ((σ ∩ τ ) → σ) ∩ (ρ → ρ) to the identity λx.x [START_REF] Liquori | Private communications[END_REF]. Kopylov [START_REF] Kopylov | Dependent intersection: a new way of defining records in type theory[END_REF] adds a dependent intersection type constructor x:A ∩ B[x] to NuPRL, allowing the resulting system to support dependent records (which are a very useful data structure to encode mathematics). The implicit product-type of Miquel, together with the dependent intersection type of Kopylov, and a suitable equalitytype is used by Stump [START_REF] Stump | From realizability to induction via dependent intersection[END_REF] to enrich the impredicative second-order system λP 2, in order to derive induction.

In order to achieve our goals, we could have carried out simply the encoding of LF ∆ in LF. But, due to the side-conditions characterizing proof-functional connectives, this would have be achieved only through a deep encoding. As an example of this, in Section 8.2, we give an encoding of a subsystem of [7], where subtyping has been simulated using relevant arrows. This encoding illustrates the expressive power of LF in treating proofs as first-class citizens, and it was also a source of inspiration for LF ∆ .

We will discuss examples showing some encoding in the LF ∆ in Chapter 8: all examples have been checked by an experimental proof development environment for LF ∆ [START_REF] Stolze | Towards a logical framework with intersection and union types[END_REF] (see

Since the intended meaning of relevant implication is "essentially" the identity, introducing variables or constants whose type is a relevant implication, amounts to assuming axioms corresponding to type inclusions such

Typed derivation of Pierce's example

Here is the typed derivation of Pierce's example (from Figure 6.9):

where: [7]). The system λ BDdL without U gives types only to strongly normalizing terms.

LF ∆ metatheory

LF ∆ can play the role of a Logical Framework only if decidable. The road map which we follow to establish decidability is the standard one, see e.g. [START_REF] Harper | A framework for defining logics[END_REF]. In particular, we prove in order: uniqueness of types and kinds, structural properties, and normalization for well-formed terms. Then we prove the inversion property, the subderivation property, subject reduction, and finally decidability. But first, we prove the fundamental lemmas: Lemma 6.3. Let α be either σ : K or ∆ : σ. Then:

that x 1 does not occur free in Γ or in τ , and that τ is valid in Γ.

Proof. All the proofs are done by induction on the structure of the derivation.

The first important step states that if a ∆-term is typable, then its type is unique up to = ∆ . Theorem 6.4 (Unicity of types and kinds).

Proof. All the proofs are done by induction on the structure of the derivation.

Strong normalization is proved as in LF. First we encode terms of LF ∆ into terms of the type assignment system λ BDdL such that redexes in the source language correspond to redexes in the target language and we use Theorem 6.2. Then, we introduce two forgetful mappings, namely || -|| and | -|, defined in Figure 6.10, to erase dependencies in types and to drop proof-functional constructors in ∆-terms and we conclude. Special care is needed in dealing with redexes occurring in type-dependencies, because these need to be flattened at the level of terms. The forgetful mappings are extended to contexts and signatures in the obvious way. The clauses for strong pairs/sums are justified by the following lemma:

Proof. By induction on ∆ 1 . Note that β-conversion is needed in the case where ∆ 1 ≡ λx:σ.∆ 1 for some ∆ 1 . In that case, it is necessary that ∆ 2 ≡ λx:τ.∆ 2 , for some ∆ 2 , and we have that

-for de Bruijn indices corresponding to variables bound outside the argument (x in the example), we update it by adding the number of extra binders (in the example, the extra binders are λz in the first case, and λz, λt in the second case); -for de Bruijn indices corresponding to variables bound inside the argument (u in the example), we do not change anything.

This auxiliary function is called lift in the literature (see e.g. [5]), where lift k n t updates the tree t, which is a subtree of the argument of the redex, where we are under k local binders, and there are n extra binders. The argument k is used to determine whether a de Bruijn index correspond to a variable inside or outside the argument, and n is the value to add, where appropriate.

Syntax of terms

We present a syntax for the language we have implemented. We use a Pure Type System approach, therefore all the terms are read through the same parser. The main differences with the ∆-framework presented in Chapter 6 are the additions of a placeholder and meta-variables, used by the refiner. We also added a let operator and changed the syntax of the strong sum so it looks more like the concrete syntax used in the implementation. A meta-variable ?x[∆ 1 ; ...; ∆ n ] has the, so called, suspended substitutions ∆ 1 ; ...; ∆ n , which will be explained clearly in Subsection 7.2.4. Finally, following the Cervesato-Pfenning jargon [START_REF] Cervesato | A linear spine calculus[END_REF], applications are in spine form, i.e. the arguments of a function are stored together in a list, exposing the head of the term separately.

Spines for ∆-terms have the following syntax:

We also have a similar syntax for the essence:

Spines for essences have the following syntax:

Note that essences of types (noted ς) belongs to the same syntactical set as essences of terms.

Concrete syntax

The concrete syntax of the terms has been implemented with OCamllex and OCamlyacc. Its simplified syntax is as follows: in the abstract syntax. The concrete syntax thus guarantees that the returned type is a λ-abstraction, and it allows a simplified behaviour of the type reconstruction algorithm (see rule (Ssum) in Figure 7.3). The behaviour of the concrete syntax is intended to mimic Coq 2 .

Implementation of the syntax

In the OCaml implementation, ∆-terms and their types along with essences and type essences are represented with a single type called term. It allows some functions (such as the normalization function) to be applied both on ∆-terms and on essences. The constructors of term contain the location information retrieved by the parser that allows the typechecker to give the precise location of a subterm to the user, in case of error.

The App constructor takes as parameters the applied function and the list of all the arguments. The list of parameters is used as a stack, hence the rightmost argument is the head of the list, and can easily be removed in the OCaml recursive functions. The variables are referred to as strings in the Const constructor, and as de Bruijn indices in Var constructors.

The evaluator of Bull

The evaluator follows the applicative order strategy, which recursively normalizes all subterms from left to right (with the help of the visit_term function), then:

-if the resulting term is a redex, reduces it, then use the same strategy again; -or else, the resulting term is in normal form.

Reduction rules

The reduction notions, from which we can defined one-step reduction, multistep reduction, and equivalence relation, are defined below.

1. for ∆-terms:

for pure λ-terms:

Implementation

When the user inputs a term, the refiner creates meta-variables and tries to instantiate them, but this should remain as much as possible invisible to the user. Therefore the term returned by the refiner should be meta-variable free, even though not in normal form. Thus terms in the global signature Σ are meta-variable free, and the δΦ reductions are only used by the unifier and the refiner.

If we want to normalize a term, The function strongly_normalize works on both ∆terms and pure λ-terms, and supposes that the given term is meta-variable free. Note that reductions can create odd spines, for instance if you consider the term (λx:σ.x S 1 ) (∆ S 2 ), a simple β-redex would give ∆ S 2 S 1 , therefore we merge S 2 and S 1 in a single spine.

The subtyping algorithm of Bull

The subtyping algorithm is basically the same as the one described in Chapter 5. The only difference is that the types are normalized before applying the algorithm.

The functions rewriting the terms in normal forms are the following: Definition 7.2 (Typing judgments). We have five typing judgments, corresponding to five OCaml functions: The rules are described in Figure 7.6;

5. The function essence_with_hint takes as inputs a meta-environment Φ 1 , a global environment Σ, an essence environment Ψ, a term ∆, and its expected essence M . It either fails or succeeds by returning the updated meta-environment Φ 2 . The corresponding judgment is the following:

The rules are described in Figure 7.7. There is a rule (Default) which applies only if none of the other rules work.

The Read-Eval-Print-Loop of Bull

The Read-Eval-Print-Loop (REPL) reads a command which is given by the parser as a list of atomic commands. For instance, if the user writes:

The parser creates the following list of three atomic commands:

1. the command asking a to be an axiom of type Type;

2. the command asking b to be an axiom of type Type;

3. the command asking f to be an axiom of type a -> b.

The REPL tries to process the whole list. If there is a single failure while processing the list of atomic commands, it backtracks so the whole commands fails without changing the environment. These commands are similar to the vernacular Coq commands and are quite intuitive. Here is the list of the REPL commands, along with their description:

show this list of commands Load "file".

for loading a script file Axiom term : type. define a constant or an axiom Definition name [: type] := term. define a term Print name.

print the definition of name Printall.

print all the signature (axioms and definitions) Compute name.

normalize name and print the result Quit. quit

Future work

The current version of Bull [START_REF] Stolze | [END_REF] (ver. 0.9, October 2019) is still a work-in-progress. We plan to implement the following features:

1. Inductive types are the most important feature to add, in order to have a really usable theorem prover. We plan to take inspiration from the works of Paulin-Mohring [START_REF] Paulin-Mohring | Inductive definitions in the system coq rules and properties[END_REF]. This should be reasonably feasible;

2. Mixing subtyping and unification is a difficult problem, especially with intersection and union types. The most extensive research which has been done in this domain is the work of Dudenhefner, Martens, and Rehof [START_REF] Dudenhefner | The intersection type unification problem[END_REF], where the authors study unification modulo subtyping with intersection types (but no union). It would be challenging to find a unification algorithm modulo subtyping for intersection and union types, but ideally it would allow us to do some implicit coercions. Take from example the code in Subsection 8.1.1, it would be interesting for the user to use implicit coercions in this way:

The unification algorithm would then guess that the first wildcard should be replaced with Pos -> F and the second one should be replaced with Neg -> F, which does not seem feasible if the unification algorithm does not take subtyping into account;

Pierce's code

We recall the Pierce code from Figure 1.1:

The expressive power of union types highlighted by Pierce is rendered in LF ∆ by: N eg : Type Zero : Type P os : Type T : Type F : Type Test : P os ∪ N eg

The Bull code corresponding to this example is the following:

As you can see, the code is quite short and readable, in contrast to the LF encoding of the same example found in Figure 8.2.

Hereditary Harrop formulae

The encoding of Hereditary Harrop's Formulae is one of the motivating examples given by Pfenning for introducing refinement types in [START_REF] Pfenning | Refinement types for logical frameworks[END_REF]. In LF ∆ it can be expressed as in Figure 8.1 and type checked in Bull, without any reference to intersection types, by a subtle use of union types. We add also rules for solving and backchaining. Hereditary Harrop formulae can be recursively defined using two mutually recursive syntactical objects called programs (π) and goals (γ):

Using Example 6.1, we can provide an alternative encoding of atoms, goals and programs which is more faithful to the one by Pfenning. Namely, we can introduce in the signature the constants c 1 : α → r γ and c 2 : α → r π in order to represent the axioms atom goal and atom prog in Pfenning's encoding. Our approach based on union types, while retaining the same expressivity permits to shortcut certain inclusions and to rule out also certain exotic goals and exotic programs. Indeed, for the purpose of establishing the adequacy of the encoding, it is sufficient to avoid variables involving union types in the derivation contexts. The Bull code is the following:

(* three base types: atomic propositions, non-atomic goals and non-atomic programs *) Axiom atom : Type. Axiom non_atomic_goal : Type.

Atomic propositions, non-atomic goals and non-atomic programs: α, γ 0 , π 0 : Type Goals and programs:

2 (pr 1 impl x y) impl 2 = λx:γ.λy:π.in α 2 (pr 2 impl x y) and : (γ → γ → γ 0 ) ∩ (π → π → π 0 ) and 1 = λx:γ.λy:γ.in α 2 (pr 1 and x y) and 2 = λx:π.λy:π.in α 2 (pr 2 and x y) or : (γ → γ → γ 0 ) or 1 = λx:γ.λy:γ.in α 2 (or x y) solve p g indicates that the judgment p g is valid. bchain p a g indicates that, if p g is valid, then p a is valid. solve : π → γ → Type bchain : π → α → γ → Type Rules for solve: -: Π(p:π)(g 1 , g 2 :γ).solve p g 1 → solve p g 2 → solve p (and

.solve (and 2 p 1 p 2 ) g → solve p 1 (impl 1 p 2 g) -: Π(p:π)(a:α)(g:γ).bchain p a g → solve p g → solve p (in γ 0 1 a) Rules for bchain: -: Π(a:α)(g:γ).bchain (impl 2 g (in π 0 1 a)) a g -: Π(p 1 , p 2 :π)(a:α)(g:γ).bchain p 1 a g → bchain (and 2 p 1 p 2 ) a g -: Π(p 1 , p 2 :π)(a:α)(g:γ).bchain p 2 a g → bchain (and 2 p 1 p 2 ) a g -: Π(p:π)(a:α)(g, g 1 , g 2 :γ).bchain (impl 2 (and 1 g 1 g 2 ) p) a g → bchain (impl 2 g 1 (impl 2 g 2 p)) a g -: Π(p 1 , p 2 :π)(a:α)(g, g 1 :γ).bchain (impl 2 g 1 p 1 ) a g → bchain (impl 2 g 1 (and 2 p 1 p 2 )) a g -: Π(p 1 , p 2 :π)(a:α)(g, g 1 :γ).bchain (impl 2 g 1 p 2 ) a g → bchain (impl 2 g 1 (and 2 p 1 p 2 )) a g (* backchain p a g means: if p |-g is valid, then p |-a is valid *) Metacircular Encodings. This example uses an experimental implementation of relevant arrows in Bull. The following diagram summarizes the network of adequate encodings/inclusions between LF ∆ , LF, and λ BDdL that can be defined:

We denote by S 1 =⇒ S 2 the encoding of system S 1 in system S 2 , where the label sh (resp. dp), denotes a shallow (resp. deep) embedding. The notation S 1 → S 2 denotes that S 2 is an extension of S 1 .

With the intention of providing a better formal understanding of the semantics of strong intersection and union types in a logical framework, we provide in Section 8.2 a deep LF encoding of a presentation of λ BDdL à la Church [START_REF] Daniel | A realizability interpretation for intersection and union types[END_REF]. An encoding of λ BDdL in LF ∆ can be mechanically type checked in the environment [START_REF] Stolze | Towards a logical framework with intersection and union types[END_REF]. We even can add the relevant arrow. The corresponding Bull code is the following: We also can show that the commutativity of union with a relevant arrow λx.x : (σ ∪ τ ) → r (τ ∪ σ):

Definition communion' := csabst (cunion s t) (cunion t s) (sfun x ⇒ smatch ccopair s t x with y ⇒ cini t s (inj_r (aOk t) y) , y ⇒ cini t s (inj_l (aOk s) y) end).

A shallow encoding of LF in LF ∆ making essential use of intersection types can be also type checked. The corresponding Bull code is the following: Axiom of_ax : of_3 star sqre. (* Rules for lambda-abstraction are "essentially" the same *) Definition of_lam1 := forall t1 t2 t3, of_2 t1 star -> (forall x, of_1 x t1 -> of_1 (t2 x) (t3 x)) -> of_1 (lam_1 t1 t2) (pi_1 t1 t3). Definition of_lam2 := forall t1 t2 t3, of_2 t1 star -> (forall x, of_1 x t1 -> of_2 (t2 x) (t3 x)) -> of_2 (lam_2 t1 t2) (pi_2 t1 t3). Axiom of_lam : of_lam1 & of_lam2. (* Rules for product are ''essentially'' the same *) Definition of_pi1 := forall t1 t2, of_2 t1 star -> (forall x, of_1 x t1 -> of_2 (t2 x) star) -> of_2 (pi_1 t1 t2) star. Definition of_pi2 := forall t1 t2, of_2 t1 star -> (forall x, of_1 x t1 -> of_3 (t2 x) sqre) -> of_3 (pi_2 t1 t2) sqre. Axiom of_pi : of_pi1 & of_pi2. (* Rules for application are ''essentially'' the same *) Definition of_app1 := forall t1 t2 t3 t4, of_1 t1 (pi_1 t3 t4) -> of_1 t2 t3 -> of_1 (app_1 t1 t2) (t4 t2). Definition of_app2 := forall t1 t2 t3 t4, of_2 t1 (pi_2 t3 t4) -> of_1 t2 t3 -> of_2 (app_2 t1 t2) (t4 t2). Axiom of_app : of_app1 & of_app2.

We finish this chapter by providing examples of encoding in LF.

Encodings in LF

We present a pure LF encoding of a presentation of λ BDdL à la Church, using the Coq syntax, and the Higher-Order Abstract Syntax (HOAS) [START_REF] Pfenning | Higher-order abstract syntax[END_REF]. We use HOAS in order to take advantage of the higher-order features of the frameworks: other abstract syntax representation techniques would not be much different, but more verbose: The Eq predicate plays the same role of the essence function in LF ∆ , namely, it encodes the judgment that two proofs (i.e. two terms of type (OK _)) have the same structure. This is crucial in the Pair axiom (i.e. the introduction rule of the intersection type constructor) where we can inhabit the type (inter s t) only when the proofs of its component types s and t share the same structure (i.e. we have a witness of type (Eq s t M N), where M has type (OK s) and N has type (OK t)). A similar role is played by the Eq premise in the Sum axiom (i.e. the elimination rule of the union type constructor). We have an Eq axiom for each proof rule.

Using this encoding, we can encode auto-application, polymorphic identity, and commutativity of union: The definition of commutunion is quite unreadable, and has been created from the following Ltac script: Using the same encoding of LF ∆ in Coq, the Pierce's code from Figure 1.1 would be encoded as: