Daniel Hirschkoff

Jean-Marie Madiot

Davide Sangiorgi

Duality and i/o-types in the π-calculus

We study duality between input and output in the π-calculus.

In dualisable versions of π, including πI and fusions, duality breaks with the addition of ordinary input/output types. We introduce π, intuitively the minimal symmetrical conservative extension of π with input/output types. We prove some duality properties for π and we study embeddings between π and π in both directions. As an example of application of the dualities, we exploit the dualities of π and its theory to relate two encodings of call-by-name λ-calculus, by Milner and by van Bakel and Vigliotti, syntactically quite different from each other.

Introduction

It is common in mathematics to look for dualities; dualities may reveal underlying structure and lead to simpler theories. In turn, dualities can be used to relate different mathematical entities. In this work, our goal is to study dualities in the typed π-calculus, and to exploit them to understand the possible relationships between encodings of functions as π-calculus processes.

Reasoning about processes usually involves proving behavioural equivalences. In the case of the π-calculus, there is a well-established theory of equivalences and proof techniques. In some cases, it is necessary to work in a typed setting. Types allow one to express constraints about the observations available to the context when comparing two processes. One of the simplest and widely used such discipline is given by input/output-types [START_REF] Sangiorgi | The Pi-Calculus: a theory of mobile processes[END_REF] -i/o-types in the sequel.

In the π-calculus (simply called π below), the natural form of duality comes from the symmetry between input and output. There are several variants of π where processes can be 'symmetrised' by replacing inputs with outputs and vice versa. The π-calculus with internal mobility, πI [START_REF] Sangiorgi | π-calculus, internal mobility, and agent-passing calculi[END_REF], is a subcalculus of π where only bound outputs are allowed (a bound output, that we shall note a(x).P , is the emission of a private name x on some channel a). In πI, duality can be expressed at an operational level, by exchanging (bound) inputs and bound outputs: the dual of a(x).x(y).0 is a(x).x(y).0.

Other well-known variants of π with dualities are the calculi in the fusion family [START_REF] Parrow | The fusion calculus: expressiveness and symmetry in mobile processes[END_REF][START_REF] Fu | The χ-calculus[END_REF][START_REF] Gardner | Explicit fusions[END_REF]. In fusions, a construct for free input acts as the dual of the free output construct of π, and the calculus has only one binder, restriction. Interaction on a given channel has the effect of fusing (that is, identifying) names.

The discipline of simple types can be adapted both to πI and to fusions, while preserving dualities. The situation is less clear for i/o-types, which can be very useful to establish equivalences between processes. Let us give some intuitions about why it is so. In i/o-types, types are assigned to channels and express capabilities: a name of type oT can be used only to emit values of type T , and similarly for the input capability (iT ). This is expressed by the following typing rules for i/o-types in π: Γ ⊢ a : iT Γ, x : T ⊢ P Γ ⊢ a(x).P Γ ⊢ a : oT Γ ⊢ b : T Γ ⊢ P Γ ⊢ ab.P

The rule for input can be read as follows: process a(x).P is well-typed provided (i) the typing environment, Γ , ensures that the input capability on a can be derived, and (ii) the continuation of the input can be typed in an environment where x is used according to T . The typing rule for output checks that (i) the output capability on a is derivable, (ii) the emitted value, b, has the right type, and (iii) the continuation P can be typed. As an example, a : i(iT ) ⊢ a(x).xt.0 cannot be derived, because only the input capability is received on a, which prevents xt.0 from being typable.

I/o-types come with a notion of subtyping, that makes it possible to relate type ♯T (which stands for both input and output capabilities) with input and output capabilities (in particular, we have ♯T ≤ iT and ♯T ≤ oT ). We stress an asymmetry between the constraints attached to the transmitted name in the two rules above. Indeed, while in a reception we somehow enforce a "contract" on the usage of the received name, in the rule for output this is not the case: we can use subtyping in order to derive type, say, iU for b when typechecking the output, while b's type can be ♯U when typechecking the continuation P .

The starting point of this work is the conflict between the asymmetry inherent to i/o-types and the symmetries we want to obtain via duality. For example i/o-types can be adapted to πI, but duality cannot be applied to the resulting typings. In fusion calculi, the conflict with the asymmetry of i/o-types is even more dramatic. Indeed, subtyping in i/o-types is closely related to substitution, since replacing a name with another makes sense only if the latter has a more general type. Fusions are intuitively substitutions operating in both directions, which leaves no room for subtyping. In work in preparation [START_REF] Hirschkoff | On subtyping in symmetric versions of the π-calculus[END_REF], we investigate this relationship between subtyping and substitution, and compare several variants of existing calculi, including the one presented in this paper.

In this paper, in order to work in a setting that provides a form of duality and where i/o-types can be used, we introduce a calculus named π (Section 2). π is an extension of π with constructs for free input and bound output (note that bound output is not seen as a derived construct in π). In π, we rely on substitutions as the main mechanism at work along interactions. To achieve this, we forbid interactions involving a free input and a free output: the type system rules out processes that use both kinds of prefixes on the same channel.

Calculus π contains π, and any π process that can be typed using i/o-types can be typed in exactly the same way in π. Moreover π contains a 'dualised' version of π: one can choose to use some channels in free input and bound output.

For such channels, the typing rules intuitively enforce a 'contract' on the usage of the transmitted name on the side of the emitter (dually to the typing rules presented above). We show how π can be related to π, by translating π into a variant of the π-calculus with i/o-types in a fully abstract way. This result shows that π and π are rather close in terms of expressiveness.

We also define a notion of typed barbed congruence in π, which allows us to validate at a behavioural level the properties we have mentioned above: two processes are equivalent if and only if their duals are. To our knowledge, no existing calculus with i/o-types enjoys this form of duality for behaviours.

As an application of π, its dualities, and its behavioural theory, we use π to relate two encodings of call-by-name λ-calculus. The first one is the ordinary encoding by Milner [START_REF] Milner | Functions as processes[END_REF], the second one is by van Bakel and Vigliotti [START_REF] Van Bakel | A logical interpretation of the λ-calculus into the π-calculus, preserving spine reduction and types[END_REF]. The two encodings are syntactically quite different. Milner's is input-based, in that an abstraction interacts with its environment via an input. In contrast, van Bakel and Vigliotti's is output-based. Moreover, only the latter makes use of link processes, that is, forwarders that under certain conditions act as substitutions.

Van Bakel and Vigliotti actually encode strong call-by-name -reductions may also take place inside a λ-abstraction. We therefore compare van Bakel and Vigliotti's encoding with the strong variant of Milner's encoding, obtained by replacing an input with a delayed input, following [START_REF] Merro | Locality in the pi-calculus and applications to distributed objects[END_REF] (in a delayed input a(x):P , the continuation P may perform transitions not involving the binder x even when the head input at a has not been consumed).

We exploit π (in fact the extension of π with delayed input) to prove that the two encodings are the dual of one another. This is achieved by first embedding the π-terms of the λ-encodings into π, and then applying behavioural laws of π. The correctness of these transformations is justified using i/o-types (essentially to express the conditions under which a link can be erased in favour of a substitution). Some of the transformations needed for the λ-encodings, however, are proved in this paper only for barbed bisimilarity; see the concluding section for a discussion.

