Kaustuv Chaudhuri

Carlos Olarte

Elaine Pimentel

Joëlle Despeyroux

Hybrid Linear Logic, revisited

Introduction

Logical frameworks are adequate tools for specifying proof systems, since they support levels of abstraction that facilitate writing declarative specifications of object-level logical systems. Thus designing suitable logical frameworks for adequately specifying different proof systems has become one of the main tasks for many logicians working in computer science.

Among the many frameworks that have been used for the specification of proof systems, linear logic [START_REF] Girard | Linear logic[END_REF] (LL) is one of the most successful ones. This is mainly because LL is resource conscious and, at the same time, it can internalize classical and intuitionistic behaviors (see, for example, [START_REF] Miller | A formal framework for specifying sequent calculus proof systems[END_REF][START_REF] Cervesato | A Linear Logical Framework[END_REF]). However, since specifications of object-level systems into the logical framework should be natural and direct, there are some features that often cannot be adequately captured in LL, e.g. modalities different from the ones present in LL.

Extensions of LL, or its intuitionistic version ILL [START_REF] Girard | Linear logic[END_REF], have been proposed in order to fill this gap, hence having stronger logical frameworks that preserve the elegant properties of linear logic as the underlying logic. Two of such extensions are HyLL (Hybrid Linear Logic) [START_REF] Despeyroux | A hybrid linear logic for constrained transition systems[END_REF], an extension of ILL, and SELL (Subexponential Linear Logic) [START_REF] Vincent Danos | The structure of exponentials: Uncovering the dynamics of linear logic proofs[END_REF][START_REF] Nigam | Algorithmic specifications in linear logic with subexponentials[END_REF], an extension of ILL/LL 1 . These logics have been extensively used for specifying systems that exhibit modalities such as temporal or spatial ones. The difference between HyLL and SELL relies on the way modalities are handled.

In HyLL, truth judgments are labeled by worlds and two hybrid connectives relate worlds with formulas: the satisfaction at which states that a proposition is true at a given world, and the localization ↓ which binds a name for the (current) world the proposition is true at. These constructors allow for the specification of modal connectives such as A (A is true written using an infix arrow τ → τ . A type is a predicate type if it is of the form τ 1 → • • • → τ n → o, where n ≥ 0. Terms are simply typed λ-terms and we identify two terms up to the usual α, β, and η-conversions. The substitution notation B[t/x] denotes the λ-normal form of the β-redex (λx.B)t.

The set of linear logic formulas is given by the following grammar: ,⊥, respectively; and the additive version of these connectives, which are written as &, , ⊕, 0, respectively; the exponentials ! and ?; and the (typed) universal and existential quantifiers ∀ τ and ∃ τ . In the quantifiers, the syntactic variable τ can range over all non-predicate types: ∀ τ and ∃ τ both have type (τ → o) → o. The expressions ∀ τ λx.B and ∃ τ λx.B are abbreviated as the more usual ∀ τ x.B and ∃ τ x.B. From this point on, we will drop the subscript τ when it is not important or it can be determined from context. Formulas are taken to be in negation normal form using the standard classical linear logic dualities, e.g., (F ⊗ G) ⊥ ≡ F ⊥ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ?) and positive (⊗, 1, ⊕, 0, ∃, !). Note that the dual of a negative connective is positive and vice-versa. In general, the introduction rules for negative connectives are all invertible, meaning that the conclusion of any of these introduction rules is equivalent to its premises. The introduction rules for the positive connectives are not necessarily invertible. The notions of negative and positive polarities are extended to formulas in the natural way by considering the outermost connective. Although any bias can be assigned to atomic formulas, this work will consider only negative atoms.

F, G ::= p( t) | p( t) ⊥ | 1 | 0 | | ⊥ | F ⊗ G | F . .
The focused system LLF for classical linear logic is presented in Figure 1. There are two kinds of arrows in this proof system: ⇓ and ⇑, and a pair of contexts to the left of the arrows: Γ is a set of formulas whose main connective is a question-mark (being hence the unbounded context), while ∆ is a multi-set of linear formulas, behaving as the bounded context. Sequents with the ⇓ arrow belong to the positive phase and introduce the logical connective of the "focused" formula (the one to the right of the arrow). Building proofs of such sequents may require non-invertible proof steps to be taken. Sequents with the ⇑ arrow belong to the negative phase and decompose the multiset of formulas on the right of the arrow in such a way that only inference rules over negative formulas are applied; the others are "stored" in the linear context using the rule R ⇑. The structural rules D 1 , D 2 and R ⇓ make the transition between negative and positive phases. The positive phase begins by choosing a positive formula F on which to focus (using D 1 , D 2 ). Positive rules are applied to F until either: 1 or a negated atom is encountered (and the proof must end by applying the initial rules); or the promotion rule (!) is applied; or a negative subformula is encountered and the proof switches to the negative phase (using R ⇓).

This change of phases on proof search is particularly interesting when the focused formula is a bipole [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF].

Definition 2.1 (Bipoles). We call a monopole a linear logic formula that is built up from atoms and occurrences of the negative connectives, with the restriction that ? has atomic scope. Bipoles, on the other hand, are positive formulas built from monopoles and negated atoms using only positive connectives, with the additional restriction that ! can only be applied to a monopole. where the F i,j are either atoms or the result of applying ? to an atomic formula. Similarly, bipoles can be rewritten as formulas of the form

∃x 1 . . . ∃x p [⊕ i=1,...,n ⊗ j=1,...,mi G i,j ],
where G i,j are either negated atoms, monopole formulas, or the result of applying ! to a monopole formula. Notice that the units , 0, ⊥, and 1 are 0-ary versions of &, ⊕, Given this normal representation of bipoles and according to the focusing discipline, it turns out that, once introduced, a bipole is completely decomposed into its atomic subformulas, a fact illustrated by the following bipole derivation.

• • • • • • Γ ; ∆ ⇑ • Γ; ∆ ⇑ . . . .
i,j ] [!] • • • Γ; ∆ ⇓ ∃x 1 . . . ∃x t [⊕ i=1,...,k ⊗ j=1,...,qi G i,j ] [∃, ⊕, ⊗]
Here p i,j is atomic for all i, j. If the connective ! is not present, then the rule ! is replaced by the rule R ⇓. Notice that the derivation above contains a single positive and a single negative phase. This two phase decomposition will enable us to adequately capture the application of object-level inference rules as will be shown in Section 3.

Negative rules

Γ; ∆ ⇑ L Γ; ∆ ⇑ ⊥, L [⊥] Γ; ∆ ⇑ F, G, L Γ; ∆ ⇑ F . . . .
Γ; ∆ ⇑ ?F, L [?] Γ; ∆ ⇑ , L [ ] Γ; ∆ ⇑ F, L Γ; ∆ ⇑ G, L Γ; ∆ ⇑ F & G, L [&] Γ; ∆ ⇑ F [y/x], L Γ; ∆ ⇑ ∀x.F, L [∀]
Positive rules

Γ; • ⇓ 1 [1] Γ; ∆ 1 ⇓ F Γ; ∆ 2 ⇓ G Γ; ∆ 1 , ∆ 2 ⇓ F ⊗ G [⊗] Γ; ∆ ⇓ F i Γ; ∆ ⇓ F 1 ⊕ F 2 [⊕ i ] Γ; ∆ ⇓ F [t/x] Γ; ∆ ⇓ ∃x.F [∃] Γ; • ⇑ F Γ; • ⇓ ! F [!]
Identity, Decide, and Release rules

Γ; p( t) ⇓ p( t) ⊥ [I 1 ] Γ, p( t); • ⇓ p( t) ⊥ [I 2 ] Γ; ∆ ⇓ P Γ; ∆, P ⇑ • [D 1 ] Γ, P ; ∆ ⇓ P Γ, P ; ∆ ⇑ • [D 2 ]
In [D 1 ] and [D 2 ], P is not an atom.

Γ; ∆, P a ⇑ L Γ; ∆ ⇑ P a , L [R ⇑]
provided that P a is positive or an atom

Γ; ∆ ⇑ N Γ; ∆ ⇓ N [R ⇓]
provided that N is negative Figure 1: Focused proof linear logic system LLF. Γ is a set, ∆ is a multiset and L is a list of formulas.

ILL [START_REF] Girard | Linear logic[END_REF], the intuitionistic version of LL, is obtained as usual by restricting, in the two sided presentation of LL, the right multiset so to have exactly one formula. Hence the system ILL does not allow the connectives and ? and the unit ⊥, and the rules are the ones for (the 2-sided presentation of) LL restricted accordingly, having explicit rules for the linear implication -•. The specification and verification of systems may use intuitionistic systems (as in e.g., [NM09, dMDF14, Nig14, CPT16, CR15, NOP17, OPR18]), or classical systems (see e.g., [START_REF] Nigam | Specifying proof systems in linear logic with subexponentials[END_REF][START_REF] Miller | A formal framework for specifying sequent calculus proof systems[END_REF][START_REF] Nigam | An extended framework for specifying and reasoning about proof systems[END_REF]). In this work, we will specify object logics in LL based systems.

Hybrid Linear Logic

Hybrid Linear Logic (HyLL) is a conservative extension of ILL where the truth judgments are labeled by worlds representing constraints on states and state transitions. Judgments of HyLL are of the form "A is true at world w", abbreviated as A @ w. Particular choices of worlds produce particular instances of HyLL, e.g., A @ t can be interpreted as "A is true at time t". HyLL was first proposed in [START_REF] Despeyroux | A hybrid linear logic for constrained transition systems[END_REF] and it has been used as a logical framework for specifying modalities as well as biological systems [START_REF] De | A logical framework for systems biology[END_REF]. Formally, worlds are defined as follows.

Definition 2.2 (HyLL worlds). A constraint domain W is a monoid structure W, ., ι . The elements of W are called worlds and its reachability relation : W × W is defined as u w iff there exists v ∈ W such that u.v = w.

The identity world ι is the -initial and it is intended to represent the lack of any constraints. Thus, the ordinary first-order ILL can be embedded into any instance of HyLL by setting all world labels to the identity. A typical example of constraint domain is T = IN , +, 0 , representing instants of time.

Formulas in HyLL are constructed from atomic propositions, connectives of first-order intuitionistic linear logic and the following two hybrid connectives: satisfaction (at), which states that a proposition is true at a given world (w, ι, u.v, . . .), and localization (↓), which binds a name for the current world where the proposition is true at. More precisely, formulas in HyLL are built from:

A, B ::= p( t) | A ⊗ B | 1 | A -• B | A & B | | A ⊕ B | 0 | !A | ∀x. A | ∃x. A | (A at w) | ↓ u. A | ∀u. A | ∃u. A
Note that world u is bounded in the propositions ↓ u. A, ∀u. A and ∃u. A. World variables cannot be used in terms, and neither can term variables occur in worlds. This restriction is important for the modular design of HyLL because it keeps purely logical truth separate from constraint truth. We note that ↓ and at commute freely with all non-hybrid connectives [START_REF] Despeyroux | A hybrid linear logic for constrained transition systems[END_REF].

The sequent calculus presentation of HyLL uses sequents of the form Γ; ∆ C @ w where Γ (unbounded context) is a set and ∆ (linear context) is a multiset of judgments of the form A @ w. Note that in a judgment A @ w and in a proposition A at w, w can be any expression in W, not only a variable.

Judgmental rules

Γ; p( t) @ w p( t) @ w [init] Γ, A @ u; ∆, A @ u C @ w Γ, A @ u; ∆ C @ w [copy]
Multiplicative rules

