# A Decidable Subtyping Logic for Intersection and Union Types

Luigi Liquori, Claude Stolze

► To cite this version:

Luigi Liquori, Claude Stolze. A Decidable Subtyping Logic for Intersection and Union Types. TTCS 2017 - 2nd International Conference on Topics in Theoretical Computer Science, Sep 2017, Tehran, Iran. pp.74-90, 10.1007/978-3-319-68953-1_7. hal-01760641

HAL Id: hal-01760641

https://inria.hal.science/hal-01760641

Submitted on 6 Apr 2018

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A Decidable Subtyping Logic for Intersection and Union Types*

Luigi Liquori and Claude Stolze

Université Côte d'Azur, INRIA, France

Luigi.Liquori@inria.fr

Claude.Stolze@inria.fr

**Abstract.** Using Curry-Howard isomorphism, we extend the typed lambda-calculus with intersection and union types, and its corresponding proof-functional logic, previously defined by the authors, with subtyping and explicit coercions. We show the extension of the lambda-calculus to be isomorphic to the Barbanera-Dezani-de'Liguoro type assignment system and we provide a sound interpretation of the proof-functional logic with the NJ(β) logic, using Mints' realizers. We finally present a sound and complete algorithm for subtyping in presence of intersection and union types. The algorithm is conceived to work for the (sub)type theory Ξ.

**Keywords.** Logics and lambda-calculus, type and subtype systems.

## 1 Introduction

This paper is a contribution to the study of typed lambda-calculi à la Church in presence of intersection, union types, and subtyping and their role in logical investigations; it is a natural follow up of a recent paper by the authors [DdLS16].

Intersection types were first introduced as a form of *ad hoc* polymorphism in (pure) lambda-calculi à la Curry. The paper by Barendregt, Coppo, and Dezani [BCDC83] is a classic reference, while [Bar13] is a definitive reference.

Union types were later introduced as a dual of intersection by MacQueen, Plotkin, and Sethi [MPS86]: Barbanera, Dezani, and de'Liguoro [BDCd95] is a definitive reference; Frisch, Castagna, and Benzaken [FCB08] designed a type system with intersection, union, and negation types whose semantics are loosely the corresponding set-theoretical constructs.

As intersection and union types had their classical development for (undecidable) type assignment systems, many papers moved from intersection and union type theories to (typed) lambda-calculi à la Church: the programming language Forsythe, by Reynolds [Rey96], is probably the first reference for intersection types, while Pierce's PhD thesis combines also unions and intersections [Pie91]; a recent implementation of a typed programming language featuring intersection and union types is [Dun14].

Proof-functional logical connectives allow reasoning about the structure of logical proofs, in this way giving to the latter the status of first-class objects. This is in contrast with classical truth-functional connectives where the meaning of a compound formula

<footnote>* Work supported by the COST Action CA15123 EUTYPES "The European research network on types for programming and verification".</footnote>
is dependent only on the truth value of its subformulas. Following this approach, the
logical relation between type assignment systems and typed systems featuring intersec-
tion and union types were studied in [LR07,DL10,DdLS16].

Proof-functional connectives represent evidence as a “polymorphic” construction, that is, the same evidence can be used as a proof for different sentences. Pottinger [Pot80] first introduced a conjunction, called strong conjunction $∩$, requiring more than the existence of constructions proving the left and the right hand side of the conjuncts. According to Pottinger: “*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$*”. This interpretation makes inhabitants of $A ∩ B$ as uniform evidences for both $A$ and $B$. Later, Lopez-Escobar [LE85] presented the first proof-functional logic with strong conjunction as a special case of ordinary conjunction.

Mints [Min89] presented a logical interpretation of strong conjunction using reali-
zers: the logical predicate $r_{A∩B}[M]$ is true if the pure lambda-term $M$ is a realizer (also
read as “M is a method to assess $A ∩ B$”) for both the formula $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, Lopez-Escobar’s strong
equivalence, or Bruce, Di Cosmo, and Longo provable type isomorphism [BCL92].

Recently [DdLS16] extended the logical interpretation with union types as another
proof-functional operator, the strong union $∪$. Paraphrasing Pottinger’s point of view,
we could say that the intuitive meaning of $∪$ is that if we have a reason to assert $A$ (or
$B$), then the same reason will also assert $A ∪ B$. This interpretation makes inhabitants
of $(A ∪ B) ⊃ C$ be uniform evidences for both $A ⊃ C$ and $B ⊃ C$. Symmetri-
cally to intersection, and extending Mints’ logical interpretation, the logical predicate
$r_{A∪B}[M]$ succeeds if the pure lambda-term $M$ is a realizer for either the formula $r_A[M]$
or $r_B[M]$.

**1.1 Contributions.**

This paper focus on the logical and algorithmic aspects of subtyping in presence of
intersection and union types: our interest is not only theoretical but also pragmatic
since, in a dependent-type setting, it opens the door to logical frameworks and proof-
assistants. We also inspect the relationship between pure and typed lambda-calculi
and their corresponding proof-functional logics as dictated by the well-known Curry-
Howard [How80] correspondence. We’ll present and explore the relationships between
the following four formal systems:

- $\Lambda_u^{∩}$, the type assignment system with intersection and union types for pure lambda-calculus with subtyping with the (sub)type theory $Ξ$, as defined in [BDCd95]: a type assignment judgment have the shape $Γ ⊢ M : σ$;

- $\Lambda_t^{∩}$, an extension of the typed lambda-calculus with strong pairs and strong sums, as defined in [DL10], with subtyping and explicit coercions: a type judgment has the shape $Γ^σ ⊢ M @ Δ : σ$, where $Δ$ is a typed lambda-term enriched with strong pairs and strong sums;

- $\mathcal{L}^{∩}$, an extension of the proof-functional logic $\mathcal{L}^{∪}$ of [DdLS16] with *ad hoc* formulas and inference rules for subtyping and explicit coercions: sequents have the shape $Γ ⊢ Δ : σ$;
- NJ(β), a natural deduction system for derivations in first-order intuitionistic logic with pure lambda-terms [Pra65].

Intuitively, $\Delta$ denotes a proof for a type assignment derivation for $M$; from an opera-
tional point of view, reductions in pure $M$ and typed $\Delta$ must be synchronized by suit-
able parallel reduction rules in order to preserve parallel reduction of subjects. From a
typing point of view, the type rules of $\Lambda_{t\leq}^{\cup}$ should encode the proof-functional nature
of strong intersection and strong union, i.e. the fact that in an intersection (resp. union)
the two $\Delta$ relate to the same $M$.

Thanks to an erasing function $\iota-\jmath$ translating typed $\Delta$ to pure $M$, we could rea-
son only on a proof-functional logic $\mathcal{L}_{\leq}^{\cup}$ assigning types to $\Delta$. Therefore, the original
contribution are as follows:

- to define the typed lambda-calculus $\Lambda_{t\leq}^{\cup}$ obtained by extending the typed calculus of [DL10] with a subtyping relation and explicit coercions, keeping decidability of type checking, and showing the isomorphism with the type assignment system $\Lambda_{t\leq}^{\cup}$ of [BDCd95]. Terms of $\Lambda_{t\leq}^{\cup}$ have the form $M@\Delta$ where $M$ is a pure lambda-term, while $\Delta$ is a typed lambda-term enriched with strong pairs and strong sums;

- to define $\mathcal{L}_{\leq}^{\cup}$ obtained by extending the proof-functional logic $\mathcal{L}_{\leq}^{\cup}$ of [DdLS16]: we show that the extended $\mathcal{L}_{\leq}^{\cup}$ logic of subtyping is sound with respect to the realizability logic NJ($\beta$), using Mint's realizability arguments;

- to present an algorithm for subtyping in presence of intersection and union types.
The algorithm (presented in functional style) is conceived to work for the (sub)type
theory $\Xi$ (i.e. axioms 1 to 14, as presented in [BDCd95]).

For lack of space, the full metatheoretical development can be found in [LS17].

## 1.2 Related Work

We shortly list the main research lines involving type (assignment) systems with in-
tersection, union, and subtyping for (un)typed lambda-calculi, proof-functional logics
containing “strong operators”, and realizability.

The formal investigation of soundness and completeness for a notion of realizability
was initiated by Lopez-Escobar [LE85] and subsequently refined by Mints [Min89].

Barbanera and Martini [BM94] studied three proof-functional operators, namely
the strong conjunction, the relevant implication (related with Meyer-Routley's [MR72]
system $B^+$), and the strong equivalence connective for double implication, relating
those connectives with a suitable type assignment system, a realizability semantics, and
a completeness theorem.

Dezani-Ciancaglini, Ghilezan, and Venneri [DCGV97] investigated a Curry-Ho-
ward interpretation of intersection and union types (for Combinatory Logic): using the
well-understood relation between combinatory logic and lambda-calculus, they encode
type-free lambda-terms into suitable combinatory logic formulas and then type them us-
ing intersection and union types. This is a complementary approach to the realizability-
based one here and in [DdLS16].

Various authors defined lambda-calculi à la Church for intersection types with re-
lated logics: see [Bar13] (pp. 780-781) for a complete list.
As mentioned before, Barbanera, Dezani-Ciancaglini, and de'Liguoro [BDCd95] introduced a pure lambda-calculus $\Lambda_u^{\supseteq}$ with a related type assignment system featuring intersection and union types, and a powerful subtyping relation.

The previous work [DL10] presented a typed calculus $\Lambda_t^{\supset}$ (without subtyping) that explored the relationship between the proof-functional intersections and unions and the corresponding type assignment system (without subtyping).

In [DdLS16] we introduced an erasing function, called *essence* and denoted by $\iota\Delta$, to understand the connection between pure terms and typed terms: we proved the isomorphism between $\Lambda_t^{\supset}$ and $\Lambda_u^{\supset}$, and we showed that $\mathcal{L}^{\supset}$ can be thought of as a proof-functional logic. The present paper extends all the systems and logics of [DdLS16] and presents a comparative analysis of the (sub)type theories $\Xi$ and $\Pi$ of [BDCd95]: this motivates the use of the (sub)type theory $\Xi$ with their natural correspondence with $NJ(\beta)$.

Hindley gave first a subtyping algorithm for type intersection [Hin82]: there is a rich literature reducing the subtyping problem in presence of intersection and union to a set constraint problem: good references are [Dam94,Aik99,DP04,FCB08]. The closest work to the algorithm presented in this paper has been made by Aiken and Wimmers [AW93] who 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. The rewriting in disjunctive normal form makes this algorithm exponential in time and space in the worst case.

Pfenning work on Refinement Types [Pfe93] pioneered an extension of Edinburgh Logical Framework with subtyping and intersection types: our aim is to study extensions of LF featuring fully fledged proof-functional logical connectives like strong conjunction, strong disjunction in presence of subtyping and relevant implication.

## 2 System

The pseudo-syntax of $\sigma$, $M$, $\Delta$, and the derived $M@\Delta$ are defined using the following three syntactic categories:

$$ \sigma ::= \omega \mid \phi \mid \sigma \rightarrow \sigma \mid \sigma \cap \sigma \mid \sigma \cup \sigma $$

$$ M ::= x \mid \lambda x.M \mid MM $$

$$ \Delta ::= * \mid x \mid \lambda x:\Delta \mid \Delta\Delta \mid \langle\Delta, \Delta\rangle \mid [\Delta, \Delta] \mid \text{pr}_1\Delta \mid \text{pr}_2\Delta \mid \text{in}_1\Delta \mid \text{in}_2\Delta \mid [\sigma]\Delta $$

where $\phi$ denotes arbitrary constant types and $\omega$ denotes a special type that is inhabited by all terms. The $\Delta$-expression $\langle\Delta, \Delta\rangle$ denotes the strong pair while $[\Delta, \Delta]$ denotes the strong sum, with the respective projections and injections, respectively. Finally $[\sigma]\Delta$ denotes the explicit coercion of $\Delta$ with the type $\sigma$.

The untyped reduction semantics for the calculus $\dot{a}la$ Curry $\Lambda_t^{\supset}$ is ordinary $\beta$-reduction, even if subject reduction holds only in presence of the “Gross-Knuth” parallel reduction (Def. 13.2.7 in [Bar84]), where all redexes in $M$ are contracted simultaneously. Reduction for the calculus $\dot{a}la$ Church $\Lambda_t^{\supset}$ is delicate because it must keep
<figure><img src="image_2.png" /><figcaption>**Fig. 1. Intersection and Union Type Assignment System $\Lambda_u^{\cap \cup}$ [BDCd95] (main rules).**</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>**Fig. 2. Typed Calculus $\Lambda_t^{\cap \cup}$ [DL10] (main rules).**</figcaption></figure>

synchronized the untyped reduction of $M$ with the typed reduction of $\Delta$: it is defined in Section 5 of [DL10]. Reductions in $\mathcal{L}^{\cap \cup}$ is ordinary $\beta$-reduction plus the following four reduction rules:

$$ \mathrm{pr}_i(\langle \Delta_1, \Delta_2 \rangle) \to_{\mathrm{pr}_i} \Delta_i \quad [\lambda x: \sigma_1. \Delta_1, \lambda x: \sigma_2. \Delta_2] \mathrm{in}_i \Delta_3 \to_{\mathrm{in}_i} \Delta_i \{\Delta_3 / i\} \quad i \in \{1, 2\} $$