Paper outline. Section 2 introduces π, and presents its main properties. To analyse dualities in encodings of λ into π, in Section 3, we extend π, notably with delayed prefixes. As the addition of these constructs is standard, they are omitted from the original syntax so to simplify the presentation. Section 4 gives concluding remarks.

π, a symmetric π-calculus

In this section, we present π, a π-calculus with i/o-types that enjoys duality properties. We define the syntax and operational semantics for π processes in Section 2.1, introduce types and barbed congruence in Section 2.2, establish duality in Section 2.3, and present results relating π and π in Section 2.4.

Syntax and Operational Semantics

We consider an infinite set of names, ranged over using a, b, . . . , x, y, . . . . The syntax of π is as follows:

P ::= 0 | P |P | !P | α.P | (νa)P α ::= ρb | ρ(x) ρ ::= a | a
π differs from the usual π-calculus by the presence of the free input ab and bound output a(x) prefixes. Note that in π, the latter is not a notation for (νx)ax.P , but a primitive construct. These prefixes are the symmetric counterpart of ab and a(x) respectively. Given a process P , fn(P ) stands for the set of free names of P -restriction, bound input and bound output are binding constructs. Given ρ of the form a or a, n(ρ) is defined by n(a) = n(a) = a.

Structural congruence is standard, and defined as in π (in particular, there are no axioms involving prefixes). The reduction laws allow communication involving two prefixes only if at least one of them is bound :

ab.P | a(x).Q → P | Q[b/x] P → Q if P ≡→≡ Q ab.P | a(x).Q → P | Q[b/x] (νa)P → (νa)Q if P → Q a(x).P | a(x).Q → (νx)(P | Q) P | R → Q | R if P → Q
Note that ab | ac is a process of π that has no reduction; this process is ruled out by the type system presented below.

Types and Behavioural Equivalence

Types are a refinement of standard i/o-types: in addition to capabilities (ranged over using c), we annotate types with sorts (s), that specify whether a name can be used in free input (sort e) or in free output (r) -note that a name cannot be used to build both kinds of free prefixes.

T ::= c s T | 1 c ::= i | o | ♯ s ::= e | r
If name a has type c r T , we shall refer to a as an r-name, and similarly for e. The subtyping relation is the smallest reflexive and transitive relation ≤ satisfying the rules of Figure 1. As in the π-calculus i r is covariant and o r is contravariant. Dually, i e is contravariant and o e is covariant. Note that sorts (e, r) are not affected by subtyping.

The type system is defined as a refinement of input/output types, and is given by the rules of Figure 2. There is a dedicated typing rule for every kind of prefix (free, ρb, or bound, ρ(x)), according to the sort of the involved name. We write Γ (a) for the type associated to a in Γ . T ↔ stands for T where we switch the top-level capability: (c s T ) ↔ = c s T where o = i, i = o, ♯ = ♯. The typing rules for r-names impose a constraint on the receiving side: all inputs on an r-channel should be bound. Note that a(x).P and (νx)ax.P are not equivalent from the point of view of typing: typing a bound output on an r-channel (a) imposes that the transmitted name (x) is used according to the "dual constraint" w.r.t.

♯ s T ≤ i s T ♯ s T ≤ o s T T1 ≤ T2 i r T1 ≤ i r T2 T1 ≤ T2 o r T2 ≤ o r T1 T1 ≤ T2 i e T2 ≤ i e T1 T1 ≤ T2 o e T1 ≤ o e T2 Fig. 1. Subtyping Γ (a) ≤ T Γ ⊢ a : T Fig. 2. π:
Typing rules what a's type specifies: this is enforced using T ↔ (while names received on a are used according to T ). Symmetrical considerations can be made for e-names, that impose constraints on the emitting side.

We write Γ ⊢ P, Q when both Γ ⊢ P and Γ ⊢ Q can be derived.

Remark 1 ("Double contract"). We could adopt a more liberal typing for bound outputs on r names, and use the rule

Γ ⊢ a : o r T Γ, x : T ′ ⊢ P T ′ ≤ T Γ ⊢ a(x).P
(and its counterpart for inputs on e-names). This would have the effect of typing a(x).P like (νx)ax.P . We instead chose to enforce what we call a "double contract": the same way a receiving process uses the bound name according to the type specified in the channel that is used for reception, the continuation of a bound output uses the emitted name according to T ↔ , the symmetrised version of T . This corresponds to a useful programming idiom in π, where it is common to create a name, transmit one capability on this name and use locally the other, dual capability. This idiom is used e.g. in [START_REF] Vasconcelos | Fundamentals of session types[END_REF] and in [SW01, Sect. 5.7.3]. This choice moreover makes the proofs in Section 3.2 easier.

Observe that when a typable process reduces according to

a(x).P | a(x).Q → (νx)(P | Q) ,
if a has type, say, ♯ r (o s T ), then in the right hand side process, name x is given type ♯ s T , and the ♯ capability is "split" into i s T (used by P ) and o s T (used by Q) -it would be the other way around if a's sort were e.

Lemma 1 (Properties of typing). Proposition 1 (Subject reduction). If Γ ⊢ P and P → Q then Γ ⊢ Q.

Proof. By transition induction. Lemma 1 (4) is used when a bound prefix communicates with a free prefix; Lemma 1 (3) is used for the interaction between two bound prefixes, since T and T ↔ have a common subtype. ⊓ ⊔ Definition 1 (Contexts). Contexts are processes with one occurrence of the hole, written [-]. They are defined by the following grammar:

C ::= [-] | C|P | P |C | !C | α.C | (νa)C .
Definition 2. Let Γ, ∆ be typing environments. We say that Γ extends ∆ if the support of ∆ is included in the support of Γ , and if

∆ ⊢ x : T entails Γ ⊢ x : T for all x. A context C is a (Γ/∆)-context, written Γ/∆ ⊢ C, if C can
be typed in the environment Γ , the hole being well-typed in any context that extends ∆.

As a consequence of the previous definition and of Lemma 1, it is easy to show that if ∆ ⊢ P and Γ/∆ ⊢ C, then Γ ⊢ C[P ].

We now move to the definition of behavioural equivalence.

Definition 3 (Barbs). Given ρ ∈ {a, a}, where a is a name, we say that P exhibits barb ρ, written P ↓ ρ , if P ≡ (νc 1 . . . c n )(α.Q | R) where α ∈ {ρ(x), ρb} with a ∈ {c 1 , . . . , c n }. We extend the definition to weak barbs: P ⇓ ρ stands for P ⇒↓ ρ where ⇒ is the reflexive transitive closure of →.

Definition 4 (Typed barbed congruence). Barbed bisimilarity is the largest symmetric relation ≈ such that whenever P ≈ Q, P ↓ ρ implies Q ⇓ ρ and P → P ′ implies Q ⇒ ≈ P ′ . When ∆ ⊢ P, Q, we say that P and Q are barbed congruent at ∆, written

∆ ⊲ P ∼ = c Q, if for all (Γ /∆)-context C, C[P ] ≈ C[Q].

Duality

Definition 5 (Dual of a process). The dual of a process P , written P , is the process obtained by transforming prefixes as follows: ab = ab, ab = ab, a(x) = a(x), a(x) = a(x), and applying dualisation homeomorphically to the other constructs.

Lemma 2 (Duality for reduction).

If P → Q then P → Q.
Dualising a type means swapping i/o capabilities and e/r sorts.

Definition 6 (Dual of a type). The dual of T , written T , is defined by setting c s T = c s T , with r = e, e = r, i = o, and o = i. We extend the definition to typing environments, and write Γ for the dual of Γ .