Γ; ∆ A @ w Γ; ∆ B @ w Γ; ∆, ∆ A ⊗ B @ w [⊗R] Γ; ∆, A @ u, B @ u C @ w Γ; ∆, A ⊗ B @ u C @ w [⊗L] Γ; • 1 @ w [1R] Γ; ∆ C @ w Γ; ∆, 1@ u C @ w [1L] Γ; ∆, A @ w B @ w Γ; ∆ A -• B @ w [-•R] Γ; ∆ A @ u Γ; ∆ , B @ u C @ w Γ; ∆, ∆ , A -• B @ u C @ w [-•L] Additive rules Γ; ∆ @ w [ R] Γ; ∆, 0 @ u C @ w [0L] Γ; ∆ A @ w Γ; ∆ B @ w Γ; ∆ A & B @ w [&R] Γ; ∆, A i @ u C @ w Γ; ∆, A 1 & A 2 @ u C @ w [&L i ] Γ; ∆ A i @ w Γ; ∆ A 1 ⊕ A 2 @ w [⊕R i ] Γ; ∆, A @ u C @ w Γ; ∆, B @ u C @ w Γ; ∆, A ⊕ B @ u C @ w [⊕L]
Quantifier rules

Γ; ∆ A @ w Γ; ∆ ∀α. A @ w [∀R] Γ; ∆, A[τ /α] @ u C @ w Γ; ∆, ∀α. A @ u C @ w [∀L] Γ; ∆ A[τ /α] @ w Γ; ∆ ∃α. A @ w [∃R] Γ; ∆, A @ u C @ w Γ; ∆, ∃α. A @ u C @ w [∃L]
In ∀R and ∃L, α is assumed to be fresh with respect to Γ, ∆, and C.

In ∃R and ∀L, τ stands for a term or world, as appropriate. The inference rules are depicted in Figure 2. Note that (A at u) is a mobile proposition: it carries with it the world at which it is true. Both introduction rules for the the other hybrid connective, ↓, bind the current world. Weakening and contraction are admissible rules for the unbounded context.

Exponential rules

Γ; • A @ w Γ; • !A @ w [! R] Γ, A @ u; ∆ C @ w Γ; ∆, !A @ u C @ w [! L] Hybrid connectives Γ; ∆ A @ u Γ; ∆ (A at u) @ w [at R] Γ; ∆, A @ u C @ w Γ; ∆, (A at u) @ v C @ w [at L] Γ; ∆ A[w/u] @ w Γ; ∆ ↓ u.A @ w [↓ R] Γ; ∆, A[v/u] @ v C @ w Γ; ∆, ↓ u.A @ v C @ w [↓ L]
The most important structural properties are the admissibility of the general identity and cut theorems. While the first provides a syntactic completeness theorem for the logic, the latter guarantees consistency (i.e. that there is no proof of .; . 0 @ w).

Theorem 2.1 (Identity/Cut [START_REF] Despeyroux | A hybrid linear logic for constrained transition systems[END_REF]).

1. Γ; A @ w A @ w.

2. If Γ; ∆ A @ u and Γ; ∆ , A @ u C @ w, then Γ; ∆, ∆ C @ w.

If Γ;

• A @ u and Γ, A @ u; ∆ C @ w, then Γ; ∆ C @ w.

HyLL is conservative with respect to intuitionistic linear logic: as long as no hybrid connectives are used, the proofs in HyLL are identical to those in ILL. Moreover, HyLL is more expressive than S5, as it allows direct manipulation of the worlds using the hybrid connectives, while HyLL's δ connective (see Section 5) is not definable in S5.

Finally, we also note that HyLL admits a complete focused proof system. The interested reader can find proofs and further meta-theoretical theorems about HyLL in [START_REF] Despeyroux | A hybrid linear logic for constrained transition systems[END_REF].

Relative Expressiveness Power of HyLL

Different frameworks can be more or less adequate for specifying different systems. While very specific frameworks often provide better encodings for a small range of systems, general frameworks can handle more systems, sometimes not efficiently or in a natural way. Therefore, finding frameworks that are general enough while still adequate and efficient is a key issue. With that in mind, we will compare HyLL with two other LL based frameworks: LL itself and linear logic with subexponentials (SELL).

We start by proving that HyLL's axioms and rules can be adequately specified in LL. It turns out that any interpretation of a system into another must be adequate, in the sense that there must be a 1-1 relation between the sets of interpreted objects with the set of their interpretations. The level of adequacy can then determine how tight are those systems. We show that our encoding has the highest possible level of adequacy (on the level of derivations -see [START_REF] Nigam | A framework for proof systems[END_REF]), so that one step of derivation in HyLL corresponds to one focused step in LL. This means that every proof in HyLL can be exactly mimicked by a derivation in LLF. We note, however, that HyLL enables for more semantical driven specifications when compared to LL, as it will be discussed in Section 5.

Since linear logic with subexponentials (SELL) is a conservative extension of LL, the specification of HyLL into LL trivially implies that HyLL can be similarly encoded in SELL as well. Our approach in Section 3.2, however, will be entirely different: we will interpret worlds as subexponentials, hence having a better meta level understanding of the behavior of worlds in HyLL.

HyLL and LL

We briefly recapitulate the basic concepts of the specification of sequent-style calculi in LLF (see [START_REF] Miller | A formal framework for specifying sequent calculus proof systems[END_REF] for a more detailed presentation). Let obj be the type of object-level formulas and let In that way, the • and • predicates identify which object-level formulas appear on which side of the sequent: brackets down for left (useful mnemonic: for "left") and brackets up for right, while the double brackets • identify formulas in the (left) unbounded context.

Inference rules are specified as a rewriting clause that replaces the active formula in the conclusion by the active formulas in the premises. The linear logic connectives indicate how these object level formulas are connected: contexts are copied (&) or split (⊗), in different inference rules (⊕) or in the same sequent (

. ). As a matter of example, the additive version of the inference rules for conjunction in intuitionistic logic

Γ, A -→ C Γ, A ∧ B -→ C ∧ L1 Γ, B -→ C Γ, A ∧ B -→ C ∧ L2 Γ -→ A Γ -→ B Γ -→ A ∧ B ∧ R
can be specified as the following bipoles:

∧ L : ∃A, B.( A ∧ B ⊥ ⊗ ( A ⊕ B )) ∧ R : ∃A, B.( A ∧ B ⊥ ⊗ ( A & B ))
The following definition shows how to encode HyLL inference rules into LL.

Definition 3.1 (HyLL rules into LL). Let w, d, h and o denote, respectively, the types for worlds, (first-order) objects, HyLL formulas and LL formulas. Let • , • and • be predicates of the type h → w → o and A, B, C have, respectively, types w → h, d → h and h. The encoding of HyLL inference rules into LL is depicted in Figure 3 (we omit the encoding of most of the linear logic connectives that can be found in [START_REF] Miller | A formal framework for specifying sequent calculus proof systems[END_REF]). Observe that left and right inference rules for the hybrid connectives (at and ↓) are the same (Figure 2). This is reflected in the duality of the encoding where we only replace • with • . Observe also that the inference rules for the quantifiers (first-order and worlds) look the same. The difference is on the type of the variables involved. Since A has type w → h, the encoding clause ∀R(W ) guarantees that the variable v has type w. Analogously, since B has type d → h, then x has type d in the clause ∀R(F ). This neat way of controlling the behavior of objects by using types is also inherited by the encoding of the other object level inference rules.

-• L : ∃C, C , H, w, v.( (C -• C )@w ⊥ ⊗ H@v ⊥ ⊗ C@w ⊗ ( C @
H@v )) -• R : ∃C, C , w.( (C -• C )@w ⊥ ⊗ ( C@
C @w )) ! L : ∃C, w.( !C@w ⊥ ⊗? C@w ) ! R : ∃C, w.( !C@w ⊥ ⊗! C@w ) Init : ∃C, w.( C@w ⊥ ⊗ C@w ⊥ ) Copy : ∃C, w.( C@w ⊥ ⊗ C@w ) at R : ∃C, u, w.( (C at u)@w ⊥ ⊗ C@u ) at L : ∃C, u, w.( (C at u)@w ⊥ ⊗ C@u ) ↓ R : ∃A, u, w.( ↓ u.A@w ⊥ ⊗ (A w)@w ) ↓ L : ∃A, u, w.( ↓ u.A@w ⊥ ⊗ (A w)@w ) ∀R(F ) : ∃B, u.( ∀x.B@u ⊥ ⊗ ∀x. (B x)@u ) ∀L(F ) : ∃B, u.( ∀x.B@u ⊥ ⊗ ∃x. (B x)@u ) ∀R(W ) : ∃A, u.( ∀v.A@u ⊥ ⊗ ∀v. (A v)@u ) ∀L(W ) : ∃A, u.( ∀v.A@u ⊥ ⊗ ∃v. (A v)@u )
The following theorem shows that the encoding of HyLL into LL is adequate in the sense that a focused step in LLF corresponds exactly to the application of one HyLL inference rule.

Theorem 3.1 (Adequacy). Let Υ be the set of clauses in Figure 3. The sequent Γ; ∆ F @w is provable in HyLL iff Υ; • ⇑ ∆ , ? Γ , F @w is provable in LLF. Moreover, the adequacy of the encodings is on the level of derivations meaning that, when focusing on a specification clause, the bipole derivation corresponds exactly to applying the introduction rule at the object level.

Proof. We will illustrate here the case for rule at L , the other cases are similar. Applying the object level rule

Γ; ∆, A@u C@v Γ; ∆, (A at u)@w C@v [at L]
corresponds to deciding on the LL formula given by the encoding of the rule at L (stored in Υ). Due to focusing, the derivation in LL has necessarily the shape

Υ, Γ ; (A at u)@w ⇓ (A at u)@w ⊥ I 1 Υ, Γ ; ∆ , C@v , A@u ⇑ • Υ, Γ ; ∆ , C@v ⇓ A@u R ⇓, R ⇑ Υ, Γ ; ∆ , (A at u)@w , C@v ⇓ (A at u)@w ⊥ ⊗ A@u ⊗ Υ, Γ ; ∆ , (A at u)@w , C@v ⇓ ∃C, u, w.( (C at u)@w ⊥ ⊗ C@u ) 3 × ∃ Υ, Γ ; ∆ , (A at u)@w , C@v ⇑ • D 2
Note that the LL formula corresponding to (A at u)@w is consumed and, in the end of the focused phase, the encoding of A@u is stored into the linear context. This mimics exactly the application of the Rule at L in HyLL.

One may wonder whether it is possible to define an encoding of formulas from HyLL to LL by adding an extra argument on atomic predicates to represent the current world. We think that such encoding would not be completely compositional and probably not adequate. First, note that the HyLL judgment F @w applies to arbitrary formulas (not only to atomic propositions). Hence, such an encoding must define an operator ∇(F, w) that adds w to all the atomic propositions in F . However, this makes more complicated the definition of the hybrid connectives ↓ and at since, statically, it is not possible to know the correct binding.

HyLL and SELL

Linear logic with subexponentials (SELL)2 shares with LL all its connectives except the exponentials: instead of having a single pair of exponentials ! and ?, SELL may contain as many subexponentials [DJS93, NM09], written ! a and ? a , as one needs. The grammar of formulas in SELL is as follows:

F, G ::= p( t) | p( t) ⊥ | 0 | 1 | | ⊥ | F ⊗ G | F ⊕ G | F . . . .
G | F & G | ∃x.F | ∀x.F | ! a F | ? a F
The proof system for SELL is specified by a subexponential signature I, , U , where I is a set of labels, U ⊆ I is a set specifying which subexponentials allow weakening and contraction, and is a pre-order among the elements of I.

We shall use a, b, . . . to range over elements in I and we will assume that is upwardly closed with respect to U , i.e., if a ∈ U and a b, then b ∈ U .

The system SELL is constructed by adding all the rules for the linear logic connectives except those for the exponentials. The rules for subexponentials are dereliction and promotion of the subexponentials labeled with a ∈ I

? a1 F 1 , . . . ? an F n , G ? a1 F 1 , . . . ? an F n , ! a G ! a ∆, G ∆, ? a G ? a
where the rule ! a has the side condition that a a i for all i. Moreover, for all indices a ∈ U , we add the usual rules of weakening and contraction to ? a . We can enhance the expressiveness of SELL with the subexponential quantifiers and3 [START_REF] Nigam | On subexponentials, focusing and modalities in concurrent systems[END_REF] given by the rules (omitting the subexponential signature)