Figure 1 presents the main rules of the type assignment system of [BDCd95]: note that the type inference rules are not syntax-directed. Figure 2 presents the main rules of the typed calculus $\Lambda_t^{\cap \cup}$ of [DL10]$^1$; note that this type system is completely syntax directed.

The next definition clarifies what we intend with “correspondence” between an un-
typed $M$ and a typed $\Delta$: the essence partial function shows the syntactic relation be-
tween type free and typed lambda-terms. Essence maps typed proof-terms ($\Delta$'s) into
pure $\lambda$-terms: intuitively, two typed $\Delta$-terms prove the same formula if they have the
same proof-essence.

**Definition 1 (Proof Essence).**

The essence function between pure and typed lambda-terms is defined as follows:

$$ \begin{align*} \l{\lambda x: \sigma. \Delta} &\triangleq \lambda x. \l{\Delta} \\ \l{\Delta_1 \Delta_2} &\triangleq \l{\Delta_1} \l{\Delta_2} \\ \l{\mathrm{pr}_i \Delta} &\triangleq \l{\Delta} \\ \l{\langle \Delta_1, \Delta_2 \rangle} &\triangleq \l{\Delta_1} \\ \l{[\lambda x: \sigma_1. \Delta_1, \lambda x: \sigma_2. \Delta_2]} &\triangleq \l{\Delta_3} \\ \end{align*} $$

<footnote n="1">¹ Contexts $\Gamma^\flat$ contains assumptions of the shape $x@\iota_x:\sigma$: the present paper uses ordinary contexts $\Gamma$, since $\Gamma$ can be easily obtained by erasing all the $_@\iota_x$ in $\Gamma^\flat$.</footnote>
<figure><img src="image_4.png" /><figcaption>Fig. 3. Proof-functional logic $\mathcal{L}^{\cap \cup}$ (main rules).</figcaption></figure>

Figure 3 presents the main rules of the proof-functional logic $\mathcal{L}^{\cap \cup}$ of [DdLS16]: that logic is *proof-functional*, in the sense of Pottinger [Pot80] and Lopez-Escobar [LE85]: formulas encode, using the Curry-Howard isomorphism, *derivations* $\mathcal{D} : \Gamma \vdash M : \sigma$ in the type assignment system $\Lambda_{\mathcal{U}}^{\cap \cup}$ which are, in turn, isomorphic to typed judgments $\Gamma \vdash M @ \Delta : \sigma$ of $\Lambda_{\mathcal{T}}^{\cap \cup}$. It is worth noticing that if we drop the restriction concerning the “essence” in rules $(\cap I)$ and $(\cup E)$ in the system $\mathcal{L}^{\cap \cup}$ and replace $\sigma \cap \tau$ by $\sigma \times \tau$, and $\sigma \cup \tau$ by $\sigma + \tau$, we get a simply typed lambda-calculus with product and sums, namely a truth-functional intuitionistic propositional logic with implication, conjunction, and disjunction in disguise: the resulting logic loses its proof-functionality.

The whole picture is now ready to be extended with the subtyping relation, as introduced in [BCDC83] and extended in [BDCd95] with unions. Subtyping is a preorder over types, and it is written as $\sigma \leq \tau$; a (sub)type theory denotes any collection of inequalities between types satisfying natural closure conditions. The (sub)type theory, called $\Xi$ (see Definition 3.6 of [BDCd95]), is defined by the subtyping axioms and inference rules defined as follows:

(1) $\sigma \leq \sigma \cap \sigma$

(2) $\sigma \cup \sigma \leq \sigma$

(3) $\sigma \cap \tau \leq \sigma, \sigma \cap \tau \leq \tau$

(4) $\sigma \cup \tau \leq \sigma, \sigma \cup \tau \leq \tau$

(5) $\sigma \leq \omega$

(6) $\sigma \leq \sigma$

(7) $\sigma_1 \leq \sigma_2, \tau_1 \leq \tau_2 \Rightarrow \sigma_1 \cap \tau_1 \leq \sigma_2 \cap \tau_2$

(8) $\sigma_1 \leq \sigma_2, \tau_1 \leq \tau_2 \Rightarrow \sigma_1 \cup \tau_1 \leq \sigma_2 \cup \tau_2$

(9) $\sigma \leq \tau, \tau \leq \rho \Rightarrow \sigma \leq \rho$

(10) $\sigma \cap (\tau \cup \rho) \leq (\sigma \cap \tau) \cup (\sigma \cap \rho)$

(11) $(\sigma \to \tau) \cap (\sigma \to \rho) \leq \sigma \to (\tau \cap \rho)$

(12) $(\sigma \to \rho) \cap (\tau \to \rho) \leq (\sigma \cup \tau) \to \rho$

(13) $\omega \leq \omega \to \omega$

(14) $\sigma_2 \leq \sigma_1, \tau_1 \leq \tau_2 \Rightarrow \sigma_1 \to \tau_1 \leq \sigma_2 \to \tau_2$

The (sub)theory $\Xi$ suggests the interpretation of $\omega$ as the *set universe*, of $\cap$ as the *set intersection*, of $\cup$ as the *set union*, and of $\leq$ as a sound (but not complete) *subset relation*, respectively, in the spirit of [FCB08]. In the following, we write $\sigma \sim \tau$ iff $\sigma \leq \tau$ and $\tau \leq \sigma$. We note that distributivity of union over intersection and intersection over union, i.e. $\sigma \cup (\tau \cap \rho) \sim (\sigma \cup \tau) \cap (\sigma \cup \rho)$ and $\sigma \cap (\tau \cup \rho) \sim (\sigma \cap \tau) \cup (\sigma \cap \rho)$ are derivable (see, e.g. derivation in [BDCd95], page 9).

Once the subtyping preorder has been defined, a classical subsumption (respectively an explicit coercion rule) can be defined as follows:
<figure><img src="image_5.png" /><figcaption>Fig. 4. The Logic NJ (main rules)</figcaption></figure>

$$ \frac{\Gamma \vdash M : \sigma \quad \sigma \leq \tau}{\Gamma \vdash M : \tau} (\leq) \qquad \frac{\Gamma \vdash M @ \Delta : \sigma \quad \sigma \leq \tau}{\Gamma \vdash M @ [\tau] \Delta : \tau} (\leq) \qquad \frac{\Gamma \vdash \Delta : \sigma \quad \sigma \leq \tau}{\Gamma \vdash [\tau] \Delta : \tau} (\leq) $$

This completes the remainder of the type assignment $\Lambda_{\leq}^{\sqsubseteq}$ of [BDCd95], and the presentation of the typed system $\Lambda_{\geq}^{\sqsupseteq}$, and of the proof-functional logic $\mathcal{L}_{\leq}^{\sqsubseteq}$, respectively.

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

**Theorem 2 (Equivalence).**

Let $M$ and $\Delta$ and $\Gamma^\Delta$, $\Gamma$, $B$ such that $\iota\Delta\iota \equiv M$. Then:

1. $\Gamma \vdash M : \sigma \text{ iff } \Gamma^\Delta \vdash M @ \Delta : \sigma$;

2. $\Gamma^\Delta \vdash M @ \Delta : \sigma \text{ iff } \Gamma \vdash \Delta : \sigma$;

3. $\Gamma \vdash M : \sigma \text{ iff } \Gamma \vdash \Delta : \sigma$.

*Proof.* Point 1 by upgrading Theorem 10 of [DL10]; point 2 by induction on the structure of derivations, using Definition 1; point 3 by 1,2. $\square$

The next theorem states that adding subtyping as explicit coercions does not break the properties of the extended typed systems.

**Theorem 3 (Conservativity).**

The typed system $\Lambda_{\leq}^{\sqsubseteq}$ and the proof-functional logic $\mathcal{L}_{\leq}^{\sqsubseteq}$, both obtained by extending with the (sub)type theory $\Xi$ and with explicit coercions type rules ($\leq$), preserve subject reduction (parallel-synchronized $\beta$-reduction for $\Lambda_{\geq}^{\sqsupseteq}$), Church-Rosser, strong normalization, unicity of typing, decidability of type reconstruction and of type checking, judgment decidability and isomorphism of typed-untyped derivations.

*Proof.* For proving properties of $\Lambda_{\leq}^{\sqsubseteq}$ we proceeds by upgrading results of Theorems 11, 12 and 19 of [DL10] with the subsumption rule ($\leq$). Properties of $\mathcal{L}_{\leq}^{\sqsubseteq}$ are mostly inherited by $\Lambda_{\geq}^{\sqsupseteq}$ using Theorem 2 or, as for case of subject reduction for $\beta$-, $\mathrm{pr}_i$- and $\mathrm{in}_i$-reductions, is proved by induction on the structure of the derivation. Decidability of subtyping is proved in Theorems 18 and 19. $\square$

## 3 Realizers

We start this section by recalling the logic $\vdash_{NJ}$, as sketched in Figure 4. By NJ we mean the natural deduction presentation of the intuitionistic first-order predicate calculus [Pra65]. Derivations in NJ are trees of judgments $G \vdash_{NJ} A$, where $G$ is a set
of undischarged assumptions, rather than trees of formulas, as in Gentzen's original formulation. Then we extend NJ as follows:

**Definition 4. (Logic NJ(β)).**

Let $\mathbf{P}_{\phi}(x)$ be a unary predicate for each atomic type $\phi$: the natural deduction system for first-order intuitionistic logic NJ(β) extends NJ with untyped lambda-terms and predicates $\mathbf{P}_{\phi}(x)$, the latter being axiomatized via the two Post rules:

$$ \frac{G_{\Gamma} \vdash_{\mathrm{NJ}(\beta)} \mathbf{P}_{\phi}(M) \quad M =_{\beta\eta} N}{G_{\Gamma} \vdash_{\mathrm{NJ}(\beta)} \mathbf{P}_{\phi}(N)} \quad (\beta) \qquad \frac{G_{\Gamma} \vdash_{\mathrm{NJ}(\beta)} \mathbf{P}_{\omega}(M)}{G_{\Gamma} \vdash_{\mathrm{NJ}(\beta)} \mathbf{P}_{\omega}(N)} \quad (Ax_{\omega}) $$

For a given context $\Gamma \triangleq \{x_1:\sigma_1, \dots, x_n:\sigma_n\}$, we associate a logical context $G_{\Gamma} \triangleq r_{\sigma_1}[x_1], \dots, r_{\sigma_n}[x_n]$. Note that $G_{\Gamma, x:\sigma} \equiv G_{\Gamma}, r_{\sigma}[x]$ and $x \notin Fv(G_{\Gamma})$, since $x \notin \mathrm{Dom}(\Gamma)$, by context definition.

In [DdLS16], we provided a foundation for the proof-functional logic $\mathcal{L}^{\cap \cup}$ by extending Mints' provable realizability to cope with intersection and union types, but without subtyping. What follows scale up Mints' realizability to $\mathcal{L}^{\cap \cup}$. The next definition is a reminder of the notion of realizer, as first introduced for intersection types by Mints [Min89], and extended by the authors in [DdLS16].

**Definition 5. (Mints' realizers in NJ(β)).**

Let $\mathbf{P}_{\phi}(x)$ be a unary predicate for each atomic type $\phi$. Then we define the predicates $r_{\sigma}[x]$ for each type $\sigma$ by induction over $\sigma$, as follows:

$$ \begin{array}{l@{\qquad}l} r_{\phi}[x] & \triangleq \mathbf{P}_{\phi}(x) & r_{\sigma_1 \to \sigma_2}[x] \triangleq \forall y. r_{\sigma_1}[y] \supset r_{\sigma_2}[xy] \\ r_{\omega}[x] & \triangleq \top & r_{\sigma_1 \cup \sigma_2}[x] \triangleq r_{\sigma_1}[x] \lor r_{\sigma_2}[x] \\ & & r_{\sigma_1 \cap \sigma_2}[x] \triangleq r_{\sigma_1}[x] \land r_{\sigma_2}[x] \end{array} $$

where $\supset$ denotes implication, $\land$ and $\lor$ are the logical connectives for conjunction and disjunction respectively, that must be kept distinct from $\cap$ and $\cup$. Formulas have the shape $r_{\sigma}[M]$, whose intended meaning is that $M$ is a method for $\sigma$ in the intersection-union type discipline with subtyping.

Intuitively, we write $r_{\sigma}[M]$ to denote a formula in NJ(β), realized by the pure lambda-term $M$ of type $\sigma$ in $\Lambda_{\leq}^{\cap \cup}$. Observe that $M$ is “distilled” by applying the essence function to the typed proof-term $\Delta$, which faithfully encodes the type assignment derivation $\Gamma \vdash \iota\Delta\iota : \sigma$ in $\Lambda_{\leq}^{\cap \cup}$. The next theorem states that the proof-functional logic $\mathcal{L}_{\leq}^{\cap \cup}$ is sound w.r.t. Mints' realizers in NJ(β).

**Lemma 6** ($\Lambda_{\leq}^{\cap \cup}$ versus NJ(β)). If $\Gamma \vdash M : \sigma$, then $G_{\Gamma} \vdash_{\mathrm{NJ}(\beta)} r_{\sigma}[M]$.

*Proof.* By structural induction on the derivation tree of $B \vdash M : \sigma$:

- rules (Var), ($\cup$I), ($\cap$I), ($\cap E$) correspond trivially to (Hyp), ($\lor$I), ($\land$I), and ($\land E$);

- rule ($\cup E$) is derivable from rule ($\lor E$) and a classical substitution lemma;

- it can be showed that all the subtyping rules are derivable in NJ(β), therefore ($\leq$) is derivable;
- rules ($\rightarrow I$) and ($\rightarrow E$) are derivable:

$$ \frac{\frac{G_{\Gamma}, r_{\sigma}[x] \vdash_{\mathrm{NJ}(\beta)} r_{\tau}[M]}{G_{\Gamma} \vdash_{\mathrm{NJ}(\beta)} r_{\sigma}[x] \supset r_{\tau}[M]} (\supset I) \\ \frac{G_{\Gamma} \vdash_{\mathrm{NJ}(\beta)} r_{\sigma \to \tau}[\lambda x.M]}{(\forall I)} \\ \frac{\frac{G_{\Gamma} \vdash_{\mathrm{NJ}(\beta)} r_{\sigma \to \tau}[M]}{G_{\Gamma} \vdash_{\mathrm{NJ}(\beta)} r_{\sigma}[N] \supset r_{\tau}[MN]} (\forall E) \qquad G_{\Gamma} \vdash_{\mathrm{NJ}(\beta)} r_{\sigma}[N]}{(\supset E)} \qquad \supset E) $$

□

Informally speaking, $r_{\sigma}[M]$ can be interpreted as “$M$ is an element of the set $\sigma$”, and the judgment $\sigma_1 \le \sigma_2$ in the (sub)type theory $\Xi$ can be interpreted as $r_{\sigma_1}[x] \vdash_{\mathrm{NJ}(\beta)} r_{\sigma_2}[x]$. As a simple consequence of Lemma 6, we can now state soundness:

**Theorem 7 (Soundness of $\mathrm{NJ}(\beta)$ and $\mathcal{L}_{\leq}^{\cap}$).** If $\Gamma \vdash \Delta : \sigma$ then $G_{\Gamma} \vdash_{\mathrm{NJ}(\beta)} r_{\sigma}[\Delta]$. □

*Proof. Trivial by Lemma 6 and Theorem 2 part 3.*

□

The completeness result, i.e. If $G_{\Gamma} \vdash_{\mathrm{NJ}(\beta)} r_{\sigma}[M]$, then there exists $\Delta$ such that $\Gamma \vdash \Delta : \sigma$ and $\lceil \Delta \rceil \equiv M$ is more tricky because of the presence of the union elimination rule ($\forall E$) in $\mathrm{NJ}(\beta)$. As an example, let $\phi \equiv (\sigma \cup \tau) \cap (\sigma \cup \rho) \to \sigma \cup (\tau \cap \rho)$: with a fairly complex derivation in $\mathrm{NJ}(\beta)$ we can realize $G_{\emptyset} \vdash_{\mathrm{NJ}(\beta)} r_{\phi}[\lambda x.x]$, and then by completeness the type assignment $\emptyset \vdash \lambda x.x : \phi$ should be derivable in [BDCd95], which is not the case without subtyping. We left completeness for a future work.

*Remark 8.*

The type assignment system $\Lambda_{\leq}^{\cap}$ of [BDCd95] was based on the (sub)type theory $\Xi$ (see Definition 3.6 of [BDCd95]): the paper also introduced a stronger (sub)type theory, called $\Pi$, by adding the extra axiom

$$ (15) \qquad \mathbf{P}(\sigma) \Rightarrow \sigma \to \tau \cup \rho \le (\sigma \to \tau) \cup (\sigma \to \rho), $$

where $\mathbf{P}(\sigma)$ is true if $\sigma$ syntactically corresponds to an Harrop formula. However, in $\mathrm{NJ}(\beta)$, the judgment $r_{\sigma \to (\tau \cup \rho)}[x] \vdash_{\mathrm{NJ}(\beta)} r_{(\sigma \to \tau) \cup (\sigma \to \rho)}[x]$ is not derivable because the judgment $A \supset (B \lor C) \vdash_{\mathrm{NJ}(\beta)} (A \supset B) \lor (A \supset C)$ is not derivable in $\mathrm{NJ}$. As such, the (sub)type theory $\Pi$ cannot be overlapped with an interpretation of (sub)types as (sub)sets, as the following example show. The identity function $\lambda x.x$ inhabits the function set $\{a, b\} \to \{a\} \cup \{b\}$ but, by axiom (15), it should also inhabit $\{a, b\} \to \{a\}$ or $\{a, b\} \to \{b\}$, which is clearly not the case.

# 4 Subtyping algorithm

The previous section showed that the proof-functional logic $\mathcal{L}_{\leq}^{\cap}$ is sound w.r.t. the logic $\mathrm{NJ}(\beta)$. The truth of the sequent “$\Gamma \vdash \Delta : \sigma$” complicates its decidability because of the presence of the predicate $\sigma \le \tau$ as a premise in rule (≤): in fact, the subtype system is not an algorithm because of the presence of reflexivity and transitivity rules
that are not syntax-directed. The same subtyping premise can affect the decidability of type checking of $\Lambda_{\leq}^{\cap}$. This section presents a sound and complete algorithm $\mathcal{A}$ for subtyping in the (sub)type theory $\Xi$. In what follows we use the following useful shorthands:

$$ \cap_i (\cup_j \sigma_{i,j}) \triangleq \cap_1 (\cup_1 \sigma_{1,1} \dots \cup_j \sigma_{1,j}) \dots \cap_i (\cup_1 \sigma_{i,1} \dots \cup_j \sigma_{i,j}), \text{ and} $$

$$ \cup_i (\cap_j \sigma_{i,j}) \triangleq \cup_1 (\cap_1 \sigma_{1,1} \dots \cap_j \sigma_{1,j}) \dots \cup_i (\cap_1 \sigma_{i,1} \dots \cap_j \sigma_{i,j}). $$

Those shorthands can also apply to unions of unions, intersections of intersections, intersections of arrows, etc.

Algorithm $\mathcal{A}$ alone has a polynomial complexity, but it requires the types to be in some normal form that will be detailed later. We therefore have a preprocessing phase that is exponential in space. The preprocessing uses the following four subroutines:

- $\mathcal{R}_1$, to simplify the shape of types containing the $\omega$ type: its complexity is linear;

- $\mathcal{R}_2$ (well-known), to transform a type in its conjunctive normal form, denoted by CNF, i.e. types being, roughly, intersection of unions: its complexity is exponential in space;

- $\mathcal{R}_3$ (well-known), to transform a type in its disjunctive normal form, denoted by DNF, i.e. types being, roughly, union of intersections: its complexity is exponential in space;

- $\mathcal{R}_4$, to transform a type in its arrow normal form, denoted by ANF, i.e. types being, roughly, arrow types where all the domains are intersection of ANF and all the codomains are union of ANF: its complexity is exponential in space.

**Definition 9. (Subroutine $\mathcal{R}_1$)**

The term rewriting system $\mathcal{R}_1$ is defined as follows:

- $\omega \cap \sigma$ and $\sigma \cap \omega$ rewrite to $\sigma$;

- $\omega \cup \sigma$ and $\sigma \cup \omega$ rewrite to $\omega$;

- $\sigma \to \omega$ rewrites to $\omega$.

It is easy to verify that $\mathcal{R}_1$ terminates and its complexity is linear. The next definition recall the usual conjunctive/disjunctive normal form with corresponding subroutines $\mathcal{R}_2$ and $\mathcal{R}_3$, and introduce the arrow normal form with his corresponding subroutine $\mathcal{R}_4$.

**Definition 10. (Subroutines $\mathcal{R}_2$ and $\mathcal{R}_3$)**

- A type is in CNF if it has the form $\cap_i (\cup_j \sigma_{i,j})$, and all the $\sigma_{i,j}$ are either atomic types, arrow types, or $\omega$;

- The term rewriting system $\mathcal{R}_2$ rewrites a type in its CNF; it is defined as follows:

- $\sigma \cup (\tau \cap \rho)$ rewrites to $(\sigma \cup \tau) \cap (\sigma \cup \rho)$;

- $(\sigma \cap \tau) \cup \rho$ rewrites to $(\sigma \cup \rho) \cap (\tau \cup \rho)$;

- A type is in DNF if it has the form $\cup_i (\cap_j \sigma_{i,j})$, and all the $\sigma_{i,j}$ are either atomic types, arrow types, or $\omega$;

- The term rewriting system $\mathcal{R}_3$ rewrites a type in its DNF; it is defined as follows:

- $\sigma \cap (\tau \cup \rho)$ rewrites to $(\sigma \cap \tau) \cup (\sigma \cap \rho)$;

- $(\sigma \cup \tau) \cap \rho$ rewrites to $(\sigma \cap \rho) \cup (\tau \cap \rho)$.
It is well documented in the literature that $\mathcal{R}_2$ and $\mathcal{R}_3$ terminate, and that the complexity of those algorithms is exponential.

As you can see in the (sub)type $\Xi$'s rules (11) and (12), intersection and union interact with the arrow type; in order to simplify this, we define the following subroutine:

**Definition 11. (Subroutine $\mathcal{R}_4$)**

- A type is in arrow normal form (ANF) if:

- it is an atomic type or $\omega$;

- it is an arrow type in the form $(\cap_i \sigma_i) \rightarrow (\cup_j \tau_j)$, where the $\sigma_i$ and $\tau_j$ are ANFs;

- The term rewriting system $\mathcal{R}_4$ rewrites an arrow type into an intersection of ANF; it is defined as follows:

- $\sigma \rightarrow \tau$ rewrites to $\mathcal{R}_3(\sigma) \rightarrow \mathcal{R}_2(\tau)$;

- $\cup_i \sigma_i \rightarrow \cap_j \tau_j$ rewrites to $\cap_i (\cap_j (\sigma_i \rightarrow \tau_j))$.

Since $\mathcal{R}_2$ and $\mathcal{R}_3$ terminate, $\mathcal{R}_4$ terminates and its complexity is exponential. The next lemma ensures we can safely use the $\mathcal{R}_{1,2,3,4}$ subroutines in the preprocessing, because they preserve type equivalence, denoted by $\sim$. Let $\sigma \sim \tau$ iff $\sigma \le \tau$ and $\tau \le \sigma$.

**Lemma 12.** For all the term rewriting systems $\mathcal{R}_{1,2,3,4}$ we have that $R(\sigma) \sim \sigma$.

*Proof.* Each rewriting rule rewrites a term into an equivalent ($\sim$) term. □

We can now define how the types are being preprocessed before being fed to the algorithm $\mathcal{A}$.

**Definition 13.**

- A type is in disjunctive arrow normal form (DANF) if it is in DNF and all the arrow type subterms are in ANF;

- A type is in conjunctive arrow normal form (CANF) if it is in CNF and all the arrow type subterms are in ANF.

Let $\sigma \le \tau$ be an instance of the subtyping problem. The preprocessing algorithm rewrites $\sigma$ into a DANF by applying $\mathcal{R}_3 \circ \mathcal{R}_4 \circ \mathcal{R}_1$, and $\tau$ into a CANF by applying $\mathcal{R}_2 \circ \mathcal{R}_4 \circ \mathcal{R}_1$.

## 4.1 The algorithm $\mathcal{A}$

Our algorithm $\mathcal{A}$ is composed of two mutually inductive functions, called $\mathcal{A}_1$ and $\mathcal{A}_2$. It proceeds as follows: $\sigma \le \tau$ is preprocessed into $\cup_i (\cap_j \sigma_{i,j}) \le \cap_h (\cup_k \tau_{h,k})$, where all the $\sigma_{i,j}, \tau_{h,k}$ are in ANF; it is then processed by $\mathcal{A}_1$, which accepts or rejects it.

**Definition 14. (Main function $\mathcal{A}_1$).**

*input*: $\cup_i (\cap_j \sigma_{i,j}) \le \cap_h (\cup_k \tau_{h,k})$ where all the $\sigma_{i,j}, \tau_{h,k}$ are ANF; *output*: boolean.

- if $\cap_h (\cup_k \tau_{h,k})$ is $\omega$, then accept, else

if for all $i$ and $h$, there exists some $j$ and some $k$, such that $\mathcal{A}_2(\sigma_{i,j} \le \tau_{h,k})$ is true, then accept, else reject.

**Definition 15. (Subtyping function $\mathcal{A}_2$).**

*input*: $\sigma \le \tau$, where $\sigma \ne \omega$ and $\tau \ne \omega$ are ANFs; *output*: boolean.
- Case $\omega \le \phi$: reject;

- Case $\omega \le \sigma \to \tau$: reject;

- Case $\phi \le \phi'$: if $\phi \equiv \phi'$ then accept, else reject;

- Case $\phi \le \sigma \to \tau$: reject;

- Case $\sigma \to \tau \le \phi$: reject;

- Case $\sigma \to \tau \le \sigma' \to \tau'$: if $A_1(\sigma' \le \sigma)$ and $A_1(\tau \le \tau')$, then accept, else reject.

The following two lemmas will be used to prove soundness and completeness of the algorithm $A_1$.

**Lemma 16.**

1. $\sigma \cup \tau \le \rho \text{ iff } \sigma \le \rho \text{ and } \tau \le \rho$;

2. $\sigma \le \tau \cap \rho \text{ iff } \sigma \le \tau \text{ and } \sigma \le \rho$.

*Proof.* The two parts can be proved by examining the subtyping rules of the (sub)type theory $\Xi$. $\square$

**Lemma 17.**

If all the $\sigma_i$ and $\tau_j$ are ANFs, then:

1. If $\exists j, \cap_i \sigma_i \le \tau_j$, then $\cap_i \sigma_i \le \cup_j \tau_j$;

2. If $\exists i, \sigma_i \le \cup \tau_j$, then $\cap_i \sigma_i \le \cup_j \tau_j$.

*Proof.* The two parts can be proved by induction on the subtyping rules of the (sub)type theory $\Xi$ using the ANF definition. $\square$

The soundness proof is now straightforward.

**Theorem 18 ($A_1, A_2$'s Soundness).**

1. Let $\sigma$ (resp. $\tau$) be in DANF (resp. CANF). If $A_1(\sigma \le \tau)$, then $\sigma \le \tau$;

2. Let $\sigma$ and $\tau$ be in ANF, such that $\tau \not\equiv \omega$. If $A_2(\sigma \le \tau)$, then $\sigma \le \tau$.

*Proof.* The proof follows the algorithm, therefore it proceeds by mutual induction.

1. By case analysis on the algorithm $A_1$ using Lemmas 16 and 17, and part 2;

2. By case analysis on the algorithm $A_2$, and by looking at the subtyping rules. $\square$

**Theorem 19 ($A_1, A_2$'s Completeness).**

1. For any type $\sigma'$, $\tau'$ such that $\sigma' \le \tau'$, let $\cup_i(\cap_j \sigma_{i,j}) \equiv \mathbb{R}_3 \circ \mathbb{R}_4 \circ \mathbb{R}_1(\sigma')$ and $\cap_h(\cup_k \tau_{h,k}) \equiv \mathbb{R}_2 \circ \mathbb{R}_4 \circ \mathbb{R}_1(\tau')$. We have that $A_1(\cup_i(\cap_j \sigma_{i,j}) \le \cap_h(\cup_k \tau_{h,k}))$;

2. Let $\sigma$ and $\tau$ be in ANF, such that $\tau \not\asymp \omega$. If $\sigma \le \tau$, then $A_2(\mathbb{R}_1(\sigma) \le \mathbb{R}_1(\tau))$.

*Proof.* We know by Lemma 12 that rewriting preserves subtyping, therefore as $\sigma' \le \tau'$, we know that $\cup_i(\cap_j \sigma_{i,j}) \le \cup_j \cap_h(\cup_k \tau_{h,k})$. The proof proceeds by mutual induction.

1. The proof of this point relies on Lemmas 16 and 17: it is not shown by lack of space (see [LS17]);

2. - Case $\omega \le \tau$: by hypothesis, $\omega \not\le \tau$, so this case is absurd;

- Case $\phi \le \phi'$: we can show that $\phi \equiv \phi'$;

- Case $\sigma \to \tau \le \phi$: it can be proved that this case is absurd;

- Case $\phi \le \sigma \to \tau$: we can show that $\phi \le \sigma \to \tau \text{ iff } \sigma \to \tau \sim \omega$, and this contradicts the hypothesis $\sigma \to \tau \not\asymp \omega$: this is absurd;

- Case $\sigma \to \tau \le \sigma' \to \tau'$: we can show that $\tau \le \tau'$, and $\sigma' \le \sigma$. We conclude by induction hypothesis. $\square$
# 5 Conclusions

We mention some future research directions.

Completeness of $\mathcal{L}^{\cap}$. We have not proven yet completeness for our logic towards NJ($\beta$), but we conjecture that if $G_{\Gamma}$ is a logical context and $G_{\Gamma} \vdash_{\text{NJ}(\beta)} r_{\sigma}[M]$, then $\Gamma \vdash M : \sigma$.

Strong/Relevant Implication is another proof-functional connective: as well explained in [BM94], 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”. Relevant implication is well-known in the literature, corresponding to Meyer and Routley’s Minimal Relevant Logic $B^+$ [MR72]. Following our parallelism between type systems for lambda-calculi à la Curry, à la Church, and logics, we could conjecture that strong implication, denoted by $\supset_r$ in the logic, by $\rightarrow_r$ in the type theory, and by $\lambda_r$ in the typed lambda-calculus, can lead to the following type (assignment) rules, proof-functional logical inference, and Mints’ realizer in NJ($\beta$), respectively:

$$ \frac{\frac{\Gamma \vdash l : \sigma \rightarrow \tau \quad (\rightarrow_r I)}{\Gamma \vdash l : \sigma \rightarrow_r \tau}}{\Gamma, x:\sigma \vdash \Delta : \tau \quad \forall \Delta_l \equiv x \quad (\rightarrow_r I)} \qquad \frac{\frac{\Gamma, x:\sigma \vdash x @ \Delta : \tau}{\Gamma \vdash \lambda x.x @ \lambda_r x:\sigma.\Delta : \sigma \rightarrow_r \tau}}{G_{\Gamma} \vdash r_{\sigma \rightarrow \tau}[l] \quad (\supset_r I)} $$

As showed in Remark 8, even a stronger (sub)type theory of $\Xi$ (i.e. the (sub)theory $\Pi$ of [BDCd95]) cannot be overlapped with a sound and complete interpretation of (sub)types as (sub)sets. We conjecture that, by extending the proof-functional logic with relevant implication $(\mathcal{L}^{\cap \rightarrow_r})$, we could achieve completeness, by combining explicit coercions and relevant abstractions, as the following derivation shows:

$$ \frac{\frac{\Gamma \vdash x : \sigma \quad \sigma \leq \tau}{\Gamma \vdash (\tau)x : \tau} \quad \forall (\tau)x_l \equiv x}{\Gamma \vdash \lambda_r x : \sigma.(\tau)x : \sigma \rightarrow_r \tau} \quad \Gamma \vdash \Delta : \sigma \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \Gamma \vdash (\lambda_r x : \sigma.(\tau)x) \Delta : \tau $$

Dependent Types / Logical Frameworks. Our aim is to build a small logical framework à la Edinburgh Logical Framework [HHP93], featuring dependent types and proof-functional logical connectives. We conjecture that, in addition to the usual machinery dealing with dependent types and a suitable upgrade of the essence function, the following typing rules can be good candidates for a proof-functional LF extension:

$$ \frac{\Gamma, x:\sigma \vdash \Delta : \tau \quad \forall \Delta_l \equiv x \quad (\Pi^r I)}{\Gamma \vdash \lambda^r x:\sigma.\Delta : \Pi^r x:\sigma.\tau} \qquad \frac{\Gamma \vdash \Delta_1 : \sigma \quad \Gamma \vdash \Delta_2 : \tau \quad \forall \Delta_1 l \equiv \forall \Delta_2 l}{\Gamma \vdash (\Delta_1, \Delta_2) : \sigma \cap \tau} \quad (\cap I) \\ \frac{\Gamma \vdash \Delta_1 : \Pi y:\sigma.\rho [\text{in}_1^\tau y/x] \quad \forall \Delta_1 l \equiv \forall \Delta_2 l}{\Gamma \vdash \Delta_2 : \Pi y:\tau.\rho [\text{in}_2^\sigma y/x] \quad \Gamma \vdash \Delta_3 : \sigma \cup \tau} \quad (\cup E) \\ \frac{\Gamma \vdash [\Delta_1, \Delta_2] \Delta_3 : \rho [\Delta_3/x]}{\Gamma \vdash [\Delta_1, \Delta_2] \Delta_3 : \sigma [\Delta_3/x]} \quad (\cup I) $$
Studying the behavior of proof-functional connectives would be beneficial to existing interactive theorem provers such as Coq or Isabelle, and dependently typed programming languages such as Agda, Beluga, Epigram, or Idris.

*Prototype Implementation.* We are currently implementing a small kernel for a logical framework featuring union and intersection types, as the $Λ^{∩∪}$ calculus and the proof-functional logic $L^{∩∪}$ does. The actual type system also features an experimental implementation of dependent-types à la LF following the above type rules, and of a *Read-Eval-Print-Loop* (REPL). We will put our future efforts to integrate our algorithm $A$ to the type checker engine. We conjecture that our subtyping algorithm could be rewritten nondeterministically for an alternating Turing machine in polynomial time: this would mean that this problem is in PSPACE. This could be coherent with the fact that inclusion problem for regular tree languages is PSPACE-complete [Sei90]. The aim of the prototype is to check the expressiveness of the proof-functional nature of the logical engine in the sense that when the user must prove e.g. a strong conjunction formula $σ_1 ∩ σ_2$ obtaining (mostly interactively) a witness $Δ_1$ for $σ_1$, the prototype can “squeeze” the proof-functional essence $M$ of $Δ_1$ to accelerate, and in some case automatize, the construction of a witness $Δ_2$ proof for the formula $σ_2$ having the same essence $M$ of $Δ_1$. Existing proof assistants could get some benefit if extended with a proof-functional logic. We are also started an encoding of the proof-functional operators of intersection and union in Coq. The actual state of the prototype can be retrieved at https://github.com/cstolze/Bull.

**Acknowledgment.** We are grateful to Ugo de'Liguoro, Daniel Dougherty, and the anonymous referees for their useful comments and suggestions.

## References

Aik99. Alexander Aiken. Introduction to set constraint-based program analysis. *Sci. Comput. Program.*, 35(2):79–111, 1999.

AW93. Alexander Aiken and Edward L. Wimmers. Type inclusion constraints and type inference. In *FPCA*, pages 31–41. ACM, 1993.

Bar84. Henk P. Barendregt. *The λ-Calculus*. Studies in logic and the foundations of mathematics, North-Holland, 1984.

Bar13. Henk P. Barendregt. *The λ-Calculus with Types*. Association for Symbolic Logic, Cambridge University Press, 2013.

BCDC83. Henk P. Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A Filter Lambda Model and the Completeness of Type Assignment. *Journal of Symbolic Logic*, 48(4):931–940, 1983.

BCL92. Kim B. Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. *Mathematical Structures in Computer Science*, 2(2):231–247, 1992.

BDCd95. Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de'Liguoro. Intersection and union types: syntax and semantics. *Inf. Comput.*, 119(2):202–230, 1995.

BM94. Franco Barbanera and Simone Martini. Proof-functional connectives and realizability. *Archive for Mathematical Logic*, 33:189–211, 1994.

Dam94. Flemming M. Damm. Subtyping with union types, intersection types and recursive types. In *TACS*, pages 687–706, 1994.
DCGV97. Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, and Betti Venneri. The "relevance" of intersection and union types. *Notre Dame Journal of Formal Logic*, 38(2):246–269, 1997.

DdLS16. Daniel J. Dougherty, Ugo de'Liguoro, Luigi Liquori, and Claude Stolze. A realizability interpretation for intersection and union types. In *APLAS*, volume 10017 of *Lecture Notes in Computer Science*, pages 187–205. Springer, 2016.

DL10. Daniel J. Dougherty and Luigi Liquori. Logic and computation in a lambda calculus with intersection and union types. In *LPAR*, volume 6355 of *Lecture Notes in Computer Science*, pages 173–191. Springer, 2010.

DP04. Joshua Dunfield and Frank Pfenning. Tridirectional typechecking. In *POPL*, pages 281–292, 2004.

Dun14. Joshua Dunfield. Elaborating intersection and union types. *J. Funct. Program.*, 24(2-3):133–165, 2014.

FCB08. Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types. *J. ACM*, 55(4):19:1–19:64, 2008.

HHP93. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. *J. ACM*, 40(1):143–184, 1993.

Hin82. J. Roger Hindley. The simple semantics for Coppo-Dezani-Sallé types. In *International Symposium on Programming*, pages 212–226, 1982.

How80. William A. Howard. The Formulae-as-Types Notion of Construction. In *To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism*, pages 479–490. Academic press, 1980.

LE85. Edgar G. K. Lopez-Escobar. Proof functional connectives. In *Methods in Mathematical Logic*, volume 1130 of *Lecture Notes in Mathematics*, pages 208–221. Springer-Verlag, 1985.

LR07. Luigi Liquori and Simona Ronchi Della Rocca. Intersection typed system à la Church. *Information and Computation*, 9(205):1371–1386, 2007.

LS17. Luigi Liquori and Claude Stolze. A Decidable Subtyping Logic for Intersection and Union Types. Research report, Inria, https://hal.inria.fr/hal-01488428, 2017.

Min89. Grigori Mints. The completeness of provable realizability. *Notre Dame Journal of Formal Logic*, 30(3):420–441, 1989.

MPS86. David B. MacQueen, Gordon D. Plotkin, and Ravi Sethi. An ideal model for recursive polymorphic types. *Information and Control*, 71(1/2):95–130, 1986.

MR72. Robert K. Meyer and Richard Routley. Algebraic analysis of entailment I. *Logique et Analyse*, 15:407–428, 1972.

Pfe93. Frank Pfenning. Refinement types for logical frameworks. In *TYPES*, pages 285–299, 1993.

Pie91. Benjamin C. Pierce. *Programming with intersection types, union types, and bounded polymorphism*. PhD thesis, Technical Report CMU-CS-91-205, Carnegie Mellon University, 1991.

Pot80. Garrel Pottinger. A type assignment for the strongly normalizable λ-terms. In *To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism*, pages 561–577. Academic Press, 1980.

Pra65. Dag Prawitz. *Natural deduction: a proof-theoretical study*. PhD thesis, Almqvist & Wiksell, 1965.

Rey96. John C. Reynolds. Design of the programming language Forsythe. Technical Report CMU-CS-96-146, Carnegie Mellon University, 1996.

Sei90. Helmut Seidl. Deciding equivalence of finite tree automata. *Journal of Symbolic Logic*, 19(3):424–437, 1990.