Lemma 3 (Duality for typing).

1. If T 1 ≤ T 2 then T 1 ≤ T 2 . 2. If Γ ⊢ P then Γ ⊢ P . 3. If Γ/∆ ⊢ C then Γ /∆ ⊢ C.
Proof.

(1): the covariant type operators (i r and o e ) are dual of each other, and so are the contravariant operators (o r and i e ).

(2) follows from the shape of the typing rules, e.g., the dual of the rule for i r is an instance of the rule for i r = o e .

(3) holds because if Φ extends ∆ then Φ extends ∆ (item (1)).

⊓ ⊔

Most importantly, duality holds for typed barbed congruence. The result is easy in the untyped case, since duality preserves reduction and dualises barbs. On the other hand, we are not aware of the existence of another system having this property in presence of i/o-types.

Theorem 1 (Duality for ∼ = c ). If ∆ ⊲ P ∼ = c Q then ∆ ⊲ P ∼ = c Q.
Proof. By Lemma 3, we only have to prove that if P ≈ Q then P ≈ Q, i.e., duality preserves reduction and swaps barbs.

⊓ ⊔

Embeddings between π and π

From π to π io . As explained in Section 1, the π-calculus with i/o-types (that we note π io ) is an asymmetric calculus. In some sense, π can be seen as a 'dualisation' of π io . This can be formulated rigorously by projecting π into π io . To define this projection, which we call a partial dualisation, we work in an extended version of π io , where capabilities are duplicated: in addition to the i, o, ♯ capabilities, we also have capabilities i, o and ♯, that intuitively correspond to the image of the "e-part" of π through the encoding. The additional capabilities act exactly like the corresponding usual capabilities, in particular w.r.t. subtyping and duality. We write π io 2 for the resulting calculus. We discuss below (Remark 3) to what extent the addition of these capabilities is necessary. We also rely on π io 2 to prove that π is a conservative extension of the π-calculus in Theorem 2 -π io 2 is actually close, operationally, to both calculi.

Definition 7 (Partial dualisation). We define a translation from typed processes in π to π io 2 . The translation acts on typing derivations: given a derivation δ of Γ ⊢ P (written δ :: Γ δ ⊢ P ), we define a π io 2 process noted [P ] δ as follows:

[ρb.P ] δ = ρb.[P ] δ ′ if Γ δ (n(ρ)) = c e T [ρb.P ] δ = ρb.[P ] δ ′ if Γ δ (n(ρ)) = c r T [ρ(x).P ] δ = ρ(x).[P ] δ ′ if Γ δ (n(ρ)) = c e T [ρ(x).P ] δ = ρ(x).[P ] δ ′ if Γ δ (n(ρ)) = c r T [(νa)P ] δ = [P ] δ ′ [0] δ = 0 [!P ] δ = ![P ] δ ′ [P | Q] δ = [P ] δ ′ 1 | [Q] δ ′
In the above definition, δ ′ is the subderivation of δ, in case there is only one, and δ ′ 1 and δ ′ 2 are the obvious subderivations in the case of parallel composition. We extend the definition to types: T * stands for T where all occurrences of c r (resp. c e ) are replaced with c (resp. c, the dual of c). We define accordingly Γ * . Remark 2. The same translation could be defined for a simply typed version of π. Indeed, [•] does not depend on capabilities (i/o/♯), but only on sorts (r/e).

Lemma 4. If δ ::

Γ ⊢ P (in π), then Γ * ⊢ [P ] δ (in π io 2 ).
Proof.

In
⊢ P ′ . 4. P ≈ Q iff [P ] δP ≈ [Q] δQ .
Proof. (4) is a consequence of (1), (2), (3). For (1) remark that if Γ (a) = c r T then P and [P ] δP have the same barbs on a; if Γ (a) = c e T , they have dual barbs on a, but in this case so do Q and [Q] δQ . For (2) and (3), we remark that [•] δ is compositional and preserves the fact that two prefixes can interact -even when moving to a different δ.

⊓ ⊔

Proposition 2 (Full abstraction). If δ P :: Γ ⊢ P and δ Q :: Γ ⊢ Q then ⊓ ⊔ Remark 3 (π io 2 vs π io ). We can make two remarks about the above result. First, it would seem natural to project directly onto π io , by mapping capabilities i r and o e into i, and o r and i e into o. However, the result of Proposition 2 would not hold in this case. The intuitive reason is that in doing so, we would allow two names having different sorts in π to be equated in the image of the encoding, thus giving rise to additional observations (since we cannot equate names having different sorts in π). Technically, this question is reminiscent of the problem of closure of bisimilarity under substitutions in the π-calculus.

Γ ⊲ P ∼ = c Q (in π) iff Γ * ⊲ [P ] δP ∼ = c [Q] δQ (in π io 2 ) .
Second, the key ingredient in the definition of partial dualisation is to preserve the distinction between names having originally different sorts in the π process. It is possible to define an encoding of π io 2 into a dyadic version of π io (without the extra capabilities), in order to do so.

Lemma 7. Suppose ∆ ⊢ P, Q holds in π io .

Then

∆ ⊲ P ∼ = c Q (in π io ) iff ∆ ⊲ P ∼ = c Q (in π io 2 ).
Proof. The right-to-left implication is immediate because any π io -context is a π io 2 -context. To show the converse, we observe that a (Γ/∆)-context in π io 2 is a (Γ ′ /∆)-context in π io , where Γ ′ is Γ where every c capability is replaced with c.

From π io to π. π contains π io , the π-calculus with i/o-types: the rules for rchannels are exactly those of π io , and typability of e-free processes coincides with typability in π io . More precisely we can say that π is a conservative extension of π io . In π io we rely on typed barbed congruence as defined in [START_REF] Sangiorgi | The Pi-Calculus: a theory of mobile processes[END_REF], which is essentially the same as ∼ = c in π. Before presenting the result, the following remark introduces some notation.

Remark 4. Suppose δ :: Γ ⊢ P , in π io . Then δ r :: Γ r ⊢ P in π, where Γ r stands for Γ in which all types are decorated with r and δ r stands for δ where all usages of the typing rule for restriction introduce an r-type. Moreover [P ] δ r = P .

Theorem 2 (Conservative extension). Suppose Γ ⊢ P, Q holds in π io .

Then

Γ ⊲ P ∼ = c Q (in π io ) iff Γ r ⊲ P ∼ = c Q (in π).
Proof. We use π io 2 as an intermediate calculus. By Remark 4, let δ P , δ Q be derivations of Γ r ⊢ P and Γ r ⊢ Q such that P = [P ] δP and Q = [Q] δQ . By Proposition 2, the right hand side is equivalent to (

Γ r ) * ⊲ [P ] δP ∼ = c [Q] δQ (in π io
2 ). By hypothesis, and since (Γ r ) * = Γ , the latter is equivalent to Γ ⊲ P ∼ = c Q (in π io 2 ). Lemma 7 allows us to finish the proof.

⊓ ⊔

The result above shows that π can be embedded rather naturally into π. This is in contrast with fusion calculi, where the equivalence on π-calculus terms induced by the embedding into fusions does not coincide with a barbed congruence or equivalence in the π-calculus.