∆, G[l e /l x ] ∆, l x : a.G ∆, G[l/l x ] ∆, l x : a.G
where l e is fresh. Intuitively, subexponential variables play a similar role as eigenvariables. The generic variable l x : a represents any subexponential, constant or variable in the ideal of a. Hence l x can be substituted by any subexponential l of type b (i.e., l : b) if b a. We call the resulting system SELL .

SELL admits a cut-free, complete focused proof system (Figure 4). The sequent notation is close to the one for LLF and differs only on the treatment of contexts. SELL makes use of indexed contexts K that maps a subexponential index to multiset of formulas, e.g., if s is a subexponential index, then K[s] is a multiset of formulas, where intuitively they are all marked with ? s . That is, K[s] = {F 1 , . . . , F n } should be interpreted as the multiset of formulas ? s F 1 , . . . , ? s F n . We also make use of the operations on contexts depicted in Figure 5. Most of the operations are straightforward. For instance, (K 1 ⊗ K 2 )[s], used to specify the tensor introduction rule (⊗), is defined as follows: when s is a bounded subexponential index, 4 On the other side, for the promotion rule, we use the operation K ≤ l that restricts the indexed context K to the formulas marked with a subexponentials greater than l. Hence,

(K 1 ⊗ K 2 )[s] is obtained by multiset union of K 1 [s] and K 2 [s]; when s is an unbounded subexponential index, then it is K 1 [s].
K ≤ l [s] = K[s] if l s and K ≤ l [s] = ∅ otherwise.
By using different prefixes, SELL is an adequate framework for the specification of richer systems where subexponentials are used to mark different modalities/states. For instance, subexponentials can be used to represent contexts of proof systems [START_REF] Nigam | Specifying proof systems in linear logic with subexponentials[END_REF]; to specify systems with temporal, epistemic and spatial modalities [NOP13, OPN15, NOP17] and soft-constraints or preferences [START_REF] Pimentel | A proof theoretic study of soft concurrent constraint programming[END_REF]; to specify Bigraphs [START_REF] Chaudhuri | An adequate compositional encoding of bigraph structure in linear logic with subexponentials[END_REF]; and to specify and verify biological [START_REF] Olarte | A proof theoretic view of spatial and temporal dependencies in biochemical systems[END_REF] and multimedia interacting systems [START_REF] Arias | Foundations for reliable and flexible interactive multimedia scores[END_REF].

Linear logic allows for the specification of two kinds of context maintenance: both weakening and contraction are available (unbounded context) or neither is available (linear context). That is, when we encode (linear) judgments in HyLL belonging to different worlds, the resulting meta-level atomic formulas will be stored in the same (linear) LL context. The same happens with unbounded HyLL judgments and the unbounded LL context.

Encoding HyLL into SELL allows for a better understanding of worlds in HyLL. More precisely, we use subexponentials to represent worlds, where each world w has its own linear and unbounded contexts, represented as w and c w , respectively. Hence, a HyLL judgment of the shape F @w in the (left) linear context is encoded as the SELL formula ? w F @w . That is, HyLL judgments that hold at world w are stored at the w linear context of SELL . A judgment of the form G@w in the unbounded HyLL context is encoded as the SELL formula ? cw G@w . Thus the encoding of G@w is stored in the unbounded subexponential context c w .

The next definition introduces the encoding of HyLL inference rules into SELL . Observe that, surprisingly, the subexponential structure needed is flat on worlds, hence not reflecting their monoidal structure. This is explained by the fact that worlds in HyLL do not control the context on rules as the promotion rule in SELL does. Let us give some intuition on the above defined subexponential structure. The unbounded subexponential c will be used to store the clauses defining the encoding of the rules (see Theorem 3.2). The unbounded subexponential copy is the least of all the unbounded subexponentials. It is a dummy subexponential, 5 useful to correctly specify ! R : when ! copy is introduced, only formulas stored in the unbounded subexponentials can be present (i.e., the theory in c and the atoms of the form • , stored in c w ). Moreover, all the linear locations w (not related to copy) must be empty. This reflects the fact that the HyLL linear context must be empty when ! is introduced. Note also that w : ∞ represents Negative rules

K : ∆ ⇑ L K : ∆ ⇑ ⊥, L [⊥] K : ∆ ⇑ F, G, L K : ∆ ⇑ F . . . .
F : ∆ ⇑ L K : ∆ ⇑? l F, L [? l ] K : ∆ ⇑ , L [ ] K : ∆ ⇑ F, L K : ∆ ⇑ G, L K : ∆ ⇑ F & G, L [&] K : ∆ ⇑ F [c/x], L K : ∆ ⇑ ∀x.F, L [∀] K : ∆ ⇑ F [l e /l x ], L K : ∆ ⇑ l x : a.F, L [ R ]
Positive rules

K : • ⇓ 1 [1] given K[I \ U] = ∅ K 1 : ∆ ⇓ F K 2 : ∆ ⇓ G K 1 ⊗ K 2 : ∆, ∆ ⇓ F ⊗ G [⊗] given (K 1 = K 2 )| U K : ∆ ⇓ F i K : ∆ ⇓ F 1 ⊕ F 2 [⊕ i ] K : ∆ ⇓ F [t/x] K : ∆ ⇓ ∃x.F [∃] K : ∆ ⇓ G[l/l x ] K : ∆ ⇓ l x : a.G [ L ] K ≤ l : • ⇑ F K : • ⇓! l F [! l ] given K[{x | l x ∧ x / ∈ U}] = ∅
Initial, Reaction and Decision Rules

K : ∆ ⇓ p( t) ⊥ [I] given p( t) ∈ (∆ ∪ K[I]) and (∆ ∪ K[I \ U]) ⊆ {p( t)} K + l P : ∆ ⇓ P K + l P : ∆ ⇑ • [D l ], given l ∈ U K : ∆ ⇓ P K + l P : ∆ ⇑ • [D l ], given l / ∈ U K : ∆ ⇓ P K : ∆, P ⇑ • [D 1 ] K : ∆, P a ⇑ L K : ∆ ⇑ L, P a [R ⇑] K : ∆ ⇑ N K : ∆ ⇓ N [R ⇓]
Figure 4: Focused linear logic system with (quantified) subexponentials. Here, L is a list of formulas, ∆ is a multiset of formulas, P is not an atom, P a is positive or an atom and N is negative.

• (K 1 ⊗ K 2 )[i] = K 1 [i] ∪ K 2 [i] if i / ∈ U K 1 [i] if i ∈ U • K[S] = {K[i] | i ∈ S} • (K + l A)[i] = K[i] ∪ {A} if i = l K[i] otherwise • K ≤ i [l] = K[l] if i l ∅ if i l • (K 1 = K 2 ) | S is true if and only if (K 1 [j] = K 2 [j]
) for all j ∈ S. any subexponential in the ideal of ∞ (note that ∞ is also a dummy subexponential). This means that, in the formula w : ∞.F , the subexponential variable w could be substituted, in principle, by any element of W ∪ {c w | w ∈ W}. That is, the proposed subexponential signature correctly specifies the role of worlds in HyLL, as shown next.

Theorem 3.2 (Adequacy). Let Υ be the set of formulas resulting from the encoding in Definition 3.2. The sequent Γ; ∆ F @w is provable in HyLL iff the sequent c : {Υ}, c wi : Γ , w i : ∆ , w : F @w ; • ⇑ • is provable in SELL . 6 Moreover, the adequacy of the encodings is on the level of derivations.

Proof. Again, we will consider the rule at L , as the other cases are similar. If we decide to focus on the SELL formula corresponding to the encoding of at L (stored in ? c Υ), we obtain

w : (A at u)@w ; • ⇑ (A at u)@w ⊥ D l , I c : {Υ}, c wi : Γ , w : (A at u)@w ; • ⇓ ! w (A at u)@w ⊥ ! w c : {Υ}, c wi : Γ , w i : ∆ , v : C@v , u : A@u ; • ⇑ • c : {Υ}, c wi : Γ , w i : ∆ , v : C@v ; • ⇓ ? u A@u R ⇑, ? u c : {Υ}, c wi : Γ , w i : ∆ , w : (A at u)@w , v : C@v ; • ⇓ ! w (A at u)@w ⊥ ⊗ ? u A@u ⊗ c : {Υ}, c wi : Γ , w i : ∆ , w : (A at u)@w , v : C@v ; • ⇓ ∃C, u, w.(! w (C at u)@w ⊥ ? u ⊗ C@u ) ∃, c : {Υ}, c wi : Γ , w i : ∆ , w : (A at u)@w , v : C@v ; • ⇑ • D l ⊗ R : ∃C, C . w : ∞.(! w (C ⊗ C )@w ⊥ ⊗ ? w C@w ⊗ ? w C @w ) at R : ∃A. u : ∞, w : ∞.(! w (A at u)@w ⊥ ⊗ ? u A@u ) at L : ∃A. u : ∞, w : ∞.(! w (A at u)@w ⊥ ⊗ ? u A@u ) ↓ R : ∃A. u : ∞, w : ∞.(! w ↓ u.A@w ⊥ ⊗ ? w (A w)@w ) ↓ L : ∃A. u : ∞, w : ∞.(! w ↓ u.
A@w ⊥ ⊗ ? w (A w)@w ) ∀R(F ) : ∃A, w : ∞.(! w ∀x.B@w ⊥ ⊗ ∀x.? w (B x)@w ) ∀R(W ) : ∃A, w : ∞.(! w ∀v.A@w ⊥ ⊗ v : ∞.? w (A v)@w ) ! L : ∃C. w : ∞.(! w !C@w ⊥ ⊗ ? cw C@w ) ! R : ∃C. w : ∞.(! w !C@w ⊥ ⊗ ! copy ? cw C@w ) copy : ∃C. w : ∞.(! cw C@w ⊥ ⊗ ? w C@w ) Observe that, in a (focused) derivation proving ! w F , the only contexts that can be present are w and the ∞ due to the promotion rule and the ordering in Σ. Since the encoding does not store any formula into the context ∞, the formula ! w F must necessarily be proved from the formulas stored in w. Thus, unlike the LL derivation in the proof of Theorem 3.1, the context c is weakened in the left-hand side derivation since c w. In the end, (A at u)@w , initially stored in the location w, is substituted by A@u in the location u, in one focused step.

Information Confinement. A brief final comment on the expressiveness of worlds in HyLL. One of the features needed for specifying spatial modalities is information confinement: a space (or world) can be inconsistent and this does not imply the inconsistency of the whole system. It turns out that information confinement can be specified in SELL [START_REF] Nigam | On subexponentials, focusing and modalities in concurrent systems[END_REF] but not in HyLL. More precisely, since the formulas ! w ? w 0 -• 0 and ! w ? w 0 -• ! v ? v 0 are not provable in SELL, it is possible to specify systems where inconsistency is local to a given space and does not propagate to the other locations.

In HyLL, however, it is not possible to confine inconsistency: the HyLL rule Γ; ∆, 0@u F @w 0L

shows that any formula F in any world w is derivable from 0 appearing in any world u. Observe that, even if we exchange the rule 0L for a weaker version Γ; ∆, 0@w F @w 0 L the rule 0L would still be admissible Γ; 0@w (0 at v)@w 0 L Γ; ∆, 0@v F @v 0 L Γ; ∆, (0 at v)@w F @v at L Γ; ∆, 0@w F @v cut

µMALL and µHyMALL