Remark 5 (π and existing symmetric calculi). π contains the π-calculus, and hence contains (the typed version of) πI, the π-calculus with internal mobility (see [START_REF] Sangiorgi | The Pi-Calculus: a theory of mobile processes[END_REF]). On the other hand, because free inputs and free outputs are not allowed to interact in π, π fails to represent the fusion calculus. As mentioned above, we have not succeeded in defining a 'symmetrical version' of i/o-types that would be suitable for fusions.

Application: Relating Encodings of the λ-calculus

In this section, we use π to reason about encodings of the (call-by-name) λcalculus into the π-calculus. To do so, we need to extend π (Section 3.1). We then justify the validity of a transformation that makes use of link processes in Section 3.2. Finally, we show how duality, together with the latter transformation, allows us to relate Milner's encoding with the one of van Bakel and Vigliotti.

Extending π

Based on π, we develop an extension, called π a , with forms of asynchronous communication and polyadicity. The extension to polyadic communication is standard. Asynchronous communication is added via the inclusion of delayed prefixes: a(x):P (resp. a(x):P ) stands for a (bound) delayed input (resp. output) prefix. The intuition behind delayed prefixes is that they allow the continuation of the prefix to interact, as long as the performed action is not causally dependent on the prefix itself -this is made more precise below. Intuitively asynchrony is useful when reasoning about encodings of the λ-calculus because in a β-reduction (λx.M )N → M [N/x] the "output" part N has no continuation. It is also useful to have asynchrony in input because the considered λ-strategy allows reduction under a λ-abstraction. Moreover asynchrony allows us to derive some transformation laws involving link processes (Section 3.2). Note that synchronous prefixes are still necessary, to encode the argument of an application. Delayed prefixes are typed like bound input and output prefixes in Section 2. Types are refined with two new sorts that enforce asynchrony: d to force inputs to be bound and delayed, a to force outputs to be bound and delayed -we call such outputs asynchronous. For instance, if we have a : ♯ r d T for some T , then all inputs at a are bound and delayed. We also include recursive types.

T ::= c t s1 T 1 , . . . , sn T n | 1 | µX.T | X s ::= e | r t ::= d | a
In the polyadic case, e/r sorts are given to each element of the transmitted tuple. We present here only the typing rule for delayed input, in polyadic form, to illustrate how we extend the type system of Section 2.

Γ ⊢ a : i t s1 T 1 , . . . sn T n Γ, x 1 : T s1 1 , . . . , x n : T sn n ⊢ P Γ ⊢ a(x 1 , . . . , x n ):P (with T r = T and T e = T ↔ ). The sort d (resp. a) is forbidden in the rules to type non-delayed input (resp. output) prefixes.

The definition of operational semantics is extended as follows to handle delayed prefixes (below, ρ(y)P stands for either ρ(y).P or ρ(y):P ):

P | ρ(x):Q ≡ ρ(x):(P | Q) if x / ∈ fn(P ) ρ 1 (y):ρ 2 (x):P ≡ ρ 2 (x):ρ 1 (y):P if n(ρ 1 ) = x, x = y, y = n(ρ 2 ) (νy)ρ(x):P ≡ ρ(x):(νy)P if x = y, y = n(ρ) ρ(x):(ρ(y)P | Q) → (νy)(P | Q)[y/x] ρ(x):(ρb.P | Q) → (P | Q)[b/x] ρ(x):P → ρ(x):Q if P → Q
Barbs are defined as in Section 2, with an additional clause saying that if ρ is a barb of P and n(ρ) = x, then ρ is a barb of ρ ′ (x):P .

The results of Section 2 hold for this extended calculus, with similar proofs:

Proposition 3 (Duality, extended calculus).

1. Duality of typing: Γ ⊢ P ⇒ Γ ⊢ P . 2. Duality of barbed congruence:

Γ ⊲ P ∼ = c Q ⇒ Γ ⊲ P ∼ = c Q.
The counterpart of Theorem 2 also holds in π a , which stands for the extended calculus of this section, where types also specify how names have to be used in delayed prefixes. It can be stated w.r.t. π io,a , which is defined as π io with additional typing information to specify which names have to be used asynchronously.

Theorem 3 (Conservative extension, extended calculus). Suppose we have

Γ ⊢ P, Q in π io,a . Then Γ ⊲ P ∼ = c Q (in π io,a ) iff Γ r ⊲ P ∼ = c Q (in π a ) .
The extensions π a and π io,a are asynchronous versions of π and π io in the sense that interaction is no longer a synchronous handshaking between two processes: for at least one of the processes, the occurrence of the interaction is not observable because the consumed action is not blocking for a continuation.

3.2 Reasoning about Links, a transformation from o e a to i r a

The main result of this section is a technical lemma about the validity of a transformation which is used for the analysis of λ-calculus encodings in Section 3.3. A reader not interested in this result may safely skip this section. Differently from partial dualisation (Definition 7), the transformation, written • er , modifies prefixes, beyond simple dualisation, by introducing link processes. It also acts on types, by mapping e-names onto r-names. Definition 8. We set ab.P er = a(x).(x b | P er ), where x b = !x(z).bz is called a link process. We also define ρ(x).P er = ρ(x). P er and similarly for delayed prefixes. • er leaves free outputs unchanged and acts homeomorphically on the other constructors.

The transformation • er removes all free inputs and inserts free outputs (in the link process). We therefore expect it to return plain π processes. Moreover, the process computed in the translation of free input behaves as expected provided only the input capability is transmitted (the link process at the receiver's side exerts the input capability on x). Accordingly, we define T oe = µX.o e a X = o e a o e a o e a • • • , and T ir = µX.i r a X = i r a i r a i r a • • • . We let Γ ir (resp. Γ oe ) range over environments mapping all names to some c r a T ir (resp. c e a T oe ), for c ∈ {i, o, ♯}.

Lemma 8 (Typing for • er ). If Γ oe ⊢ P then Γ ir ⊢ P er for some Γ ir .

Proof. We prove by induction on P that if Γ ⊢ P then Γ ⊢ P er . In the case for ν we always introduce the type ♯ r a T ir . For bound prefixes we replace c e a T oe with c r a T ir , and for free inputs we type links with T ir types.

⊓ ⊔

As this result shows, • er yields processes that only transmit the input capability. This is reminiscent of the localised π-calculus [START_REF] Sangiorgi | The Pi-Calculus: a theory of mobile processes[END_REF] where only the output capability is passed.

It can be noted that Lemma 8 holds because we enforce a "double contract" in the typing rules (cf. Remark 1), which allows us to typecheck bound prefixes as e-names (before the transformation) and as r-names (after).

The relationship between P and P er is given in terms of barbed expansion precongruence, which is a preorder in between strong and weak barbed congruence.

Definition 9 (Barbed expansion precongruence). Barbed expansion is the largest relation ˙ such that whenever P ˙ Q,

-if P → P ′ then Q →⇒ Q ′ with P ′ ˙ Q ′ ; -if Q → Q ′ then P → P ′ or P = P ′ with P ′ ˙ Q ′ ; -P ↓ ρ implies Q ⇓ ρ, and Q ↓ ρ implies P ↓ ρ.
We call (resp. typed) barbed expansion precongruence ( c ) the induced (resp. typed) precongruence.

Lemma 9 (Properties of links).

1. a : i r a T ir , b : o r a T ir ⊲ a b c (νx)(a x | x b). 2. If Γ oe , a : T oe ⊢ P then Γ ir ⊲ P er [b/a] c (νa)(a b | P er ).
Proof. 1. The law is valid for the ordinary π-calculus (and is substitution-closed); Lemma 3 transfers the result to π. 2. By typing, a free output involving a in P er is necessarily in a link; in this case, we can use (1). The other kind of interaction is with some a(x):Q in P er , and b(x

):Q[b/a] behaves like (νa)(a b | a(x):Q[b/a]). ⊓ ⊔
We use Lemma 9 to deduce operational correspondence.

Lemma 10 (Operational correspondence). Suppose that Γ oe ⊢ P .

1. P ↓ ρ iff P er ↓ ρ.

2. If P → P ′ then P er → c P ′ er . 3. If P er → P 1 then P → P ′ and P 1 c P ′ er for some P ′ .

A version of these results in the weak case can also be proved, for barbed expansion. Notably, P and P er exhibit the same weak barbs.

Lemma 11. If Γ oe ⊢ P, Q then P ≈ Q iff P er ≈ Q er .
Proof. We show that ˙ {( P er , Q er ) | P ≈ Q} ˙ and {(P, Q) | P er ≈ Q er } are weak barbed bisimulations. We then use the adaptation of Lemma 10 to the weak case, for barbed expansion.

⊓ ⊔ Lemma 12. If Γ oe ⊢ P, Q and Γ ir ⊲ P er ∼ = c Q er then Γ oe ⊲ P ∼ = c Q.

Proof. We define a type system with marks on types, such that only T ir -types are marked. The marking propagates onto the names of the typed processes. We modify the encoding • er to only operate on marked prefixes. For every (∆/Γ oe )-context C, its encoding C er is a (∆ ′ /Γ ir )-context. Thanks to the compositionality of • er , the hypothesis of the lemma implies the equivalence C[P ] er ≈ C[Q] er . We then adapt the proof of Lemma 11 to this marked encoding.

⊓ ⊔

An analysis of van Bakel and Vigliotti's encoding

As announced in Section 1, we start from an adaptation of Milner's call-by-name (cbn) encoding of [START_REF] Milner | Functions as processes[END_REF] to strong cbn, which also allows reductions to occur under λ. We obtain this by using a delayed prefix in the clause for λ-abstraction.

The encoding, noted • M , is defined as follows:

x

M p = xp λx.M M p = p(x, q): M M q M N M p = (νq) M M q | (νx)(q x, p | !x(r). N M r )
The other encoding we analyse, taken from [START_REF] Van Bakel | A logical interpretation of the λ-calculus into the π-calculus, preserving spine reduction and types[END_REF], is written • B :

x B p = x(p ′ ):p ′ p λx.M B p = p(x, q): M B q M N B p = (νq) M B q | q(x, p ′ ).(p ′ p | !x(r). N B r )
Note that • B is written in [START_REF] Van Bakel | A logical interpretation of the λ-calculus into the π-calculus, preserving spine reduction and types[END_REF] using asynchronous free output and restriction instead of delayed bound output. We can adopt this more concise notation since (νx)(ax | P ) and a(x):P are strongly bisimilar processes, and similarly for x(p ′ ):p ′ p and x(p ′ ).p ′ p. (Another difference is that the replication in the encoding of the application is guarded, as in [START_REF] Van Bakel | Implicative logic based encoding of the λ-calculus into the π-calculus[END_REF], to force a tighter operational correspondence between reductions in λ and in the encodings.)

As remarked above, • B and • M differ considerably because they engage in quite different dialogues with their environments: in • M a function receives its argument via an input, in • B it interacts via an output. Differences are also visible in the encodings of variables and application (e.g. the use of links).

To compare the encodings • M and • B , we introduce an intermediate encoding, noted • I , which is defined as the dual of • M (in π):

x I p = xp λx.M I p = p(x, q): M I q M N I p = (νq) M I q | (νx)(q x, p | !x(r). N I r )
Note that while • M and • B can be expressed in π, • I uses free input, and does thus not define π-calculus processes. The three encodings given above are based on a similar usage of names. Two kinds of names are used: we refer to names that represent continuations (p, p ′ , q, r in the encodings) as handles, and to names that stand for λ-calculus parameters (x, y, z) as λ-variables. Here is how these encodings can be typed in π:

Lemma 13 (Typing the encodings). To establish that this is equivalent to M B p ≈ N B p , we rely on an adaptation of Lemma 11. For this, we define a transformation that exploits the ideas presented in Section 3.2. In particular, handles (p, p ′ , q, r) are treated like in Definition 8. The handling of λvariables (x, y, z) is somehow orthogonal, and raises no major difficulty, because such names are always transmitted as bound (fresh) names.

⊓ ⊔

Remark 6 (Call by name). To forbid reductions under λ-abstractions, we could adopt Milner's original encoding, and use an input prefix instead of delayed input in the translation of abstractions. Accordingly, adapting Van Bakel and Vigliotti's encoding to this strategy would mean introducing a free input prefix -which is rather natural in π, but is not in the π-calculus.

Concluding remarks

We have presented several properties of π, and established relationships with the π-calculus with i/o-types (π io ). The calculus π enjoys properties of dualities while being "large", in the sense that it incorporates many of the forms of prefix found in dialects of the π-calculus (free input, bound input, and, in the extension in Section 3.1, also delayed input, plus the analogue for outputs), and a non-trivial type system based on i/o-types. This syntactic abundance makes π a possibly interesting model in which to study various forms of dualities. This is exemplified in our study of encodings of the λ-calculus, where we have applied π and its theory to explain a recent encoding of cbn λ-calculus by van Bakel and Vigliotti: it can be related, via dualities, to Milner's encoding.

It would be interesting to strengthen the full abstraction in Lemma 11 from barbed bisimilarity to barbed congruence. This would allow us to replace barbed bisimilarity with typed barbed congruence in Proposition 4 as well (using the type environments of Lemma 13). While we believe the result to be true, the proof appears difficult because the link transformation modifies both processes and types, so that the types needed for barbed congruence in the two encodings are different. Therefore also the sets of contexts to be taken into account are different. The problem could be tackled by combining the theory on delayed input and the link bisimilarity in [START_REF] Merro | On asynchrony in name-passing calculi[END_REF], and adapting it to a typed setting.

We plan to further investigate the behavioural theory of π, and study in particular other transformations along the lines of Section 3.2, where link processes are used to implement substitutions. It would be interesting to provide general results on process transformations in terms of links, when the direction and the form of the links vary depending on the types of the names involved. Currently we only know how to handle them when the calculus is asynchronous and localised [START_REF] Merro | On asynchrony in name-passing calculi[END_REF].

As already mentioned, another interesting issue is how to accommodate i/otypes into πI and fusion calculi while maintaining the dualities of the untyped calculi.

  1. (Weakening) If Γ ⊢ P then Γ, a : T ⊢ P . 2. (Strengthening) If Γ, a : T ⊢ P and a ∈ fn(P ) then Γ ⊢ P . 3. (Narrowing) If ∆ ≤ Γ and Γ ⊢ P then ∆ ⊢ P . 4. (Substitution) If Γ, x : T ⊢ P and Γ ⊢ b : T then Γ ⊢ P [b/x].

  Proof. Soundness: given a derivation γ :: ∆/Γ ⊢ C, we build [C] γ which is a (∆ * /Γ * )-context. Then [C] γ [[P ] δP ] = [C[P ]] βP for some β P and we can rely on barbed congruence in π io 2 to establish [C[P ]] βP ≈ [C[Q]] βQ . By Lemma 6, we deduce C[P ] ≈ C[Q]. Completeness: we define the reverse translation {•} of [•] and reason as above to prove its soundness. Thanks to the fact that δ P :: Γ ⊢ P implies {[P ] δP } δ * P = P where δ * P :: Γ * ⊢ [P ] δ is the derivation obtained by Lemma 4, the soundness of {•} implies the completeness of [•] , and vice versa.

  moving from Γ to Γ * , we replace i e (resp. o e , i r , o r ) with o (resp. i, i, o). This transformation preserves the subtyping relation. Moreover, the rules to type prefixes i r , o r , i e , o e in π correspond to the rules for i, o, o, i in π io 2 . ⊓ ⊔ Lemma 5. Whenever δ 1 :: Γ ⊢ P and δ 2 :: Γ ⊢ P , we have Γ * ⊲ [P ] δ1 ≃ c [P ] δ2 . } is a strong bisimulation in π and is substitution-closed; hence R is included in ≃ c , since [P ] δi is typable in Γ * (by Lemma 4).