In the encodings of object systems that operate on inductive structures such as finite automata, it will be necessary to enrich our representational logic with some mechanism for reasoning about such structures. We will use the µMALL [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF] extension that enriches MALL with least (µ) and greatest (ν) fixed points. These fixed points are written in the form µB t and νB t where B, called the body, is a function of arity | t | + 1; in effect, µB (or νB) serves the role of a defined predicate of arity | t |. Since these are fixed points, we further allow for a seamless change between µB t and B(µB) tand likewise from νB t to B(νB) t-which is usually called unfolding the fixed point. To obtain the full expressive power of fixed points, it is also essential for the logic to have a notion of intensional equality between terms that obeys the equational theory of the λ-calculus; that is, two terms s and t are considered equal, written s = t, if they are related by αβη-conversion [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF]. The final ingredient in µMALL is the ability to quantify over the complete set of unifiers (CSU) of two terms s and t that contain free eigenvariables; this set, written csu(s, t), is the smallest set of unifiers of s and t such that every other unifier of s and t is an instance of some unifier in this set. For arbitrary λ-terms s and t, this set can be infinite. However, for well behaved fragments such as the first-order or the Lλ fragment [START_REF] Miller | Unification under a mixed prefix[END_REF], the CSU is no larger than a singleton. Since these are all standard concepts, we refer the reader to [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF] for further details.

The proof system for µMALL is built using sequents of the form Σ; ∆, where Σ is a context of typed eigenvariables, and ∆ is a multiset of µMALL formulas. As µMALL is an extension of the standard MALL proof system, we elide their standard rules here. The remaining rules cover equality, its formal negation ( =), and the fixed points µ and ν. The rules for the former are as follows.

Σ; t = t = (Σ; ∆)θ : θ ∈ csu(s, t) Σ; ∆, s = t =
Defined identity rules Σ; µB t @ w µB t @ w [µInit] Σ; νB t @ w νB t @ w [νInit]

Equality rules

Σ; • t = t @ w [= R] (Σ; ∆ C @ w)θ : θ ∈ csu(s, t) Σ; ∆, s = t @ u C @ w [= L]
Least fixed point rules

Σ; ∆ B(µB) t @ w Σ; ∆ µB t @ w [µ R] x; BS x @ u S x @ u Σ; ∆, S t @ u C @ w Σ; ∆, µB t @ u C @ w [µ L]
Greatest fixed point rules

x; S x @ w BS x @ w Σ; ∆ S t @ w

Σ; ∆ νB t @ w [ν R] Σ; ∆, B(νB) t @ u C @ w Σ; ∆, νB t @ u C @ w [ν L]
Figure 7: Rules specific to µHyMALL. The rules for the HyMALL connectives can be directly adapted from those in Figure 2.

The rule for inequality requires a bit of explanation. There is one premise for each θ ∈ csu(s, t). The instance (Σ; ∆)θ of the sequent Σ; ∆ is defined as usual: its eigenvariables are the eigenvariables in the set of terms {uθ : u ∈ Σ}, and for each formula F ∈ ∆ there is the formula F θ in ∆θ.

For the fixed points, there is a version of the identity rule that relates the least and greatest fixed points, an unfold rule for least fixed points, and a coinduction rule for greatest fixed points:

Σ; µB t, ν B t dInit Σ; ∆, B(µB) t Σ; ∆, µB t µ x; (S x ) ⊥ , BS x Σ; ∆, S t Σ; ∆, νB t ν
In the defined identity rule dInit, the notation B stands for λp. λ x. (B p ⊥ x ) ⊥ . In the coinduction rule (ν), the predicate S is an invariant. The first premise of the rule shows that it is indeed an invariant of B, while the second premise replaces the greatest fixed point νB with the invariant. Observe that if we use B(νB) itself for the invariant S, then we obtain:

. . .

x; B(µ B) x, B(B(νB)) x

x; (B(νB) x ) ⊥ , B(B(νB)) x Σ; ∆, B(νB) t

Σ; ∆, νB t ν

The left branch is a proof of identity where eventually the defined identity rule dInit is used to relate µ B x and νB x. This branch will therefore always be derivable. Hence, we see that the unfold rule for ν is derivable in terms of the coinduction rule, and therefore does not need to be given explicitly. The meta-theory of µMALL, including the important cut-elimination theorem, is pretty standard and exhaustively covered in [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF].

Along the same lines as µMALL, we can extend HyMALL(the multiplicative/additive fragment of HyLL in Figure 2) to µHyMALL, by adding equality and least and greatest fixed points. In fact, for fixed point predicates built using µ and ν, we will allow the arguments to contain worlds as well; likewise, we will allow for equality to hold between worlds. However, we retain the restriction from HyMALL that all undefined predicates contain no world arguments. 7Like with µMALL sequents, µHyMALL sequents will have an explicit context of eigenvariables, so they will be of the form Σ; ∆ F @ w, where ∆ is as before. Since we are limiting our attention to µHyMALL, we dispense with the unbounded context Γ, which can be added to yield µHyLL. Most of the rules from Figure 2 can be directly adapted with this additional eigenvariable context. The remaining rules are given in Figure 7.

It may be worthwhile to consider if the µHyMALL rules can be encoded in µMALL by means of an extension of Definition 3.1. Indeed, we can simply extend the rules of Figure 3

Computation Tree Logic (CTL) in Linear Logic

Hybrid linear logic is expressive enough to encode some forms of modal operators, thus allowing for the specification of properties of transition systems. As shown in [START_REF] De | A logical framework for systems biology[END_REF], it is possible to encode CTL temporal operators into HyLL considering existential (E) and bounded universal (A) path quantifiers. We show in this section the limitation of such encodings and how to fully capture E and A CTL quantifiers in both propositional µMALL and first order µHyMALL. In both cases, we follow the standard interpretation of CTL quantifiers as fixed points.

The first encoding relies on the behavior of the LL connectives to control the use of transition rules during a proof of a CTL formula. More precisely, states in the transition system are represented as atoms (in the linear context) that are consumed and produced by the encoding of transitions. The second encoding uses HyLL's words in order to define states and quantifiers on words to specify path quantifiers. Hence, the encoding resembles the semantics of CTL.

Let us start by recalling the syntax of CTL.

Definition 5.1 (CTL connectives and path quantifiers). Given a set of atomic propositions P, formulas in CTL are given by the following grammar

F ::= p | ¬F | F ∧ F | F ∨ F | QXF | QFF | QGF | Q[F UF ] p ∈ P, Q ∈ {A, E},
The temporal connectives are: X (Next) meaning "at the next state"; F (Future) meaning "in some future"; G (Globally) meaning "in all futures"; and, F UG (F until G) meaning "from now, F will be true in every steps until some future point (possibly including now) where G holds". Temporal connectives must be preceded by a path quantifier: E (Exists) meaning "for some path" or A (All) meaning "for all paths". The usual dualities apply (e.g., ¬EXF = AX¬F , ¬AGF = EF¬F ) and negation is involutive i.e., it can be restricted to atoms. Transition Systems. Let P = {p 1 , ..., p n } be a set of atomic propositions. A Kripke structure over P is a tuple K = S, I, R, L where S is a finite set of states, I ⊆ S is the set of initial states, R ⊆ S × S is a transition relation and L : S → 2 P is a labeling. We assume that given two different states s, s , L(s) = L(s ). Note that this is not a loss of generality since we can always extend P with atomic propositions to uniquely identify each state. We shall write s -→ s when (s, s ) ∈ R. Observe that, in CTL, R must be serial, i.e., every state has a successor. Finally, we write s |= K CT L F when F holds at state s with the standard meaning (see, e.g., [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF]). For instance, s |= K CT L EGF iff there exists a path π = s 1 • s 2 • s 3 • . . . starting at s (i.e. s = s 1 ) such that for all i ≥ 1, s i |= K CT L F .

Transition Systems and HyLL

In order to specify reachability properties in transition systems, some modal connectives can be defined in HyLL [START_REF] Despeyroux | A hybrid linear logic for constrained transition systems[END_REF]:

A def = ↓u. ∀w. (A at u.w) ♦A def = ↓u. ∃w. (A at u.w) δ v A def = ↓u. (A at u.v)
A (resp. ♦A) represents all (resp. some) state(s) satisfying A and reachable in some path from now. The connective δ represents a form of delay: δ v A stands for an intermediate state in a transition to A. Informally it can be thought to be "v before A".

We may use such modal operators in order to encode some features of transition systems as HyLL formulas. To each p ∈ P, we associate two HyLL atomic formulas: p and p ⊥ (abusing the notation), where by p ⊥ we denote the atomic HyLL proposition interpreting the CTL formula ¬p. Then states and transitions can be encoded as follows:

[[s]] K = p∈P v(s, p) [[s -→ s ]] K = ∀w. (([[s]] K at w) -• δ 1 ([[s ]] K ) at w) where v(s, p) = p if p ∈ L(s) and v(s, p) = p ⊥ otherwise. Given a transition relation R = {r 1 , ..., r m }, we use [[R]] K @w to denote the set {[[r 1 ]] K @w, • • • , [[r m ]] K @w}.
We can encode in HyLL a restricted fragment of CTL, namely, formulas built using only the temporal connectives EX, EF : Proposition 5.1 (Adequacy). Let K = S, I, R, L be a Kripke structure on a set of atomic propositions P. Let F be a CTL formula built from the CTL fragment ∧, ∨, EX, EF. Then,

[[p]] K = p ⊗ [[¬p]] K = p ⊥ ⊗ [[F ∧ G]] K = d + ([[F ]] K & [[G]] K ) [[F ∨ G]] K = d -([[F ]] K ) ⊕ d -([[G]] K ) [[EXF ]] K = d + (δ 1 [[F ]] K ) [[EFF ]] K = ♦[[F ]] K where d + (F ) = F ⊗
s |= K CT L F iff [[R]] K @0; [[s]] K @w [[F ]] K @w is provable in HyLL.
Proof. We will reason on the focused version of HyLL and we will assume that atoms have positive bias. Assume that s -→ s . If we decide to focus on the encoding of (s, s ) ∈ R, we necessarily obtain a derivation of the shape

[[R]] K @0; [[s ]] K @w.1 G [[R]] K @0; [[s]] K @w G (1)
where all atoms from [[s]] K @w are consumed and the formula [[s ]] K @w.1 is added into the context. This mimics exactly the transition s -→ s . The (⇒) side proceeds by induction on the structure of F . For the base case, if s |= K CT L p, it is easy to show that the sequent

[[R]] K @0; [[s]] K @u (p ⊗ )@u is provable in HyLL (similarly for ¬p). If s |= K CT L EF F , then there exists a path s 1 • s 2 • • • • starting at s s.t. there exists i ≥ 1 s.t. s i |= K
CT L F . By repetitively applying (1), we have a derivation that consumes [[s 1 ]] K to produce [[s i ]] K and the result follows by induction. The case for EXF follows similarly. Finally, the cases for ∧ and ∨ follow immediately by induction.

(⇐) We shall show that each focused step corresponds exactly to a "step" in the deduction of s

|= K CT L F . Consider the sequent [[R]] K @0; [[s]] K @w [[F ]] K @w.
We have two choices: (i) focus on [[s -→ s ]] K and, from (1), we transform the state s into the state s ; or (ii) focus on the formula on the right. In the first case, we already showed that this action mimics exactly the transition s -→ s . In the second case, the focused formula F must be of the form

F ::= p ⊗ | p ⊥ ⊗ | 1 ⊗ (F & F ) | F ⊕ F |↓ u (F at u.1) |↓ u (∃w.F at u.w)
representing the encoding of atoms, conjunction, disjunction, EXF and EFF respectively. In a negative phase, the only connectives we can introduce, if any, are the hybrid ones (↓ and at). This is a bureaucratic step allowing us to fix the formulas at the "current" world as in

Γ; ∆ F [x/w]@y Γ; ∆ ↓ x(F at y)@w at R , ↓ R
Hence, when focusing on F we fall in one of the following cases.

• F = p ⊗ (or p ⊥ ⊗ ): the context must already have p (or p ⊥ ), at the right world, to prove p (or p ⊥ ). This corresponds to proving that the state s satisfies (or not) p.

• F = 1 ⊗ (F 1 & F 2 ): 1 is proved with empty context and focus is lost in F 1 & F 2 .
Hence, after a negative phase, we have a derivation proving F 1 and another proving F 2 . This corresponds exactly to the step of proving a conjunction in CTL.

• F = F 1 ⊕ F 2 : chose one of the branches and focus is lost due to the negative delay in the encodings. This corresponds to proving a disjunction in CTL.

• F = d + (δ 1 F ): focus is lost obtaining, on the right, F fixed at the world w + 1. This mimics the step of proving F in the next time-unit ( EXF ).

• F = ∃w.F at u.w: a world w is chosen and focus is lost (due to at). This corresponds in CTL to proving EFF by showing that there exists a future world (u + w) where F holds.

Observe that our encoding cannot be extended to consider formulas of the shape EGF . In fact, the natural choice would be

[[EGF ]] K = [[F ]] K ,
but this encoding would not be adequate. Consider, for instance, a system with a unique state s and a unique (looping) transition s -→ s. Assuming that p ∈ L(s), clearly s satisfies the formula EGp. Now, consider the HyLL sequent

[[s -→ s]] K @0; [[s]] K @w [[s]] K @w.
Introducing the connectives on the right we obtain

[[s -→ s]] K @0; [[s]] K @w [[s]] K @w.v [[s -→ s]] K @0; [[s]] K @w [[s]] K @w ↓ R , ∀ R , at R
where v is fresh. Then focusing on the encoding of s -→ s :

[[s -→ s]] K @0; [[s]] K @(w + 1) G [[s -→ s]] K @0; [[s]] K @w G copy, ∀ L , -• L
Therefore the left and right worlds in the sequent will never match, and this sequent is not provable. In other words: the resources in the context are enough for proving the property for a (bounded) n but not for all natural numbers. For proving this, one necessarily needs (meta-level) induction, i.e., fixed points.

[ [ The encodings of QX, QF, Q G and QU, for Q ∈ {A, E} are in Figure 8. The encoding of the rest of the formulas is as in the case for HyLL.

Y )) [[A[F U G]]] K = µY.[[G]] K ⊕ [[F ]] K & & (s,
[E[F U G]]] K = µY.[[G]] K ⊕ [[F ]] K & (s,
EFF = µY.F ∨ EXY EGF = νY.F ∧ EXY E[F U G] = µY.G ∨ (F ∧ EXY ) AFF = µY.F ∨ AXY AGF = νY.F ∧ AXY A[F U G] = µY.G ∨ (F ∧ AXY )
The encoding relies on the following principles. Let r = (s, s ) ∈ R. The formula pos(s) (resp. neg(s)) tests if r can (resp. cannot) be fired at the current state. If it can be fired, then the current state is transformed into the new state.

Hence, the encoding of A (resp. E) test all (resp. at least one) of the fireable rules. This explains the use of & (resp. ).

Finally, the use of least or greatest fixed points reflects the fixed point characterization of CTL connectives given above.

Remark 5.1. Observe that, in all the clauses in Figure 8 B). The first is stronger, in the sense that B can choose the branch to move up with (L or R), while the second forces B to stick with R. We chose the second since it describes better the desired behavior, thus easing the proof of the following adequacy result.

Theorem 5.1 (Adequacy). Let K = S, I, R, L be a Kripke structure on a set of atomic propositions P, s ∈ S be a state and F be a CTL formula. Then,

s |= K CT L F iff the sequent •; [[s]] K , [[F ]] K is provable in µMALL.
Proof. As done for HyLL, we will consider the focused version of µMALL and we will assume that atoms have positive bias.

(⇒) We proceed by induction on the structure of the formula. The base cases for atomic formulas (p and ¬p) are trivial and the cases for ∧ and ∨ are easy consequences from the inductive hypothesis.

Cases AX and EX. Note that given two different states s and s (thus L(s) = L(s )):

• the sequents Then, for every premise, a positive phase starts, choosing between neg(s i ) and pos(s i ). In the first case, if the rule is not fireable, the proof ends. In the second case, we have

Σ; [[s i ]] K , [[F ]] K Σ; [[s]] K ,
[F ]] K in the disjunction [[AFF ]] K = µY.[[F ]] K ⊕ Ψ).
The other cases for least fixed point operators follow similarly. Cases for the greatest fixed point operators. Consider now the formula AGF . If this formula holds at s, then s must satisfy F and all reachable states from s must also satisfy AGF . Let S = {s ∈ S | s |= K CT L F and, for all s , if s -→ s , then s ∈ S} be the greatest set of states containing s. Note that the greatest fixed point in the (CTL) definition of AG computes exactly that set. Let S above be the set {s 1 , ..., s n } and

I = [[s 1 ]] ⊥ K ⊕ • • • ⊕ [[s n ]] ⊥ K .
We shall show that, for any s ∈ S, the sequent Σ

; [[s]] K , [[AGF ]] K is provable using I as inductive invariant.
Once the rule ν is applied, we have to prove two premises:

1. Premise Σ; [[s]] K , I.
; [[F ]] K , [[s]] K Σ; R 1 , [[s]] K • • • Σ; R n , [[s]] K Σ; [[F ]] K & R 1 & • • • & R n , [[s]] K & where R i = neg(s i ) ⊕ (pos(s i ) ⊗ ([[s i ]] K . . . .
; [[s ]] K , I Σ; R i , [[s]] K ⊕, ⊗, &
Since S is closed under -→, it must be the case that s ∈ S and hence the sequent Σ; [[s ]] K , I is provable (as in Premise 1 above).

The case EG is similar. (⇐) Due to focusing, we can show that the derivations in the ⇒ part are the only way to proceed during a proof in (focused) µMALL. Hence, we match exactly a "step" in the deduction of s |= K CT L F . Hence, the only interesting case Finally, it is worth noticing that, in Definition 5.2, we do not encode the transition rules as a theory (as we did in Section 5.1). In fact, consider the following: (1) the presence of a formula of the shape [[s -→ s ]] K in the context allows us to move from the current state to a successor one; (2) fixed points operators must be applied in order to go through paths, checking properties on them. Now, actions (1) and (2) should be coordinated, otherwise one would lose adequacy in the encodings. More precisely, by focusing on [[s -→ s ]] K , we may "jump" a state without checking the needed property in that state. For avoiding these problems, we internalized the transition rules directly into the encoding.

[[AXF ]] = ↓u. ∀w. trans u w ⊗ ([[F ]] at w) [[EXF ]] = ↓u. ∃w. trans u w ⊗ ([[F ]] at w) [[AFF ]] = µ(λR. [[F ]] ⊕ ↓u. ∀w. trans u w ⊗ (R at w)) [[EFF ]] = µ(λR. [[F ]] ⊕ ↓u. ∃w. trans u w ⊗ (R at w)) [[AGF ]] = ν(λR. [[F ]] & ↓u. ∀w. trans u w ⊗ (R at w)) [[EGF ]] = ν(λR. [[F ]] & ↓u. ∃w. trans u w ⊗ (R at w)) [[A[F U G]]] = µ(λR. [[G]] ⊕ ([[F ]] & ↓u. ∀w. trans u w ⊗ (R at w))) [[E[F U G]]] = µ(λR. [[G]] ⊕ ([[F ]] & ↓u. ∃w. trans u w ⊗ (R at w)))

CTL in µHyMALL

The encoding on µMALL in the previous section is heavy in two specific ways: (1) the current state of the automaton is managed by means of the neg and pos predicates, and (2) the encoding of formulas is not compositional as it is sensitive to the transition system R. These aspects limit us from even stating and proving properties of the encoding that are independent of the transition system. For instance, it is obvious from the semantics that AGF implies EGF regardless of what F or R are, and this can even be seen as a direct consequence of (A & B) (A ⊕ B) being true in linear logic, but we are prevented from writing that implication generically for any R. These issues can be addressed by means of an encoding using µHyMALL instead of µMALL.

The key difference in the encoding in µHyMALL is that we can encode the transition system directly by means of a non-recursive least fixed point expression, i.e., a table. We write this as the predicate trans that can be derived from a set of transition rules R as follows: trans = µ λT. λu. λv. From the definition of trans, we have that, for any given s, s : trans s s trans s s ⊗ trans s s and trans s s 1. These statements are easy to prove, starting with [-•R] and then using [µL] (with any invariant since trans is not recursive). Note that for any t, t = t is logically equivalent to 1. Moreover, if t and t are different terms, then csu(t, t ) is empty and a formula t = t on the left of the sequent finishes any derivation (using [= L]). Observe that in this encoding, the task of establishing the successor state is delegated to the multiplicative subformula trans u v in each case. The multiplicative split guarantees that it cannot consume any other linear assumptions. However, since trans unfolds into a disjunction of equations, there is no possible way for it to consume any linear resources in the first place. Note also that this predicate is the only one in the encoding that needs to quantify over worlds. This is typical of encodings in µHyMALL (or µHyLL): any inductive reachability relation that needs to be encoded on worlds can be represented as a least fixed point predicate.

As mentioned at the start of this subsection, the encoding in µHyMALL allows us to prove meta-theoretic properties of CTL such as, for any F , •; [[AGF ]] @ s [[AFF ]] @ s. This proof does not require examining the trans definition at all. In fact, all the characteristic properties of CTL given at the start of Section 5.2 can be proved as theorems in µHyMALL.

Concluding Remarks and Future Work

We compared the expressiveness, as logical frameworks, of two extensions of linear logic (LL). We showed that it is possible to adequately encode HyLL's logical rules into LL. In order to better analyze the meaning of worlds in HyLL, we showed that a flat subexponential structure (for worlds) suffices to encode HyLL into SELL . We also showed that information confinement cannot be specified in HyLL. Finally, with better insights about the meaning of HyLL's words, we pushed forward previous attempts of using HyLL to encode Computational Tree Logic (CTL). We showed that only by using meta-level induction (or fixed points inside the logic) it is possible to faithfully encode CTL path quantifiers.

There are some other logical frameworks that are extensions of LL, for example, HLF [START_REF] Reed | Hybridizing a logical framework[END_REF]. Being a logic in the LF family, HLF is based on natural deduction, hence having a complex notion of (βη) normal forms as well as lacking a focused system. Thus adequacy (of encodings of systems in HLF) results are often much harder to prove in HLF than in HyLL or in SELL.

While logical frameworks should be general enough for specifying and verifying properties of a large number of systems, some logical frameworks may be more suitable for dealing with specific applications than others. Hence, it makes little sense to search for "the universal logical framework". However, it is often salutary to establish connections between frameworks, specially when they are meant to reason about the same set of systems.

In this context, both HyLL and SELL have been used for formalizing and analyzing several systems. This work indicates that SELL is a broader framework for handling such systems, since it can encode HyLL's rules and worlds naturally and directly. However, the simplicity of HyLL may be of interest for specific purposes, such as building tools for diagnosis in biomedicine. Moreover, as shown in Section 5.3, HyLL offers an elegant way of specifying transitions systems and their properties (written in CTL).

Formal proofs in HyLL were implemented in [START_REF] De | A logical framework for systems biology[END_REF], in the Coq proof assistant. It would be interesting to extend the implementations of HyLL given there to µHyMALL. Such an interactive proof environment would enable both formal studies of encoded systems in µHyMALL and formal meta-theoretical study of µHyMALL itself.

Figure 2 :

 2 Figure 2: The sequent calculus for HyLL.

Figure 3 :

 3 Figure 3: Specification of HyLL rules into LL (see Definition 3.1).

Definition 3. 2 (

 2 HyLL rules into SELL ). Let w, d, h, • , • , • , A, B, C be as in Definition 3.1 and o be the type for SELL formulas. Given a HyLL constraint domain W, consider a subexponential signature Σ = I, , U such that U = {c, copy, ∞} ∪ {c w | w ∈ W}, I = W ∪ U . For any w ∈ W we have w ∞, copy c w ∞, copy c and, for any other u, w ∈ I, u w. The encoding of HyLL inference rules into SELL is depicted in Figure 6 (we omit the encodings of the other connectives, that follow similarly).

Figure 5 :

 5 Figure 5: Specification of operations on contexts.

Figure 6 :

 6 Figure 6: HyLL rules into SELL . (Definition 3.2)

  with new cases for equalities and fixed points. The extension is almost entirely trivial and elided here except for the following sketch: both [µInit] and [νInit] will be captured by means of dInit; [= R] by means of =; [= L] by means of =; [µ L] and [ν R] by means of ν; and [µ R] and [ν L] by means of µ.

  1 and d -(F ) = 1 -• F are positive and negative delays respectively. Observe that d + (F ) ≡ d -(F ) ≡ F . Delays are added for adequacy results.

Definition 5. 2 (

 2 CTL into propositional µMALL). Let K = S, I, R, L be a Kripke structure on a set of atomic propositions P. We define -[[s]] K = ( p∈P v(s, p)) ⊥ where v(s, p) = p if p ∈ L(s) and v(s, p) = p ⊥ otherwise. pos(s) = [[s]] ⊥ K neg(s) = p∈P (v(s, p) ⊥ ⊗ ).

Figure 9 :

 9 Figure 9: Encoding of CTL into µHyMALL (See Definition 5.3)

  (s,s )∈R (s = u ⊗ s = v) .

  Definition 5.3. (CTL into µHyMALL) Let K = S, I, R, L be a Kripke structure on a set of atomic propositions P. Let trans be the predicated defined as above on R. The encoding [[•]] of CTL temporal formulas, i.e., of QX, QF, QG and QU, for Q ∈ {A, E} into µHyMALL is in Figure9.

  Theorem 5.2 (Adequacy). Let K = S, I, R, L be a Kripke structure on a set of atomic propositions P, s ∈ S be a state and F be a CTL formula. Then, the µHyMALL sequent:•; • [[F ]] @ s is derivable if and only if s |= K CT L F .Proof. The proof follows the same argument in the proof of Theorem 5.1.

  . . . . . . . . . . . . . . . . . . . . . . . . . . . where atomic propositions are applied to a sequence of terms. The logical connectives for LL can be divided into the following groups: the multiplicative version of conjunction, true, disjunction, and false, which are written as ⊗, 1, . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . G | F & G | F ⊕ G | ∃ τ x.F | ∀ τ x.F | ?F | ! F

  . . . . . . . G ⊥ . Hence negation in LL has only atomic scope. First proposed by Andreoli [And92] for linear logic, focused proof systems provide normal form proofs for cut-free proofs. The connectives of linear logic can be divided into two classes: negative ( . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . , ⊥, &, , ∀,

  . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . j=1,...,mi ?p i,j	[	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . , ?, R ⇑]	• • •
		. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
		. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Γ; ∆ ⇑ ∀x 1 . . . ∀x p [& i=1,...,n . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . j=1,...,mi ?p i,j ] [∀, &] Γ; ∆ ⇓ ! ∀x 1 . . . ∀x p [& i=1,...,n . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . j=1,...,mi ?p

  . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . G, L	[	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ] Γ, F ; ∆ ⇑ L

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . .

  . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . G, L	[	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ]	K + l

.

  [AXF ]] K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	[[EXF ]] K	= =	& (s,s )∈R	(neg(s) ⊕ (pos(s) ⊗ ([[s ]] K (pos(s) ⊗ ([[s ]] K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . [[F ]] K ))	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . [[F ]] K ))
	[[AFF ]] K [[EFF ]] K	(s,s )∈R = µY. [[F ]] K ⊕ & (s,s )∈R = µY. [[F ]] K ⊕	(neg(s) ⊕ (pos(s) ⊗ ([[s ]] K (pos(s) ⊗ ([[s ]] K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Y ))	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Y ))
	[[AGF ]] K [[EGF ]] K	(s,s )∈R = νY. [[F ]] K & & (s,s )∈R = νY. [[F ]] K &	(neg(s) ⊕ (pos(s) ⊗ ([[s ]] K (pos(s) ⊗ ([[s ]] K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Y ))
				(s,s )∈R

. . . . .

  In order to prove (in CTL) the formula AFF at state s, we have to check if s satisfies F . If this is not the case, we have to check whether AFF holds for all successors of s. Hence, CTL quantifiers are usually characterized as fixed points (see e.g., [BCM + 92]).

	(pos(s) ⊗ ([[s ]] K	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Y ))
	s )∈R
	Figure 8: Encoding of CTL into propositional µMALL (see Definition 5.2).
	5.2 Encoding E and A quantifiers in propositional µMALL

  , the formula pos(s) ⊗ ([[s ]] K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . K -• B, which reads closer to what we expect: "assuming that r is fired, B holds". The formulas (L -• R) -• B and L ⊗ (R -• B) are not logically equivalent. In fact, the first formula is equivalent to (L ⊗ R ⊥ ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . B while the second is equivalent to L ⊗ (R ⊥ . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . B), is present. We could have
	written instead [[r]] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  [[s]] K , pos(s) and [[s]] K , neg(s ) are both provable. • the sequents [[s]] K , neg(s) and [[s]] K , pos(s ) are both not provable. This means that, in a context containing the formula [[s]] K , we can always prove if a given transition rule r ∈ R is fireable or not. Consider the case AXF . The derivation necessarily starts with the negative phase Σ; [[s]] K , neg(s 1 ) ⊕ (pos(s 1 ) ⊗ ([[s 1 ]] K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . [[F ]] K ) ... Σ; [[s]] K , neg(s m ) ⊕ (pos(s m ) ⊗ ([[s m ]] K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . (s,s )∈R Σ; [[s]] K , &	(neg(s) ⊕ (pos(s) ⊗ ([[s ]] K	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . [[F ]] K ))	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . [[F ]] K )	&

.

.

  pos(s i ) ⊗ ([[s i ]] K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . the positive phase ends. By inductive hypothesis, the sequent Σ; [[s i ]] K , [[F ]] K is provable. The case EXF is similar. Cases for the least fixed point operators. If AFF holds in CTL at state s, then, in all paths starting at s, there is a reachable state s such that F holds at s . Let s = s 1 -→ • • • -→ s n = s be one of such paths and consider the following derivation: Σ; [[s]] K , neg(s 1 ) ⊕ (pos(s 1 ) ⊗ ([[s 1 ]] K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µB) ... Σ; [[s]] K , neg(s m ) ⊕ (pos(s m ) ⊗ ([[s m ]] K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . The premises correspond to proving whether a transition r ∈ R is fireable or not. If r is fireable, we observe a derivation of the shape Σ; [[s i ]] K , µB Σ; [[s]] K , pos(s i ) ⊗ ([[s i ]] K . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . [[F ]] K )	⊗,	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .			. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µB)
	Σ; [[s]] K , µB			µ, ⊕, &
	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µB)	⊗,	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

and . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Σ; [[s]] K , neg(s i ) ⊕ (pos(s i ) ⊗ ([[s i ]] K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µB)) ⊕ where s becomes s i and, from that state, µB must be proved. Hence, we can show that [[s n ]] K will be eventually added to the context. By inductive hypothesis, the sequent Σ; [[s n ]] K , [[F ]] K is provable and hence Σ; [[s n ]] K , µB is provable (by unfolding and then choosing [

  . . . . . . . . . . . . . . . . . . . . . . . . . Again we have several cases to prove. The first sequent Σ; F, [[s]] K follows from inductive hypothesis.If the rule r i is not fireable at state s, then the sequent Σ; [[s]] K , R i is provable (by choosing neg(s i )). On the other hand, if r i is fireable at state s, we then have Σ

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . I).

We note that intuitionistic and classical SELL are equally expressive, as shown in[START_REF] Chaudhuri | Classical and intuitionistic subexponential logics are equally expressive[END_REF]. Hence, although we will introduce here the classical version of SELL, we could also present SELL as an extension of ILL.

can be read as "for all locations" while is meant to be "there exists a location".

As specified by the side-condition of the ⊗ rule in Figure4, it must be the case that that K 1 [s] = K 2 [s] when s is unbounded.

Subexponentials are often called dummy when they are not inhabited.

Clarifying some notation: if ∆ = {F 1 @w 1 , . . . , Fn@wn}, then ? w i ∆ = ? w 1 F 1 @w 1 , . . . , ? wn Fn@wn . Observe that, in the negative phase, such formulas will be stored at their respective contexts, that will be represented by w i : ∆ . Similarly for • .

This restriction can be lifted from HyMALL without any difficulty.

Acknowledgments. We would like to thank Dale Miller for being such a good mentor and colleague. We also thank the anonymous reviewers for their valuable comments on an earlier draft of this paper.


Kevin Louarn

Y Claveau

Chantal Fontaine

Alexandre Arnoult

Ludovic Marigo-Lombart

Inès Massiot

F Piquemal

A Bounouh

N Cavassilas

Guilhem Almuneau
email: almuneau@laas.fr

Thickness limitation of band to band tunneling process in InGaAs/GaAsSb type-II tunnel junctions designed for multijunction solar cells

Keywords: III-V Semiconductors, Gallium Arsenide Based cells, Multijunction Solar Cell, Epitaxy, Tunnel Junction

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

Tunnel Junctions (TJs) are key devices for monolithic multi-junction solar cells (MJSCs), in which they interconnect adjacent sub-cells. Each sub-cell of Multi-Junction Solar Cells (MJSCs) is designed to absorb a specific range of the solar spectrum. Thus, the absorption spectral response of the whole device is extended whilst thermalization losses are reduced, enabling to reach conversion efficiencies as high as 46% [START_REF] Dimroth | Four-Junction Wafer-Bonded Concentrator Solar Cells[END_REF].

A TJ must meet four main criteria in order to perform as an efficient interconnection between adjacent sub-cells: (i) Its peak tunneling current density (J peak ) must be higher than the photocurrent density of the MJSCs; (ii) it should have an intrinsic electrical resistivity as low as possible; (iii) it should be transparent on the spectral range of interest for the photons to be absorbed in the underlying subcells. Moreover, in the case of TJ shaped with mismatched layers, (iv) the latter layers should be elastically strained in order to avoid dislocations that could propagate in upper sub-cells. The photocurrent density is around 15 mA/cm² at 1 sun for most of the existing designs of MJSCs (wafer bonding [START_REF] Dimroth | Four-Junction Wafer-Bonded Concentrator Solar Cells[END_REF], dilute nitride (2), metamorphic (3)) and can reach values as high as [START_REF] Floro | Measuring Ge segregation by real-time stress monitoring during Si 1x Ge x molecular beam epitaxy[END_REF] A/cm² at 1000 suns. To be suited for their use in MJSCs, TJs must therefore exhibit J peak significantly higher than 15 A/cm² in order to have a low electrical resistivity at their working point. In order to evaluate and compare the electrical performances of the TJs, we focus only on the J peak value and not on the intrinsic resistance. Indeed, the J-V characteristic of a low resistive TJ is dominated by the series parasitic resistances of the global device (mostly due to the metal/semiconductor interfaces) and thus decorrelated to the tunneling junction. Such parasitic resistances have a huge impact on the apparent resistance extracted from the experimental J-V characteristic but do not affect the J peak value, as presented in [START_REF] Guter | I-V Characterization of Tunnel Diodes and Multijunction Solar Cells[END_REF].

The usual way to get low resistive TJs with high J peak values is to use highly doped materials. Although it is easy to get high doping levels in p-Type GaAs with C or Be dopants, the task is more complicated for ntype GaAs. It is indeed well known that the Si dopant in GaAs suffers from compensation and saturation issues, which limits the n-doping level to ~7x10 18 cm -3 (5) [START_REF] Neave | Silicon doping of MBE-grown GaAs films[END_REF] and thus the performance of the GaAs TJs. The use of Te for n-doping rather than Si enables to get high doping levels in the range of ~3x10 19 cm -3 which is required for strong tunneling currents. For example, AlGaAs:C/GaInP:Te or AlGaAs:C/GaAs:Te have been recently developed by metal organic vapor phase epitaxy (MOVPE) with peak tunneling current density up to 10 kA/cm² [START_REF] García | Performance analysis of AlGaAs/GaAs tunnel junctions for ultrahigh concentration photovoltaics[END_REF]. Unfortunately, the Te dopant is not commonly used for n-doped MBE-grown devices, and other MBE approaches to exceed the saturation limit of Si dopant in GaAs have to be considered. The use of specific MBE growth conditions, nominally at a low temperature and a low growth rate, have been shown to enable reaching n-doping levels as high as ~2x10 19 cm -3 [START_REF] Köhler | Comparison of Si δ-doping with homogeneous doping in GaAs[END_REF]. J peak values up to 1800 A/cm² for GaAs TJs grown at 400°C have thus been demonstrated [START_REF] Ahmed | Use of nonstoichiometry to form GaAs tunnel junctions[END_REF].

An alternative approach to improve the electrical properties of TJs is to increase the direct band to band tunneling (DBBT) probability thanks to the band-offset engineering capabilities offered by the type-II InGaAs/GaAsSb staggered-band heterojunctions. As pictured in Fig. 1, the tunneling distance in the TJ is significantly reduced in the case of a type-II band offset compared to a usual GaAs tunnel homojunction. This results in a significant increase of the tunneling current density which is directly linked to the tunneling probability and the density of states (DOS) involved in the tunneling process [START_REF] Kane | Theory of Tunneling[END_REF]. High J peak values up to 1500 A/cm² have already been achieved (11) with such InGaAs/GaAsSb metamorphic type II TJs. An even higher J peak of 12 kA/cm² was reached for a pseudomorphic InGaAs/GaAsSb type-II TJ for VCSEL applications [START_REF] Suzuki | Low resistance tunnel junctions with type-II heterostructures[END_REF]. Although such type II TJs are interesting for their electrical properties, the use of lattice-mismatched GaAsSb and InGaAs alloys with a lower bandgap than GaAs impacts the TJs structural and optical properties. Therefore, the thicknesses and the In and Sb concentrations of the TJ layers have to be carefully chosen to keep the positive impact of the type II heterojunction on the tunneling current. The use of low thicknesses and low In and Sb concentrations will fulfill the optical and structural criteria above mentionned.

In this work, we investigate the impact of the thicknesses and the In and Sb concentrations of the InGaAs and GaAsSb layers on the electrical properties of the type II TJs in order to find a TJ design that meets all the requirements for MJSCs. The study is led on a set of 7 MBE-grown In x Ga 1-x As:Si / GaAs 1-y Sb y :C TJ samples with different concentrations of x=y= 0, 0.05 and 0.12 and various thicknesses. To control the structural properties of the two mismatched ternary layers during the MBE growth, we used a home-built optical setup enabling the in-situ real-time monitoring of the wafer curvature; this allows us to check if the growth is kept pseudomorphic or is strain-relaxed. The results of J-V measurements performed on thin (14-20 nm) and thick (100 nm) type-II TJs as well as on GaAs reference TJs with equivalent thicknesses are presented, indicating that the electrical behavior of the thick type-II TJs is much better than their thin type-II and Type-I counterparts. An analysis of the local density of states (LDOS) performed with nonequilibrium Green's Functions (NEGF) is proposed to understand the impact of the thickness on the tunneling mechanisms. Finally, we propose an alternative design for type II TJs that fulfill all the requirements for MJSCs.

Fig. 1: Simulated band edge profiles at thermal equilibrium of type-II p++ GaAs 0.9 Sb 0.1 / n++ In 0.1 Ga 0.9 As (blue curve) and GaAs (black curve) TJs, showing the reduced tunneling distance due to the type-II staggered band configuration with In-and Sbcontaining alloys. Doping levels are kept constant in both structures. Band offsets of the InGaAs/GaAsSb heterojunction are taken from (11).

EXPERIMENTS

MBE growth of the In x Ga 1-x As/GaAs 1-y Sb y TJs

A set of seven MBE-grown TJ samples have been fabricated on n-type (001) GaAs substrates in a Riber 412 growth chamber. Si and C (CBr 4 injector) elements are used as n and p-type dopants, respectively. The TJ typical structure is shown in Fig. 2. Different thicknesses are used for the type-II heterojunction within the different samples. We optimized MBE growth conditions to exceed the Si saturation limits in GaAs with a growth temperature of 460°C and a growth rate of 0.5 µm/h. With such growth conditions, a n-type doping level as high as 1.3x10 19 cm -3 with Si is achieved for the cathode of the TJ whereas the p-type doping level of the TJ anode is set to 10 20 cm -3 . In this study, relatively low In and Sb concentration are used; so we assumed that the electrical activation of the Si and C doping species are similar for GaAsSb and InGaAs as for GaAs. The p-and n-doping levels are thus considered to be equivalent in the GaAs TJs and in the InGaAs/GaAsSb TJs. In order to mimic the environment in which the TJ will be placed within a MJSC, the TJ is surrounded by two GaAs layers with lower doping (2x10 18 cm -3 ) that model the subcells. A highly p-doped GaAs cap layer is grown on top of the structure to ensure a good ohmic contact. The In and Sb concentrations are kept identical for all the devices (x In =y Sb ), to provide the similar conduction and valence band offsets. Two different concentration sets x In/Sb =0.05 and 0.12, have been investigated in addition to the reference GaAs TJ (x In/Sb =0). The samples are labeled as follows: "TJ-X%-thin" or "-thick", with X denoting the In and Sb composition percentages with X=0 for GaAs. The design criterion for the "thin" TJs is defined to be below the critical thickness for strain relaxation determined by the model of Matthews and Blakeslee (13) beyond which the misfit dislocations are generated in the layers. It gives thicknesses below 20 nm for TJ-5%-thin and 14 nm for TJ-12%-thin. The thickness of the "thick" TJs, 100 nm, largely exceeds this critical thickness, and is equally distributed between the cathode and anode. The samples properties are summarized in Table 1 The wafer curvature is monitored in real time, and thereby the strain state of the layers, in order to detect any strain relaxation in the layers, as already published with other methods ( 14) [START_REF] Floro | Measuring Ge segregation by real-time stress monitoring during Si 1x Ge x molecular beam epitaxy[END_REF]. The evolution of the incremental stress (.h f ) linked to the wafer curvature through the Stoney equation, is plotted as a function of the grown film thickness (h f ). When the growth is pseudomorphic, the variation of the incremental stress is linear, and the slope is equal to the stress () experienced by the elastically-strained growing layer.

Fabrication of the test devices

30 µm-diameter circular diodes were then fabricated on the MBE-grown samples using a selfaligned process described in [START_REF] Marigo-Lombart | Single lithography-step self-aligned fabrication process for Vertical-Cavity Surface-Emitting Lasers[END_REF]. An alloyed AuGe/Ni/Au contact is deposited on the n-doped substrate backside followed by a rapid thermal annealing carried out at 450°C for 90s. The diodes are fabricated using self-aligned lift-off process consisting of a photolithography, dry etching and deposition by low temperature chemical vapor deposition (ICP-PECVD) of a SiO x layer to isolate the mesa sidewalls. After getting rid of the SiO x /resist from the top of the mesa, a Ti/Au top-contact is then deposited on the cap layer to make the front contact.

RESULTS

Structural properties of the TJs

The "Thin" type-II TJs are supposed to exhibit excellent structural properties since their thickness is below the theoretical relaxation thickness [START_REF] Matthews | Defects in epitaxial multilayers: I. Misfit dislocations[END_REF]. The structure should then be dislocation-free. As shown in Fig. 3a, by the in-situ wafer curvature measurements on the sample TJ-12%-thin (blue curve), the epitaxial growth of 7 nm of GaAs 0.88 Sb 0.12 and 7 nm of In 0.12 Ga 0.88 As is pseudomorphic. Indeed, the variation of the incremental stress (.h f ) is linear. Note that it has a negative value because both the In-and Sb-containing alloy layers are compressively strained when grown on GaAs. The incremental stress is stabilized at the end of the InGaAs/GaAsSb heterostructure growth and during the growth of the upper GaAs layer. This confirms that the InGaAs/GaAsSb layers growth is pseudomorphic. Otherwise, the GaAs layer would have experienced a tensile strain, and the value of the incremental stress would have been positive.

That is what occurs for the "thick" type-II TJ-12% structure. As shown in Fig. 3b, in-situ wafer curvature measurements indicate that strain relaxation occurs during the growth of the GaAs 0.88 Sb 0.12 layer. Upon relaxation, the incremental stress variation reverses abruptly from a negative to a positive slope, and this trend is pursued during the subsequent GaAs growth. This behavior indicates the generation of dislocations, resulting in a poor structural quality for the TJ structure. The epitaxial growth of this material was then metamorphic.

In the case of the two TJs with 5% In and Sb content with a lower lattice-mismatch to the substrate, the in-situ wafer curvature monitoring (not presented here) shows that the MBE growth remains always pseudomorphic even for the thick structure.

It is worth noting that the pseudomorphic growth is preserved for an InGaAs layer thickness of about 100 nm and 60 nm for the TJ-5% and -12% respectively. These observed critical thicknesses are thus much higher than the ones given by the Matthews' formula. It can be explained by the use of a low growth temperature which differs from the thermodynamic equilibrium conditions considered in Matthews' model. It may also stem from the doping impurities contained in the layers which may affect the mechanical properties of the semiconductor [START_REF] Swaminathan | Effect of n-and p-Type Doping on the Microhardness of GaAs, (Al,Ga)As and Ga(As,Sb) Active Layers in 0.82 and 0.87 µm Injection[END_REF].

Fig. 3:

In-situ wafer curvature measurements during MBE growth of sample TJ-12%-thin (a) and sample TJ-12%-thick (b). This "thick" sample exhibits strain relaxation appearing during the growth of the GaAsSb layer.

J-V characteristics of the devices

The J-V measurements of the samples with 5% In and Sb content are presented in Fig. 4.a and the ones of samples with 12% In and Sb contents are presented in Fig. 4.b. The J-V measurements of the reference GaAs TJs are plotted in black in both figures for comparison. The J-V characteristics of all TJs exhibit the wellknown measurement instabilities in the Negative Differential Resistance (NDR) region. More information on the origin of these instabilities can be found in (4) and [START_REF] Kidner | Bias circuit instabilities and their effect on the d.c. currentvoltage characteristics of double-barrier resonant tunneling diodes[END_REF].

Peak current densities of 370 A/cm² and 380 A/cm² are measured for TJ-GaAs-thin and -thick respectively. Reducing the thickness of the GaAs TJs from 50/50 nm down to 15/15 nm does not affect the electrical performances of the device. Albeit a further reduction of the GaAs TJs thickness may have a detrimental impact on the TJs electrical performances, but this case was not studied here. For the type II TJs, we observed an important impact on the J peak of the type-II TJs when the thicknesses of the GaAsSb and InGaAs layers are reduced. Both "thick" type-II TJs exhibit an enhancement of the electrical performance compared to the GaAs TJ reference, with J peak up to 450 A/cm² and 470 A/cm² respectively for the TJ-5%-thick and TJ-12%-thick samples. In contrast, the Sb and In incorporation in the case of "thin" type-II TJs leads to lower electrical performances than the GaAs TJs, with J peak values of only 100 A/cm² and 200 A/cm² for TJ-5%-thin and TJ-12%-thin respectively. Given the change of the band offset from type-I to type-II which should lead to an enhanced tunneling band-to-band transport, the observed behavior for thin TJ is unexpected. Another information drawn from this study is the effect of the crystalline quality on the TJs performances. Indeed, similar J-V curves with comparable J peak values are observed for thick TJ-5% and -12%. Of course, a higher J peak value was expected for TJ-12%-thick for TJ-5%-thick because of its lower bandgap, but it is worth noting that a high tunneling transport is still observed for the thick and relaxed TJ-12% sample despite its low crystalline quality. It therefore appears that the type-II heterojunction design enables to improve the performance of TJs only in the case of "thick" GaAsSb and InGaAs layers, used within the structure depicted on Fig. 2 and this, independently of their crystal quality.

DISCUSSION

Origin of the impact of the type-II TJ layer thicknesses on the tunneling mechanisms.

To understand the influence of the thickness on the tunneling properties of the type-II TJs, we performed NEGF based simulations of the quantum transport using a six-band k.p Hamiltonian for the electronic states. The details of this model, which properly considers the conduction-valence coupling at the origin of the band-to-band tunneling, can be found in ( 19) and ( 20) ; we have previously demonstrated its ability to predict the J-V characteristics of a simple GaAs TJ [START_REF] Louarn | Multiband corrections for the semi-classical simulation of interband tunneling in GaAs tunnel junctions[END_REF]. The set of material parameters is taken from [START_REF] Vurgaftman | Band parameters for III-V compound semiconductors and their alloys[END_REF], whereas the band-offsets of the InGaAs/GaAsSb heterejonction are taken from (11). The effect of strain is not considered in the calculation. As shown in [START_REF] Aeberhard | Theoretical investigation of direct and phonon-assisted tunneling currents in InAlGaAs/InGaAs bulk and quantum-well interband tunnel junctions for multijunction solar cells[END_REF] or [START_REF] Cavassilas | Quantum electronic transport in polarization-engineered GaN/InGaN/GaN tunnel junctions[END_REF] in the case of InAlGaAs/InGaAs TJs and GaN/InGaN/GaN TJs respectively, an analysis of the LDOS considering a vanishing transverse wave vector can provide relevant information on the different tunneling mechanisms of TJs with various designs. Fig. 5 presents the LDOS of the TJ-12%-thin and TJ-12%thick samples taking into account the GaAs buffer layers. The black curves show the band edge profiles at the thermal equilibrium. To reduce the computational load, the thicknesses of the GaAsSb and InGaAs layers of samples TJ-12%-thick were reduced from 50 nm / 50 nm to 30 nm / 30 nm, which has no incidence in the case of a qualitative comparison of the LDOS. The simulations were performed with a direct applied bias V app value of 80 mV, which means that the TJs operate in their tunneling operating mode.

The comparison of the LDOS maps and the band edges profiles of Fig. 5 shows two main differences between the "thick" and the "thin" type II TJs :

-The first difference is related to the depletion zone extension on each side of the junction. As the doping level on the p-side of the TJ is significantly higher than on the n-side, the depletion area extends mostly on the n-side (up to ~ 18 nm) whereas its extension is only of ~3 nm on the p-side of the TJ. The p-side depletion lengths in both the thick and the thin type II TJs are lower than in the p+-GaAsSb layers. Although the situation is the same for the n-side of the thick type II TJs, one can notice that the 18 nm depletion area extension at the n-side of the "thin" type II TJs is significantly larger than the thickness of the n+-InGaAs layer (7 nm), and thus that the band-bending extends up to the n-GaAs buffer layer. Therefore, in the case of the thin type II TJ, the quasi-Fermi levels between the p+-GaAsSb layer and the n-GaAs buffer layer govern the overlap between the conduction and the valence band, whereas for thick type II TJs the degenerately doped p+-GaAsSb and n+-InGaAs layers play this role. As shown in Fig. 5a, the DOS involved in the DBBT process is thus significantly lower for the thin TJ compared to the thick TJ. Moreover, the tunneling distance is higher for the thin type II TJ (~ 20 nm) than for the thick type II TJs (~ 10 nm), which results for the latter in a reduced tunneling probability.

-The second difference between the two TJs structure is the distance between the InGaAs/GaAsSb interface and their lower doped GaAs buffer layers. The large band offsets at the GaAs/GaAsSb and GaAs/InGaAs interfaces combined with the significant difference in doping levels create an additional band misalignment on both sides of the TJ. Quantized energy levels are therefore most likely to appear depending on the distance between the different potential drops. As indicated in Fig. 5b, there is no visible energy level quantization on the p-side of the thick TJ which exhibits a continuum DOS, and a significant density of quasi-bound states on the n-side of the TJ. On the contrary, one can notice the emergence of bound states at the p-side of the thin TJ, in which the p+ GaAsSb / p-GaAs interface is at the vicinity of the tunneling area because of the very high p+ doping level of the GaAsSb layer. These bound states can have a role in the reduction of the DOS involved in the DBBT process for the thin TJ, even if the main contribution is however expected to come from the shorter tunneling distance. Thus, reducing the p+ doping level of our TJs could be beneficial for DOS involved in the tunneling process. Moreover, it wouldn't affect the tunneling probability as long as the effective doping level N eff of the TJ (

) is not affected. As we are using unnecessary high p+ doping level (1x10 20 cm -3 ) compared to the n+ doping level (1.3x10 19 cm -3 ), there is an interesting flexibility for further optimizing the p+ doping levels in our TJs. Consequently, the combination of these two phenomena for the thin TJs annihilates the beneficial effect of the type II heterojunction on the tunneling probability. Indeed, the DOS, involved in the DBBT process, which is the other main parameter to consider for the tunneling current density is significantly reduced. It also affects the tunneling distance and thus the tunneling probability of the thin type II TJs. On the contrary, the DOS involved in the DBBT process for the thick TJ is almost the same as for an InGaAs/GaAsSb TJ of "infinite" thickness, in which the effect of the buffer layers on the TJs potential could be neglected. Nevertheless, the injection and extraction of carriers in the states available for DBBT require energy relaxation. It can explain that the experimental influence of the type II band alignment in samples TJ-5%-thick and TJ-12%-thick is not as important as we could have expected from other results in the literature (11) [START_REF] Suzuki | Low resistance tunnel junctions with type-II heterostructures[END_REF], as it results in almost the same J peak than the GaAs reference TJ (TJ-0%-thick). Fig. 5. NEGF simulations of the band edge profiles (black curve) and local density of states (LDOS) mapping for the sample TJ-12%-thin (a) and the sample TJ-12%-thick (b) with the GaAs buffer layers. The simulations are performed with 80 mV applied bias and for a null transverse momentum (k┴ =0) assuming the electron-phonon scattering.

Alternative design of type II TJs suitable for MJSCs.

The study of the LDOS shows that the low doped GaAs layers surrounding the thin type II InGaAs/GaAsSb are playing a substantial role in the decrease of the J peak . As these buffer layers mimic the subcells of the MJSC, the same behaviour will probably occur in a real MJSC. The "thin" type-II TJ design is therefore unsuitable for the PV application in spite of its interesting optical and structural properties. In another way, pulling away the GaAs layers from the TJ interface by increasing the GaAsSb and the InGaAs thickness is detrimental for the optical and structural properties, whereas our experimental study shows that it is beneficial for the electrical properties. Such thin or thick type II TJs designs are thus both not suitable in this form for MJSCs applications.

In previously published work [START_REF] Louarn | Effect of low and staggered gap quantum wells inserted in GaAs tunnel junctions[END_REF], we have proposed an alternative type II TJ design that consists of incorporating the degenerately doped n+-In 0.12 Ga 0.88 As / p+-GaAs 0.88 Sb 0.12 heterojunction as quantum wells (QWs) into the depletion area of a usual GaAs TJ. Details of the structure can be found in Ref. [START_REF] Louarn | Effect of low and staggered gap quantum wells inserted in GaAs tunnel junctions[END_REF]. The structure is almost similar to the TJ-12%-thin structure, but the n+-In 0.12 Ga 0.88 As and p+-GaAs 0.88 Sb 0.12 layer thicknesses are only 6 nm and 4 nm respectively, and the heterojunction is surrounded by degenerately doped GaAs layers instead of low doped GaAs. We thus ensure that the overlap between the conduction band and the valence band is settled by the degenerate doping levels of the GaAs TJ and not by the ones of eventual low doped layers located in the vicinity of the TJ. As the InGaAs/GaAs and the GaAsSb/GaAs interfaces are located into the depletion area, there is no quantum confinement in both the hole and the electron emitter regions. The DOS involved in the tunneling process for such a QW-TJ is thus the same as for a GaAs TJ, but the DBBT probability linked to these states is increased by the type II-offset heterojunction. As presented in Fig. 6, this TJ design provides excellent electrical characteristics. Indeed, the simple incorporation of the 6 nm n+-In 0.12 Ga 0.88 As (1.3x10 19 cm -3 ) / 4 nm thick p+-GaAs 0.88 Sb 0.12 (1x10 20 cm -3 ) heterojunction into the GaAs TJ sample (TJ-0%thick) enables to get a J peak value as high as 1200 A/cm², which is three times higher than with a usual GaAs TJ. Fig. 6. J-V characteristics of a usual GaAs TJ (sample TJ-0%-thick, black curve) and the same structure but with the insertion of a 6 nm n + -In 0.12 Ga 0.88 As (1.3x10 19 cm -3 ) / 4 nm p + -GaAs 0.88 Sb 0.12 (1x10 20 cm -3 ) quantum well (red curve).

Therefore, such a QW-TJ enables to get very high tunneling current density above 1 kA/cm 2 with a type II heterojunction. Also, the use of "thin" GaAsSb and InGaAs layers limits the impact of the low bandgap and strained materials. In contrast with a conventional type II TJ, this alternative QW-TJ design enables a good compromise between the electrical, the structural and the optical properties of TJs and so is much more attractive for MJSCs applications.

CONCLUSION

Based on the MBE growth and the J-V measurements of a set of TJ samples, we show experimental evidence of the impact of the layer thicknesses on the electrical performance of InGaAs/GaAsSb type-II TJs with low In and Sb content (< 12%). For "thin" type-II TJs with suitable structural and optical quality for MJSC, the In and Sb incorporations do not show any type-II enhancement effect on the tunneling current density and even considerably reduce it compared to a GaAs TJ. In the case of "thick" type-II TJs, the tunneling current density is increased as compared to GaAs TJ even for TJs which suffer from lower structural quality due to strain relaxation. Based on NEGF simulations of the LDOS mapping and of the band edge profiles for different thicknesses of the type II TJs, we observe also that the low doped GaAs layers located at the vicinity of the tunneling area play a partial role in the reduction of the DOS involved in the DBBT process and thereby in the reduction of the tunneling current density. As the doping of these GaAs layers are at a similar level than in the MJSCs subcells, "thin" type II TJs are unsuitable for such PV applications. However, we propose an alternative design that consists in including a "thin" type II heterojunction into a conventional GaAs TJ. This allows us to decrease the spurious effect of the limited DOS encountered in thin type II heterojunctions and to pull away the low-doped GaAs layers from the tunneling area. This structure exhibits a remarkably high J peak value of 1200 A/cm 2 . The use of thin InGaAs/GaAsSb layers also has the advantage of a limited impact on the structural and optical properties, and thus would be suitable for integration in MJSCs.

More generally, the present study shows the importance of taking into account the global environment of the TJ when designing a device rather than optimizing one-off parameter such as the thickness.

Fig. 2 :

 2 Fig. 2: Schematic structure of the MBE-grown TJ devices. In and Sb contents of the anode and cathode as well as their thicknesses are varied across different samples.

Fig. 4 .

 4 Fig. 4. a: J-V measurements of the two GaAs TJs (black curves), sample TJ-5%-thin (blue curve) and sample TJ-5%-thick (red curve). b: J-V measurements of the two GaAs TJs (black curves), sample TJ-12%thin (blue curve) and sample TJ-12%-thick (red curve). Results from (12) on similar type II TJ are shown for comparison (green curve).

Table 1 :

 1 . List of the samples presented in this work.

	Name	N/P doping level (cm -3 )	In/Sb content	Anode /Cathode thickness
	TJ-0%-thin	1.3x10 19 /1x10 20	0/0 %	15/15 nm
	TJ-0%-thick	1.3x10 19 /1x10 20	0/0 %	50/50 nm
	TJ-5%-thin	1.3x10 19 /1x10 20	5/5 %	10/10 nm
	TJ-5%-thick	1.3x10 19 /1x10 20	5/5 %	50/50 nm
	TJ-12%-thin	1.3x10 19 /1x10 20	12/12 %	7/7 nm
	TJ-12%-thick	1.3x10 19 /1x10 20	12/12 %	50/50 nm

ACKNOWLEDGEMENTS

This work was supported financially by the EURAMET agency in the frame of EMRP ENG51 SolCell project, and by the ANRT-CIFRE. The EMRP is jointly funded by the EMRP participating countries within EURAMET and the European Union. This work was partly supported by LAAS-CNRS micro and nanotechnology platform, a member of the French RENATECH network.