Proof. The relation

R △ = {([P ] δ1 , [P ] δ2 ) | δ 1 , δ 2 :: Γ ⊢ P ⊓ ⊔

Lemma 6. If δ P :: Γ ⊢ P and δ Q :: Γ ⊢ Q then we have the following:

1. (P and Q have the same barbs) iff ([P ] δP and [Q] δQ have the same barbs) 2. if P → P ′ then [P ] δP → [P ′ ] δ for some δ :: Γ ⊢ P ′ . 3. if [P ] δP → P 1 then P 1 = [P ′ ] δ with P → P ′ for some δ :: Γ

  • M , • B and • I yield processes which are typable with the respective typing environments Γ M , Γ B , Γ I , where: I is the dual of Γ M (that is, it uses i e d H and H = µZ.o e a i e d Z, Z ). Encoding • I can be obtained from • M by duality. The only difference between • I and • B is the presence of two links. We rely on a link transformation similar to the one of Section 3.2 to move from • I to • B . Thus, by composing the results on duality and on the transformation, we are able to go from • M to • B . Proposition 4. Given two λ-terms M and N , we have M M p ≈ N M p if and only if M B p ≈ N B p (both equivalences are in π io,a ).

	-Γ M types λ-variables with o r a H and handles with H = µX.i r d o r a X, X ;
	-Γ B uses respectively i r d G and o r a o r d G, G where G = µY.i r a o r d Y, Y ;
	-Γ Proof. By duality, M M

p ≈ N M p iff M I p ≈ N I p .

Γ ⊢ a : i r T Γ, x :T ⊢ P Γ ⊢ a(x).P Γ ⊢ a : i e T Γ, x : T ↔ ⊢ P Γ ⊢ a(x).P Γ ⊢ a : o e T Γ, x : T ⊢ P Γ ⊢ a(x).P Γ ⊢ a : o r T Γ, x : T ↔ ⊢ P Γ ⊢ a(x).P Γ ⊢ a : i e T Γ ⊢ b : T Γ ⊢ P Γ ⊢ ab.P Γ ⊢ a : o r T Γ ⊢ b : T Γ ⊢ P Γ ⊢ ab.P Γ, a : T ⊢ P Γ ⊢ (νa)P Γ ⊢ P Γ ⊢ Q Γ ⊢ P | Q Γ ⊢ P Γ ⊢ !P Γ ⊢ 0

Acknowledgments. This work was supported by the french ANR projects Recre, 2009-BLAN-0169-02 Panda, and 2010-BLAN-0305-01 PiCoq.


Pierre-Henri Merrer
email: phmerrer@laas.fr

Khaldoun Saleh

Olivier Llopis

S Berneschi

F Cosi

G Nunzi Conti

Characterization technique of optical whispering gallery mode resonators in the microwave frequency domain for optoelectronic oscillators

Optical Q factors measurements are performed on a Whispering Gallery Mode (WGM) disk resonator using a microwave frequency domain approach instead of using an optical domain approach. An absence of hysteretic behavior and a better linearity are obtained when performing linewidth measurements by using a microwave modulation for scanning the resonances instead of the piezoelectric based frequency tuning capability of the laser.

The WGM resonator is then used to stabilize a microwave optoelectronic oscillator. The microwave output of this system generates a 12.48 GHz signal with -94 dBc/Hz phase noise at 10 kHz offset.

Introduction

Investigations towards high spectral purity sources are a very important and interesting point in the microwave field, concerning many applications ranging from communications and radar to time-frequency metrology. The need for microwave sources able to provide high frequency (10 to 100 GHz), versatility of the output frequency and low phase noise signal is growing in response to advances in technology related to optical communication links, requiring an efficient high-data-rate system, and radar systems, requiring the detection of weak signals from a dense background clutter. Two classical approaches can be distinguished for high spectral microwaves sources: the use of quartz or SAW (surface acoustic wave) oscillators at low frequencies, which can be multiplied up to the desired frequency, or, the use of dielectric resonator oscillators, which includes ceramic and monocrystalline resonators (mainly sapphire) [START_REF] Cibiel | Optimization of an ultra low-phase noise sapphire-SiGe HBT oscillator using nonlinear CAD[END_REF]. In the first case, the multiplication entails a degradation of the phase noise of 20logN, with N being the multiplication factor. In the other case, the main problem with ceramic resonator is that its quality factor (Q) is inversely proportional to the frequency. In the special case of sapphire resonator, the disadvantage is its size because it is based on high order modes. Finally, the technologies for high spectral purity microwave sources are reaching their limits when the goal is to get simultaneously high performance in term of phase noise, high operation frequency and small size, especially in embedded systems.

A solution to overcome these limitations is to carry the microwave signal on another wave, such as an acoustic wave or an optical wave. The case of the acoustic wave is today investigated in thin film bulk acoustic wave resonators. This approach allows obtaining a small size about 100 µm², which focus the wireless market [START_REF] Campbell | Surface acoustic wave devices for mobile and wireless communications[END_REF]. However these resonators are limited in their operating frequency (up to 5 GHz) and their Q factor values (in the range of 500). The case of optics is different: what we are looking for is very high performance at higher frequencies.

The operation principle uses an optical carrier, delivered by a laser, a modulator, to transpose the microwave signal around the optical carrier, an optical frequency reference device (resonator or delay line) and a fast photodiode to bring back the signal to microwaves. It is today a well known technique, already commercialized, and this type of oscillator is known as an optical-electronic oscillator (OEO). The first OEO has been proposed in 1994 [START_REF] Yao | High frequency optical subcarrier generator[END_REF]. This type of source is based on an optical delay line, and features today ultra low phase noise performance (ex: -163 dBc/Hz at 10 kHz offset of a 10 GHz carrier [START_REF] Eliyahu | RF Amplitude and phase-noise reduction of an optical link and an opto-electronic oscillator[END_REF]). However, these oscillators are quite bulky because of the fiber spool and their phase noise spectrum features many parasitic modes due to the large number of frequencies for which a 2π phase condition is realized in these devices. Some improvements of this approach, based on the coupling of an optical oscillator and a microwave oscillator (COEO), have demonstrated again the great potential of this approach to reach very low phase noise levels [START_REF] Eliyahu | Modulation response (S21) of the coupled opto-electronic oscillator[END_REF].

An alternative approach can be to replace the optical fiber delay line by a whispering gallery mode (WGM) optical resonator [START_REF] Savchenkov | Whispering-gallery mode based opto-electronic oscillators[END_REF]. These resonators can be fabricated with crystalline material, such as calcium fluoride (CaF 2 ), to achieve extremely high Qs [START_REF] Savchenkov | Optical resonators with ten million finesse[END_REF]. Further improvement of OEO parameters can be achieved with this solution. Firstly, the size of the optical resonator is quite small, because of the small wavelength of the optical signal. Thus, the microwave signal carried by the optical carrier can be trapped in a resonator much smaller than the microwave wavelength. In this case, the microwave oscillation frequency is defined by the free-spectral-range (FSR) of the WGM resonator. Moreover, in opposition to the case of dielectric resonators, the equivalent microwave Q factor increases with the microwave frequency. This technology appears to be a disruptive technology in the field of microwave sources.

In this paper, we report on a characterization method for high-Q optical whispering gallery mode disk resonators in the microwave domain. This approach allows a measurement of the resonance characteristics of these resonators with a very good linearity. Moreover, the measured data is obtained in the same way the resonators are used afterwards in an OEO system, and the measured Q factor is the OEO Q factor. We briefly describe the polishing procedure of crystalline disks and the coupling method in order to trap laser light into the ultra-low loss WGMs. We then present in detail the experimental setup and the resonator characterization procedure. Finally, we present the experimental results on phase noise measurement of the OEO.

Fabrication of WGM resonator and coupling method

Special equipment was developed for manufacturing optical resonators based on calcium fluoride disks (about 5.5 mm in diameter). These disk-resonators were made from commercial 0.5 mm thick CaF 2 windows by core drilling a cylinder and thereafter polishing the edge into a spheroidal shape. We have optimized the polishing procedure of crystalline disks using a homemade lapping station, which is shown in Fig. 1. The almost spherical profile is obtained through a rotational stage whose pivot point can be finely adjusted. The polishing protocol is divided in six successive steps starting with an initial two-step grinding phase (disks with abrasive size of 12 and 9 microns) which is followed by a four-step finer polishing phase, based on polycrystalline diamond suspensions with decreasing grit sizes (3, 1, 0.25, and 0.05 microns, respectively). After each step a rather critical cleaning procedure using organic solvents has been implemented.

Concerning the coupling method, several techniques have been investigated in order to obtain a selective and efficient coupling into the WGM resonator. The oldest method and the common technique is the prism coupling configuration [START_REF] Braginsky | Quality-factor and nonlinear properties of optical whispering-gallery modes[END_REF]. This approach can be compacted using an angle polished optical fiber [START_REF] Ilchenko | Pigtailing the high-Q microsphere cavity: a simple fiber coupler for optical whispering-gallery modes[END_REF]. We have chosen here an alternative method that enables high efficiency coupling directly from optical fiber where it is possible to obtain the total transfer of the incoming power to the WGM [START_REF] Cai | Highly efficient optical power transfer to whispering-gallery modes by use of a symmetrical dual-coupling configuration[END_REF]. Indeed, tapered optical fibers meet the key requirements for a good performance and easy coupling: phase matching and sufficient overlap between the evanescent electromagnetic fields. Phase-matching is accomplished by matching the taper propagation constant to the WGM's propagation constant while the overall coupling strength varies exponentially with the air gap between the resonator and the taper. In practice, these coupling conditions can be optimized by varying the position of the resonator along the biconical fiber taper (which has a variable waist diameter along its length), and by controlling the air gap distance. The minimum taper diameter in our work is typically less than 1 µm, with loss levels of less than 1 dB. They are made by heating a single-mode silica fiber (typically SMF-28) with a torch and slowly pulling the fiber. Phase matching is possible because CaF 2 and silica have similar refractive indices at 1550 nm. A dedicated measurement bench has thus been set up, using three-axis piezoelectric nanometric stage (P-611 Nanocube XYZ piezo stage) to accurately position the tapers with respect to the optical resonator. The tapers are kept with a slight tension and the measurement bench has been built on an optical table in order to minimize the influence of vibrations. This allows us to get an efficient dual-coupling with tapered fibers. A schematic of the coupling system is show in Fig. 2. Two nearly identical taper couplers are placed tangentially at the opposite sides of the disk. One serves as the input coupler, and the other as the output coupler.

Resonator characterization

The first step in OEO studies is to set up a characterization bench for the resonators to be used in the OEO. It is essential to test the resonator behavior in a configuration which is as close as possible to the OEO system. The microwave characterization bench is depicted in Fig. 3. The test configuration, which has been developed was clearly dedicated to OEO design. In general the light coupled inside the WGM resonator induces a power dependent thermal shift of the mode frequency leading to thermal instability. It was demonstrated [START_REF] Carmon | Dynamical thermal behavior and thermal self-stability of microcavities[END_REF][START_REF] Del'haye | Full stabilization of a microresonator-based optical frequency comb[END_REF] that the frequency drift due to the resonator self heating can be used for thermal locking of the laser frequency to the WGM.

This technique is not applicable in the case of Q-factor measurement, which must not be perturbed by thermal nonlinearity. Thus, a more robust frequency locking mechanism has been set up using a Pound Drever Hall (PDH) feedback loop [13 -15]. The validity of this approach has been verified experimentally on a different type of optical resonator featuring similar Q factor: the fiber ring resonator [START_REF] Merrer | Laser stabilization on a fiber ring resonator and application to RF filtering[END_REF]. As soon as the laser is locked onto the resonance, it is possible to use the system for microwave applications. The laser used in this configuration is a fiber laser (Koheras Adjustik) with a very narrow linewidth (1 kHz). A microwave optical intensity modulator (Mach-Zehnder modulator, MZM) is added to the system and we use an allfiber polarization controller in order to select TE or TM modes. The signal coming out from a microwave network analyzer (Anritsu 37347A) feeds the modulator, goes through the optical resonator and is finally recovered on a fast photodiode and analyzed on port 2 of the vectorial network analyzer (VNA). The bandwidth of the MZM and the photodiode is around 20 GHz, which is larger than the FSR of the WGM resonator. ) and the linear fit of the MZM frequency response is obtained by the calibration of the VNA. The most common optical method used to characterize high-quality resonators, based on a slow scan of the wavelength of a narrow probe laser, which is obtained from a piezoelectric device (acting either directly on the grating of DFB fiber lasers or on the mirror of external cavity semiconductor laser) [START_REF] Schmidt | Nonlinear thermal effects in optical microspheres at different wavelength sweeping speeds[END_REF][START_REF] Merrer | High-Q optical resonators for laser stabilization in microwave photonics oscillators[END_REF], cannot achieve this linearity. Fig. 5 shows the hysteretic behavior of our laser output wavelength vs piezoelectric component voltage. At a fixed wavelength we encounter different slopes depending on the scanning direction. Additionally same non linearity may be also observed in the same graph. On the contrary the only requirement of the microwave approach is to able to lock the laser frequency close to the center of the resonance frequency. Fig. 6a shows an example of such a measurement from 5 GHz to 20 GHz performed on our CaF 2 disk at the through port, when the laser carrier is locked to the fundamental WGM. Fig. 6b focuses on this mode and Fig. 6c gives the information on its resonance half bandwidth (δν) and Q factor (Q = ν /δν) at the drop port.

The measured Q factor at the drop port is about 8.4x10 7 .

Optoelectronic oscillator

As previously stated, one of the basic issues in the realization a WGM-based OEO is the locking of the optical carrier onto one of the fundamental WGM in order to avoid thermal nonlinearities.

The same approach using a low frequency PDH feedback loop may be applied to stabilize the laser on a WGM resonance. A microwave feedback loop is then used to start an oscillation on one of the lateral side-modes of the resonator. This high frequency loop contains amplifiers, attenuators and a phase shifter in order to adjust the conditions for the oscillation start up. The OEO set-up is depicted in Fig. 7. The power at the CaF 2 disk entrance is about 4.5 dBm. The coupling with tapered optical fiber is rather efficient (3 dB insertion losses) so the power at the drop port is 1.5 dBm. A 3 dB optical coupler is placed before the photodiode in order to perform the phase noise measurement and the power on the photodiode is Pm = -2.5 dBm (phase noise measurement is performed in a 20 m remote location, and the signal is brought to the signal analyser through optical fiber). The high frequency loop includes two RF amplifiers: the first one with a gain of 34 dB and the second one with a gain of 25 dB. A 10 dB RF splitter allows to measure the spectrum of the microwave signal generated in the OEO and an attenuator with 11 dB attenuation is placed after the first amplifier. The RF power at the photodiode output in operating OEO is about 10 µW and the power at the input of the MZM is 19.5 dBm. The oscillation features 8 dBm output power and is obtained with 48 dB RF amplification. As theoretically predicted [START_REF] Matsko | Optical resonators with whispering-gallery modes-part I: basics[END_REF], the system has an oscillation frequency equal to the resonator FSR (12.481 GHz).

Fig. 8 shows a typical phase noise spectrum of the OEO referenced on a CaF 2 disk. This phase noise has been measured for a frequency offset, f m , ranging from 10 Hz to 100 MHz. The phase noise spectrum features different slopes. In the first one, between 10 Hz and 10 kHz, the noise slope of -30 dB/dec corresponds to an important 1/f frequency noise contribution. This 1/f frequency noise may be due to some optical noise conversion processes in the oscillating system, or to the laser PDH stabilization loop, or of another source of 1/f noise such as the 1/f noise of amplifiers or of the photodiode. The white frequency noise is characterized by a slope of -20 dB/dec from 10 kHz to 700 kHz, and it is linked to the Q-factor and to the noise to carrier ratio (NCR) of the optical part of the system. The phase noise floor appears after 700 kHz, and features a value of about -133 dBc/Hz.

The expected phase noise of the OEO, or at least the contributions other than the one of the 1/f noise, can be calculated using a simplified model of the OEO, following Leeson's approach [START_REF] Leeson | A simple model of feedback oscillator noise spectrum[END_REF]. Such a model leads to the following equation ( 1), which depends on the experimental parameters such as the microwave equivalent quality factor Q, the measured optical power P m , the sensitivity of the photodiode R(λ), the modulation index m, the microwave frequency ν, the offset frequency f m and the different noise contributions to the NCR.

( ) ( ) ( )         + + +         = 2 2 2 m shot th RIN m m m R P S S S 2 10log Q 2 2 ν 20log f L f λ (1)
with the thermal noise being S th [START_REF] Campbell | Surface acoustic wave devices for mobile and wireless communications[END_REF], the shot noise S shot [START_REF] Yao | High frequency optical subcarrier generator[END_REF] and the laser noise S RIN (4) :

R T 4k S B th = (2) ( ) m shot P λ 2qR S = (3)
( ) RIN λ R P S 2 2 m RIN = (4)
where T is the room temperature, k B is the Boltzmann constant, q is the electron charge, RIN is the relative intensity noise of the laser and R is the photodiode load resistance. This model is of course only valid in the frequency range on which the phase noise is dominated by the white frequency or phase noise contribution (additive noise effect). Knowing in our setup that P m = -2.5 dBm, R(λ) = 0.8 A/W, m = 0.8, R = 50 Ω, and RIN = -148 dBc/Hz, we can compare the simulated white phase noise with the experimental results (see Fig. 8) Finally, the phase noise performance is evaluated to be -94 dBc/Hz at 10 kHz from the carrier, and -116 dBc/Hz at 100 kHz. This phase noise level is better than the one recently demonstrated in [START_REF] Volyanskiy | Compact optoelectronic microwave oscillators using ultra-high Q whispering gallery mode disk-resonators and phase modulation[END_REF], even though the oscillator generating a 10.7 GHz signal was based on a resonator having a similar Q factor (however the two OEOs topologies are very different). This performance is close to the one of commercially available microwave dielectric resonator oscillators (DROs). However, the increase in Q factor of the optical resonator by 10 to 100 times would result in a reduction by 20 to 40 dB in the OEO phase noise, and such ultra high Qs have already been demonstrated in this type of resonators, although DRO technology is an old technology which is close to its limits in performance.

Conclusion

Optical resonators allow reaching really high quality factors in the microwave range. This technology overcomes some limitations of conventional microwave technology for the development of high spectral purity microwave sources. In this paper, an accurate microwave characterization technique dedicated to optical high Q resonators has been reported. This method allows assessing resonators optical Q factor from linewidth measurements by using a microwave modulation for scanning the resonances instead of an optical frequency modulation. An improved linearity and absence of hysteretic behavior are obtained with this approach. A X-band microwave source using a CaF 2 disk resonator and efficient dual-coupling with tapered fibers has then been realized. Even if the measured phase noise performance of this OEO is still modest, Even if the measured phase noise performance of this OEO is still modest, this performance will

Fig. 4

 4 represents the MZM frequency response measured with the VNA. The bandwidth is defined as the -3dB high cut-off frequency of the S 21 curve. The power deviation of the S 21 curve can be taken into account by doing a calibration of VNA, in order to obtain a linear fit of the MZM frequency response in the frequency range 5 GHz to 20 GHz. The WGM Q factor can then be measured as the laser carrier is locked onto one of the resonances while the microwave source of the VNA is scanning the WGM resonances with the laser sidebands in the MZM bandwidth. The relative frequency difference between the optical carrier and its sidebands is precisely defined by the microwave source which is accurately controlled in frequency. We therefore get the resonance profile of the WGMs in the microwave domain, instead of a direct measurement in the optical domain. An absence of hysteretic behavior is obtained on these measurements thanks to the MZM biased close to its linear modulation voltage (ܸ = ܸഏ మ

Fig. 1 :

 1 Fig.1: (Color online) Monocrystalline disk polishing station with the CaF2 disk magnified in

Fig. 2 .

 2 Fig.2. (Color online) Picture (a) and scheme (b) of the dual-coupling system with tapered

Fig. 3 .Fig. 4 .

 34 Fig.3. (Color online) Experimental setup of the microwave characterization technique used to

Fig. 5 .

 5 Fig.5. Hysteretic behavior of our Koheras Adjustik laser tuning mechanism based on a

Fig. 6 .

 6 Fig.6. (a) (Color online) Measured spectrum of a CaF 2 disk at the through port using the

Fig. 7 .Fig. 8 .

 78 Fig. 7. (Color online) Experimental setup of the WGM-based OEO. A : microwave amplifier,

certainly improve in the future thanks to a better understanding of the noise processes (specially the 1/f noise) and an improvement of the resonator technology. This work was supported by the funding from ANR (National Research Agency) project "ORA" 2010 BLAN 0312 03.