Pierre-Marie Pédrot
email: pierre-marie.pedrot@fmf.uni-lj.si

Nicolas Tabareau
email: nicolas.tabareau@inria.fr

An Effectful Way to Eliminate Addiction to Dependence

We define a monadic translation of type theory, called weaning translation, that allows for a large range of effects in dependent type theory-such as exceptions, non-termination, non-determinism or writing operation. Through the light of a call-by-push-value decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially, the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of the Calculus of Inductive Constructions (CIC) with a restricted version of dependent elimination. Finally, we show how to recover a translation of full CIC by mixing parametricity techniques with the weaning translation. This provides the first effectful version of CIC.

I. INTRODUCTION

The gap between type theories such as CIC and mainstream programming languages comes to a large extend from the absence of effects in type theories, because of its complex interaction with dependency. For instance, it has already been noticed that inductive types and dependent elimination do not scale well to CPS translations and classical logic [START_REF] Barthe | Cps translating inductive and coinductive types[END_REF], [START_REF] Herbelin | On the degeneracy of sigma-types in presence of computational classical logic[END_REF]. Furthermore, the traditional way to integrate effects in functional programming using monads does not scale to dependency because the monad leaks in the type during substitution.

In this paper, we propose Baclofen Type Theory (BTT), a stripped-down version of CIC, and we provide generic notion of syntactic models 1 of it that allows for a large range of effects in dependent type theory-exceptions, non-termination, non-determinism or writing operation. BTT has a restricted version of dependent elimination to overcome the difficulty to marry effect and dependency. The syntactic models are given by the weaning translation of BTT into CIC, using a variant of the traditional monadic translation. The need for this variant can be explained by analyzing the call-by-push-value (CBPV) decomposition of call-by-value and call-by-name reduction strategies. Crucially, our construction requires that the universe of algebras of the monad forms itself an algebra. A monad satisfying this property is said to be self-algebraic. We then show how very common monads satisfy this property and thus give rise to effects that can be integrated to BTT.

Finally, by mixing parametricity techniques with the weaning translation, we show how to recover a translation of full CIC, giving rise to the first effectful version of CIC. 1 By syntactic models, we mean a model directly expressed in a type theory through a program transformation, as advocated in [START_REF] Boulier | The next 700 syntactical models of type theory[END_REF].

Plan of the paper.

In Section II, we explain the main points of the construction through the CBPV decomposition. Then, Section III and IV describe the weaning translation for self-algebraic protomonads on BTT. Section V describes various instances of selfalgebraic proto-monads and their asociated effects. Section VI presents a linearity condition to ease the use of BTT on non-recursive inductive types and finally Section VII explains how a mild modification of the weaning translation using parametricity techniques allows one to recover a translation of full CIC.

Plugin implementation.

As it is the case for other syntactic models [START_REF] Jaber | The definitional side of the forcing[END_REF], [START_REF] Boulier | The next 700 syntactical models of type theory[END_REF], it is possible to implement the weaning translation as a Coq plugin. The plugin is available at https://github.com/CoqHott/ coq-effects.

II. GENESIS OF THE CONSTRUCTION

This section presents a global overview of the weaning translation given in this paper. It is based on two key ingredients that allow us to define a monadic translation of CIC for a large range of effects: i) the use of the call-by-name decomposition in Levy's call-by-push-value [START_REF] Levy | Call-by-push-value[END_REF] (CBPV) and ii) its instantiation with Eilenberg-Moore algebras for selfalgebraic monads.

A. The two canonical decompositions of a monad.

The use of monads to interpret effects in functional programming languages comes back from the seminal work of Moggi [START_REF] Moggi | Notions of computation and monads[END_REF]. In its traditional view, the monadic interpretation amounts to consider functions from A to B as functions of type A → T B where T is a computational monad. From a categorical point of view, this interpretation consists in working in the Kleisli category C T induced by a monad T on C, where the objects are those of C and the morphisms of C T (A, B) are given by C(A, TB). Actually, the Kleisli category is one of the two canonical notions of category of computations that is part of a left and right adjoints decomposition of the monad,

C F T < < C T U T } }
where F T is the identity on objects, U T is equal to T on objects and U T • F T = T. There is another canonical decomposition where the category of computations is given by algebras of the monad, i.e., objects A with an arrow T A → A compatible with the monadic operations. The category of algebras C T , called the Eilenberg-Moore category, is part of the adjunction

C F T = = C T U T } }
where F T is equal to T on objects, U T is equal to the identity on objects and U T • F T = T. This notion of computations has not given rise to a monadic interpretation in functional programming languages because the existence of the algebraic structure appears as a side condition difficult to encode in the absence of dependent types. To the opposite, the Kleisli category was more suited because it corresponds to the subcategory of free algebras of C T , and thus the algebraic nature of computational types can be canonically encoded in the interpretation of the arrow.

B. Call-by-name decomposition in CBPV.

The first observation, that was already made in [START_REF] Jaber | The definitional side of the forcing[END_REF], is that the traditional monadic interpretation is call-by-value whereas type theories such as CIC are fundamentally call-by-name. The latter fact comes from the independence on the order of evaluation hardcoded in the conversion rule. We advocate that CBPV allows to clarify the situation by decribing both callby-value and call-by-name as two distinct decompositions, leading to a more atomic presentation. CBPV's types (and terms) are divided into two classes: pure values and effectful computations. It is possible to go from one to the other using the two type constructors U and F that mimic the two parts of the adjunction decomposing a computational monad (see Figure 1). Call-by-name and call-by-value strategies can then be decomposed into CBPV, inducing in turn two monadic translations for the simply-typed λ-calculus.

The by-value decomposition [-]

v is defined on arrows as

[A → B] v := U ([A] v → F [B] v )
whereas the by-name decomposition [-] n is defined as

[A → B] n := U [A] n → [B] n .
Kleisli adjunction and forcing. When U and F are instantiated by the Kleisli adjunction for the reader monad, we recover the forcing translation. It has already been noticed in [START_REF] Jaber | The definitional side of the forcing[END_REF] that the by-value decomposition corresponded to the usual presheaf construction, while the by-name decomposition was the one preserving the conversion rule of type theory.

Eilenberg-Moore adjunction and monadic translations. We now observe that dually, when U and F are instantiated by the Eilenberg-Moore adjunction, we recover, in the call-by-value decomposition, the usual monadic interpretation for which value types A, B :: A → B is interpreted by A → T B. Quite surprisingly, we recover the definition of an arrow in the Kleisli category whereas we are using the Eilenberg-Moore adjunction. This is simply because the by-value decomposition forces one to consider only the free algebras of the monad, whose category is equivalent to the Kleisli category.

= U X | α computation types X, Y ::= A → X | F A
C. By-name Eilenberg-Moore translation for CIC.

The defect of the by-value decomposition comes from the fact that, as CIC is call-by-name, the correctness of the translation requires too many definitional equalities to hold. We advocate in this paper that this is solved by considering by-name decomposition of the Eilenberg-Moore adjunction. In that case, as U is the identity, the dependent product is translated transparently. Types are translated as plain algebras (i.e., without coherence requirement), which can be easily expressed by the dependent sum

i = ΣA : i . T A → A. (1)
But in CIC, universes satisfy a kind of self-enrichment expressed as i : i+1 . Thus, to get a correct interpretation of universes, the monad needs to satisfy the additional requirement that the type of algebras needs to be itself an algebra of the monad, that is morally i : i+1 . A monad satisfying this property will be called a self-algebraic monad. It is at the heart of the definition of the weaning translation given in the following section.

III. WEANING TRANSLATION OF CC ω

This section describes the weaning translation for the negative fragment of CIC, namely CC ω plus Σ-types, whose typing and computation rules are given in Figure 2. It is based on the notion of self-algebraic proto-monad. Definition 1. A self-algebraic proto-monad is given by the following family of terms:

• T : i → i • ret : ΠA : i . A → T A • bnd : Π(A : i ) (B : j ). T A → (A → T B) → T B • El : T i → i • hbnd : Π(A : i ) (B : T j ).
T A → (A → (El B).π 1 ) → (El B).π 1 where the universe indices i, j are implicitly universally quantified and i is defined in [START_REF] Barthe | Cps translating inductive and coinductive types[END_REF], furthermore subject to the following definitional equation: propositionally. Furthermore, the self-algebraic quality is given by the El primitive, which intuitively endows i with a structure of T-algebra, even though it is not a formal requirement. Actually, we could make the connection with category theory more precise by asking for propositional equality for the rest of the laws. But propositional equalities cannot be of any use in the syntactical translation because using them would create higher coherence issues, and since the inception of Homotopy Type Theory [START_REF] Univalent | Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF], it is well-known that this turns out to be a subtle matter. Remark 1. It looks like it is possible to use the fact that (El B).π 1 is always equipped with a weak algebra structure given by (El B).π 2 to canonically derive the heterogeneous binding operation hbnd out of bnd as

El (ret i M ) ≡ M . Γ M : A Γ N : B{x := M } Γ Σx : A. B : i Γ (M, N ) : Σx : A. B (M, N ).π 1 ≡ M (M, N ).π 2 ≡ N
hbnd := λA B M F. (El B).π 2 (bnd _ _ M (λx : A. ret _ (F x)))
but this does not work to interpret inductive datatypes. In general, the resulting term would not satisfy the crucial definitional equation of Definition 3. Remark 2. For a given monad T, there can be several algebra structures on i , and thus distinct implementations for El as discussed in Section V.

In what follows, we will be using the typical ambiguity of type theory, and we will not explicit the universe indices of the various universe-polymorphic terms. It would be possible to do so at the cost of annotating the type-formers of the source theory, but we consider that the additional burden would not bring more insight into the translation.

[ i ] := ret i+1 ((T i ), µ i ) [x] := x [λx : A. M ] := λx : [[A]]. [M ] [M N ] := [M ] [N ] [Πx : A. B] := ret ((Πx : [[A]]. [[B]]), µ ΠAB ) [[A]] := (El [A]).π 1 µ i := λA : T (T i ). bnd (T i ) i A (λX : T i . X) µ ΠAB := λ( f : T (Πx : [[A]]. [[B]])) (x : [[A]]). hbnd (Πx : [[A]]. [[B]]) [B] f (λf : Πx : [[A]]. [[B]]. f x) [[•]] := • [[Γ, x : A]] := [[Γ]], x : [[A]]
Definition 2 (Weaning). Assuming a self-algebraic protomonad, we define the weaning translation from CC ω to CC ω + Σ by induction over the term syntax in Figure 3.

As explain in Section II, the translation is essentially trans-parent on the functional fragment. Only types are heavily modified. Intuitively, this corresponds to a universe-aware version of the Eilenberg-Moore construction, where all types carry a weak T-algebra structure which does not satisfy any equation.

Luckily, on all closed types, the weak algebra structure will definitionally evaluate to a proper algebra. We now turn to the proof that this translation gives rise to a syntactical model of CC ω . First, it naturally preserves definitional equalities.

Proposition 1 (Computational soundness). If M ≡ N then [M ] ≡ [N ].
Proof. Congruence rules are transparent owing to the fact the translation is defined by induction on syntax, and the β-rule is transparent as well because any β-redex is translated into another β-redex.

Remark 3. If the target theory furthermore validates the ηrule for Π-types, it it obvious that the source theory also does, for λ-abstractions and applications are transparently translated. This is another free consequence of the fact that the translation stems from a call-by-push-value decomposition.

Proposition 2 (Type unfolding). The following definitional equations hold:

• [[ i ]] ≡ T i • [[Πx : A. B]] ≡ Πx : [[A]]. [[B]]
Proof. By application of the reduction rule on El.

Proposition 3 (Typing soundness). If Γ M : A then it follows that [[Γ]] [M ] : [[A]].
Proof. The variable, λ-abstraction and application cases are direct, thanks to the application of the conversion rule on Πtypes from Proposition 2. Conversion is handled transparently thanks to Proposition 1. The only non-trivial cases are the rules introducing types. All type formers are translated into a term of the form ret (A, µ A ), so by Proposition 2 it is sufficient to check that (A, µ A ) : ≡ ΣA : . T A → A.

• For the rule i : i+1 , we must therefore show that (T i , µ i ) : i+1 . We have indeed T i : i+1 because i : i+1 . It is also obvious that µ i : T (T i ) → T i because this corresponds to the free algebra structure.

• Likewise, for the rule Πx : A. B : max(i,j) , we have Πx :

[[A]]. [[B]] : max(i,j
) by applying the induction hypothesis. It remains to show that µ ΠAB has the expected type, which is a matter of straightforward symbol pushing.

Thus, we get a model of CC ω by a translation into CIC.

Theorem 1. Weaning provides a syntactic model of CC ω .

IV. WEANING TRANSLATION OF BTT

This section extends the weaning translation to inductive types, and in particular to dependent elimination. Because the weaning translation adds effects to the theory, full dependent elimination is not valid anymore. This is a typical issue arising in presence of effects as it has been oberved independently by Barthe and Uustalu [START_REF] Barthe | Cps translating inductive and coinductive types[END_REF] and by Herbelin [START_REF] Herbelin | On the degeneracy of sigma-types in presence of computational classical logic[END_REF]; and which reappeared in our recent work on forcing.

In this section, we present a restriction of dependent elimination that allows for the definition of the weaning translation on inductive types. We call the type theory resulting from this restriction Baclofen Type Theory (BTT), because it alleviates addiction to dependence. It is the source calculus of both the weaning and the forcing translation 2 and, as such, is a good candidate to model effectful type theories.

A. Blaclofen Type Theory

On the negative fragment, BTT coincides with CC ω . The only difference between BTT and CIC appears on the eliminators of inductive types. While CIC has one notion of patternmatching that implements both non-dependent and dependent elimination, BTT has two. The first one is non-dependent and is unconditionally valid, while the second one is dependent and restricted through the use of storage operators.

We recall here the definition of storage operators [START_REF] Krivine | Classical logic, storage operators and second-order lambda-calculus[END_REF], a notion arising from classical realizability. Intuitively, a storage operator on type A is a term θ A : A → (A → R) → R allowing to enforce a call-by-value semantics on terms of type A in an otherwise call-by-name language by means of continuation-passing style. When A is an inductive datatype, there is a canonical storage operator on A only defined in terms of non-dependent elimination.

In order to keep the presentation simple, we will not be using the usual fixpoint-based presentation of CIC as a source calculus, but will rather define eliminators. Also, we will only present BTT on three prototypical inductive types: booleans, lists and propositional equality. Those inductive types have been chosen because they feature all the ingredients appearing in generic inductive types: multiple constructors, parameters, indices and recursion. They are defined-in a Coqlike syntax-as:

Inductive bool : := | true : bool | false : bool Inductive list (A : ) : := | nil : list A | cons : A → list A → list A Inductive eq (A : ) (x : A) : A → := refl : eq A x x
In BTT, the non-dependent eliminators are unrestricted and are the same as in CIC. They are given by the following terms, with the usual ι-rules: bool_case : ΠP. P → P → bool → P list_case : ΠA P. P → (A → list A → P → P ) → list A → P eq_case : ΠA (x : A) (P : A → ). P x → eq A x y → P y

Storage operators can be defined using only those nondependent elimination. The storage operators for our prototypical inductive examples are defined in Figure 4. In BTT,

θ bool : bool → (bool → ) → := λb k. bool_case ((bool → ) → ) (λk. k true) (λk. k false) b k θ list : ΠA. list A → (list A → ) → := λA l k. list_case A ((list A → ) → ) (λk. k nil) (λx _ r k. r (λl. k (cons A x l))) l k θ eq
: ΠA (x y : A). eq A x y → (Πy : A. eq A x y → ) → := λA x y e k. eq_case A x (λy : A. storage operators are used to constraint the evaluation of the predicate on which dependent elimination is performed. On our prototypical inductive examples, dependent eliminators are given by the terms (together with the usual ι-rules):

(eq A x y → ) → ) (λk. k x (refl A x)) y e
bool_rect : ΠP : bool → . P true → P false → Πb : bool. θ bool b P list_rect : ΠA (P : list A → ). P (nil A) → (Πx l. θ list A l P → θ list A (cons A x l) P ) → Πl : list A. θ list A l P eq_rect : ΠA (x : A) (P : Πy : A. eq A x y → ). P x (refl A x) → Πy e. θ eq A x y e P Note that the usual dependent elimination of CIC can be decomposed into this restricted elimination followed by an ηrule for inductive types which can be written: θ A a P = P for all inductive types A. While this η-rule is actually propositionally valid in CIC, it is not preserved in presence of effects.

We highlight that BTT is the source theory of both the call-by-name forcing translation and, as we will see, the weaning translation, which itself encompasses a large class of effects. Furthermore, it also prevents the paradox arising from careless mixing of CIC with computational classical logic of Herbelin [START_REF] Herbelin | On the degeneracy of sigma-types in presence of computational classical logic[END_REF]. Thence we believe that we have enough phenomenological evidence to claim that BTT is the proper way to mix dependent type theory with computational effects.

Conjecture 1. BTT models effectful type theories.

Obviously, this claim is somewhat ill-defined. As of today, it is not even clear what an effectful type theory is. As for the Church-Turing thesis, it should rather be taken as a definition of what an effectful type theory is.

B. Dependent Monads

In order to interpret inductive types of BTT, we need to define a stronger notion of proto-monad, which is also equipped with structure allowing to depend on free algebras. Definition 3. We say that a self-algebraic proto-monad T has dependent elimination whenever the following equation holds

hbnd A B (ret A M ) F ≡ F M
and furthermore there exists a universe-polymorphic dependent binding operation

• dbnd : Π(A : i ) (R : [[ k ]]) (B : A → [[R]] → T j ). Π(x : T A) (r : [[R]]). (Πx : A. [[B x r]]) → (El (hbnd A [R → j ] x B r))
.π 1 subject to the following definitional equation:

dbnd A R B (ret A M ) N F ≡ F M N .
For readability purposes, we use the translation macros [•] and [[•]] slightly abusively above, as they do not apply to the target theory, but they can be expanded nevertheless in the same syntactical way, e.g., [[B x r]] := (El (B x r)).π 1 . Remark 4. Note that the equation on dbnd is only well-typed whenever the equation on hbnd holds definitionally.

Altough the type of dbnd is intimidating, this is just an artefact due to dependent typing. As witnessed by its reduction rule, this is simply a variant of the hbnd term where B is allowed to depend on the x : A argument, and they share the same computational content. It has additional arguments R and r for technical reasons arising from commutative cuts that are needed to define dependent recursors.

In what follows, we will assume that T is a self-algebraic proto-monad with dependent elimination.

C. Inductive Types without Dependent Elimination

In the next sections, we assume that our target theory implements at least CIC [START_REF] Paulin-Mohring | Introduction to the Calculus of Inductive Constructions[END_REF], in particular fixpoints with a guard condition.

The translation of inductive datatypes is rather straightforward from a programming point of view. The language we are working in is call-by-name, so that all non-recursive datatypes are interpreted as a free algebra of T. For recursive datatypes, recursive calls are turned into the free algebra itself, which raises an issue in CIC. Namely, datatype constructors must satisfy the positivity criterion. In order for our translation to go through, we assume that T is syntactically strictly positive in its argument, which will be the case for all examples from Section V. We define formally the inductive type translation below.

[P 1 ]]) . . . (p n : [[P n ]]) and indices (x 1 : [[X 1 ]]) . . . (x m : [[X m ]]), with constructors c • 1 . . . c • k defined as follows. Assume a constructor c of I of type Π(p 1 : P 1 ) . . . (p n : P n ) (a 1 : A 1 ) . . . (a l : A l ). I p 1 . . . p n M 1 . . . M m with argument types A, then c • has type Π(p 1 : [[P 1 ]]) . . . (p n : [[P n ]]) (a 1 : [[A 1 ]]) . . . (a l : [[A l ]]). I • p 1 . . . p n [M 1 ] . . . [M m ]
where we pose locally

[[I]] := λp 1 . . . p n x 1 . . . x m . T (I • p 1 . . . p n x 1 . . . x m ).
Inductive bool [I] := λ( p :

• : := | true • : bool • | false • : bool • Inductive list • (A : T ) : := | nil • : list • A | cons • : [[A]] → T (list • A) → list • A Inductive eq • (A : T ) (x : [[A]]) : [[A]] → := | refl • : eq • A x x
[[ P ]]) ( x : [[ X]]). ret ((T (I • p x)), µ I ) [c] := λ( p : [[ P ]]) ( a : [[ A]]). ret (I • p [ M ]) (c • p a) µ I := λι : T (T (I • p x)). bnd _ _ ι (λi. i)
Although the syntax is heavyweight, the translation is essentially pointwise, except that it inserts a few free algebra structures here and there. Proposition 4. The translation of inductive types preserves typing.

Proof. Direct check. In particular, we have the conversion

[[I p x]] ≡ T (I • [ p] [ x]).
We can now define non-dependent eliminators on inductive datatypes by only relying on hbnd. Just as T needed to satisfy a positivity condition, the existence of those eliminators depend on hbnd being syntactically positive as We will assume that this is the case in what follows, and once again the examples of Section V will show that this is not a strong restriction in practice.

Rather than giving the generic translation, which would not be very readable, we provide the eliminators on the three prototypical examples. Definition 6. We extend the translation using these constants for the corresponding eliminators from the source theory, i.e.,

[bool_case] := bool_case • and similarly for list and eq; the eliminators are defined as: Proof. Simple application of the conversion rule of hbnd.

bool_case • : [[ΠP. P → P → bool → P ]] := λP p t p f b. hbnd _ _ b (λb. match b with true • ⇒ p t | false • ⇒ p f ) list_case • : [[ΠA P. P → (A → list A → P → P ) → list A → P ]] := λA P p 0 p S l. hbnd _ _ l (fix Φ l ⇒ match l with | nil • _ ⇒ p 0 | cons • _ x l ⇒ p S x l (hbnd _ _ l Φ))
As one can observe, the eliminator for list • uses CIC fixpoints in a non-trivial way, and this is precisely from where the requirement that hbnd is syntactically positive stems.

The empty type is an inductive type, so it is straightforward to give a criterion characterizing the consistency of the translated theory.

Proposition 6 (Consistency). The source theory is consistent iff T ⊥ is empty in the target theory.

Proof. Indeed, [[⊥]] ≡ T ⊥ • ∼ = T ⊥ where ∼ = denotes type isomorphism.
In Section VII, we will see how to use parametricity techniques to overcome this condition by allowing the inconsistent world to cohabitate with a consistent one even when T ⊥ is inhabited.

D. Dependent Case Analysis

Finally, we show how dependent elimination restricted to storage operators is definable in the source theory, thus leading to a model of BTT. Proposition 7. There exists dependent eliminators for bool, list and eq with the restricted types of Section IV-A which satisfy in addition the usual ι-rules.

Proof. The dependent eliminators are implemented essentially like their non-dependent counterpart, except that hbnd is turned into dbnd. The additional R and r arguments of dbnd are instantiated respectively with the type of P and P from the corresponding recursor. Validity of ι-rules is in turn ensured by the conversion rule on dbnd.

Contrarily to the forcing translation, it is sometimes possible to cheat and implement full dependent elimination. Proposition 8. If there is a term : ΠA : . T A and one can definitionally discriminate terms of the form ret A M , then full dependent elimination is implementable.

Proof. The eliminator is defined as the standard CIC eliminator on terms which are applied constructors (i.e., of the form ret _ (c M ) for some constructor c) and otherwise uses to produce a dummy proof.

Obviously, by Proposition 6 the existence of entails that the theory resulting from weaning is logically inconsistent, but it may still have some use for programming or proof extraction. Practical examples will be given in the next section.

However, it is shown in Section VII that, using parametricity techniques, it is possible to get effects with full dependent elimination without the cost of inconsistency.

V. INSTANCES OF THE WEANING TRANSLATION

In this section, we describe a few representative instances of our model. The diversity of the effects obtained shows that this construction is quite generic. For the various T we give, the monad structure is well-known, so that we will only describe the data specific to this article. The corresponding code can be found at https://github.com/CoqHott/coq-effects.

Our target theory is computational, thus it is possible to give equational theories for the effectful operators we introduce thereafter. Nonetheless, this section is more about the proof of concept, and hence we will refrain from describing them.

A. Writer on a free monoid

We assume a fixed universe-polymorphic type Ω • and we also assume that target theory features a universepolymorphic type of lists.

Definition 7. Let T A := A × list Ω • together with El := λA. A.π 1 hbnd := λA B x f. match x with | (x, nil _) ⇒ f x | (x, l) ⇒ (El B).π 2 ((f x), l) dbnd := λA B R x r f. match x with | (x, nil _) ⇒ f x r | (x, l) ⇒ (El B).π 2 ((f x r), l)
Note that we are somehow cheating to implement this instance, because we take advantage of the fact we can definitionally observe whether the monoid element is the unit to satisfy the conversion rule on hbnd. Definition 8. We extend the source theory with Ω : , tell : Ω → unit and listen : unit → Ω as follows where app is list concatenation.

[Ω] := ret

((list Ω • ), µ Ω ) µ Ω := λω. app (ω.π 1 ) (ω.π 2 ) [tell] := λω : list Ω • . ((), ω) [listen] := λi : unit • × list Ω • . i.π 2
It is possible more generally to observe the current written value on universes and inductive datatypes, but we will not describe the relevant combinators here. This translation preserves consistency, but its logical implications are unclear.

B. Dynamic Exceptions

As for the writer, we assume a fixed universe-polymorphic type E • , and in addition that the target theory has a sum type.

Definition 9. The exception monad is defined as T

A := A + E • together with El := λA. match A with in l X ⇒ X | in r e ⇒ e hbnd := λA B x f. match x with | in l x ⇒ f x | in r e ⇒ (El B).π 2 (in r e) dbnd := λA B R x r f. match x with | in l x ⇒ f x r | in r e ⇒ ( e).π 2 (in r e)
where : E • → is arbitrary, e.g., := λ_. (1, λ_. ()).

The fact that is arbitrary reflects the choice we have to make about types returning exceptions, because it is not specified at all. It fixes the meaning of Γ M : fail N , where fail is defined below. Definition 10. We extend the source theory with E : and fail : E → ΠA : . A defined as follows.

[E] := ret

(E • , µ E ) µ E := λe. match e with in l e ⇒ e | in r e ⇒ e [fail] := λe A. (El A).π 2 (in r e)
The reader should be aware that the exceptions arising from this translation are call-by-name, so that they do not behave like their usual call-by-value counterpart. In particular, we have [fail M (Πx : A. B)] ≡ [λx : A. fail M B]. This means that exceptions cannot be caught on Π-types. We can catch them on universes and inductive types though, because they are translated as free algebras. For instance, there exists in the source theory a term catch bool of type ΠP : bool → . P true → P false → (Πe : E. P (fail e bool)) → Πb : bool. P b with the expected reduction rules on all three cases. Because of Proposition 6, the resulting theory is inconsistent as soon as E • is inhabited. Yet, the translation can be used for logical purposes. The careful reader may indeed have realized that the weaning translation on exceptions is no more than Friedman's trick [START_REF] Friedman | Classically and intuitionistically provably recursive functions[END_REF] on steroids. Thus we can use it for program extraction on the Σ 0 1 classical fragment. Proposition 9. We have

[[¬¬A]] ∼ = ([[A]] → E • ) → E • .
Proposition 10. If I is a first-order type, then there is a term eval

I : [[I]] → I + E • .
By Proposition 8, full dependent elimination is interpreted, so that by putting all these properties together we recover this interesting extraction result by taking E • := I. Theorem 2. If I is a first-order type and there is a proof of ¬¬I in CIC, then there is a proof of I in CIC.

C. Non-determinism

We sketch a model of BTT with non-determinism here.

Definition 11. The non-empty list monad is defined as T

A := A × list A together with El (X, (nil _)) := X El (X, [X 1 ; . . . ; X n ]) := (X.π 1 × X 1 .π 1 . . . × X n .π 1 , µ)
where µ is canonically defined from the algebra structure on the X i . Likewise, it is possible to define hbnd and dbnd similarly to the usual bnd combinator.

Note that just as in the case of exceptions, El could be defined in many other ways, because effectful types are not specified. For instance, it is also valid to take El A := A.π 1 .

In any case, this monad allows to write a merging operator that features non-determinism. Definition 12. We extend the source theory with an operator amb : ΠA : . A → A → A defined as follows.

[amb] := λA x y. (El A).π 2 (x, (cons _ y (nil _))) Despite its type, amb is neither the first nor the second projection. On closed types, it is possible to give an equational theory to amb (e.g., it is associative). Once again, the model preserves consistency, but its added logical expressivity is not known.

D. Non-termination

It turns out that the delay monad is indeed a self-algebraic monad, so that it is possible to build a type theory with built-in non-termination and arbitrary fixpoints. The definition of El above is very naive, and implies that all impure types evaluate to the singleton type. This is degenerated, and it is possible to do better by using a heterogeneous delay monad instead. Following Capretta's work [START_REF] Capretta | General recursion via coinductive types[END_REF], we can define a fixpoint operator through the weaning translation. Note that any type can be turned into a free algebra by using the box type from the next section so that one can define a generic fixpoint. The resulting theory is inconsistent by virtue of Proposition 6, but this does not prevent its use as a dependently-typed programming language with decidable typing and general recursion.

(([[

A]] → T C) → [[A]] → T C) → [[A]] → T C.

VI. LINEARITY AS A GUARD CONDITION

The restriction on dependent elimination of BTT can be extended on a more semantical ground by using linearity, a notion that has been first described by Munch-Maccagnoni [START_REF] Munch-Maccagnoni | Models of a Non-Associative Composition[END_REF] and rephrased recently in the context of CBPV by Levy [START_REF] Levy | Contextual isomorphisms[END_REF]. Linearity3 is a property of call-by-name functions which intuitively represents the fact that a function is semantically call-by-value. We recall Levy's definition below in a typetheoretical setting, which first relies on the existence of a unary sum type. Naturally, in CIC, box A is isomorphic to A, thanks to dependent elimination. This is not the case anymore in BTT, precisely because full dependent elimination is not available. Instead, the fact that this type is an inductive type provides a way to locally perform computation in a call-by-value fashion. This is made clear through the weaning translation, as witnessed by the following lemma.

Proposition 12. [[box A]] ∼ = T [[A]] holds in CIC.

We can now define the proper notion of linearity in the weaning translation.

Definition 15 (Linearity). We say that a term M : [[A → B]]

is linear whenever there is a proof of

Πx : [[box A]]. [λf. f (box_case A A (λx : A. x) x)] M = [λf. box_case A B f x] M
in the target theory.

This definition uses equality of the target theory, so that we can define a predicate linear : ΠA B. [[A → B]] → in the target theory. Although it is defined here in terms of the weaning translation, it can be generalized to any syntactic translation of type theory in a straightforward way. In particular, in a pure language, the notion is trivial. For instance, in CIC, by taking [•] to be the identity, all functions are linear because box A is isomorphic to A. This is not true in presence of non-trivial effects. Let for instance be ϕ : unit → unit := λ_. (), and assume that the language allows non-termination. Thus there is a nonconverging term loop : box unit. Then the linearity equation is not valid for M := ϕ and x := loop, because the left-hand side converges, while the right-hand side diverges.

At first sight, it seems that linearity is a property that makes sense in the context of semantics of programming languages, but which has little to do with logic. Surprisingly, it turns out to be a valuable criterion to assess that a predicate is insensitive to storing.

Proposition 13 (Storing invariance). Let us assume that T satisfies the monad laws propositionally, that hbnd is extensionally defined as in Remark 1, and furthemore that the target theory satisfies functional extensionality. Let I be a non-recursive inductive type.

If a predicate P :

[[I → ]] is linear, then Πi : [[I]]. [θ I ] i P = P i.
Proof. As θ I is defined as a single pattern-matching, it unfolds to an application of hbnd to a case analysis. But [ ] is a free algebra, and by the canonicity of hbnd, this can be rewritten to an application of bnd to a case analysis. Then, using the isomorphism of Proposition 12, the equation of linearity is transported on T I • . We conclude by a rewriting of monadic laws and dependent elimination on I • .

The above lemma uses type theory in a non-trivial way, because to be formulated it requires that predicates are actual terms from the theory, and thus relies on the existence of universes. We suspect this is the reason why the few attempts at an effectful dependent type theory have been strongly restricted up to now.

Confortingly, this property is not limited to the weaning translation as it holds also for call-by-name forcing under the same assumption. This is quite expected, as the definitions of BTT and linearity do not dependent on the underlying effect. Furthermore, it is also obviously true for the identity translation of CIC.

Remark 5. Storing invariance does not hold for recursive inductive types. This is due to the fact that linearity on f only captures the fact that f commutes with one pattern-matching, whereas it would need to commute with arbitrary fixpoints to extend to recursive types.

Notwithstanding the above limitation, storing invariance allows to provide a semantical restriction on non-recursive dependent elimination in BTT rather than having to go through storage operators. Namely, it is semantically correct to provide a dependent pattern-matching in BTT on, say, bool of the following form. The key difference with standard CIC pattern-matching is the side condition of linearity on C.

Obviously, it is not palatable to have to write proofs of linearity, and one would like to have the system decide automatically whether a predicate is linear. Just as the fixpoint guard condition of CIC is a syntactic underapproximation of a semantical notion of positivity, it is possible to provide a syntactic approximation for linearity. A few syntactical closure properties are described in Levy's paper for instance. Most notably, storage operators would syntactically turn an arbitrary predicate into a linear one, because they start with a linear pattern-matching on the variable being eliminated. It means that there would not be any need to hardwire them in BTT.

Apart from the fact it is not clear how to extend linearity to recursive inductive types, this would result in a patternmatching-based theory closer to CIC, and easier to work with in a proof assistant. We will refrain from exploring this further in this paper and leave it for future work.

VII. PARAMETRIC WEANING TRANSLATION FOR CIC

This section is dedicated to the description of a technique based on parametricity to recover a syntactical model of full CIC out of the weaning translation, while allowing at the same time this pure world to cohabitate with effectful programs.

Parametricity is a well-known proof technique introduced by Reynolds [START_REF] Reynolds | Types, abstraction and parametric polymorphism[END_REF] that is used for a vast range of purposes, e.g., the automatic derivation of properties of programs according to their type described by Wadler [START_REF] Wadler | Theorems for free![END_REF]. A few years ago, Bernardy and others showed that parametricity could be written as a syntactical translation over type theory [START_REF] Bernardy | Realizability and Parametricity in Pure Type Systems[END_REF]. In a nutshell, their translation associates to a term M : A a term [M ] ε : [A] ε M where [A] ε translates to the parametricity predicate over A. The elegance of the translation stems from the fact that just as for CC ω , it does not make any formal distinction between terms and types and that the parametricity predicate [A] ε and parametricity theorem [M ] ε are actually derived by the same syntactical induction.

Contrarily to their presentation, we will not use parametricity to state properties on terms from an underlying theory but rather use it to carve out non-parametric terms from the underlying theory, resulting in a syntactical model of CIC instead of BTT.

Moreover, the translation we give is a variant of parametricity that we will call internal, by opposition to Bernardy's presentation which we will call external. The difference lays in the handling of free variables. In Bernardy's original presentation, terms from the source theory cannot depend on the fact that variables are assumed parametric. This is due to terms being translated in two sequents, where the first translation is essentially identity for unary parametricity, and the second one explicits parametricity of the first term.

By contrast, we will call our translation internal because it only produces one sequent, and furthermore translated terms rely essentially on the fact that parametricity assumptions on variables are available. In particular, as a syntactical enhancement, variables from the context will be translated as Σ-types rather than as a pair of variables.

A. Parametricity Restriction

The intuitive idea of this model is simple. As the weaning translation fails to interpret dependent elimination because there are non-canonical inductive terms in the model, let us simply claim that we will only be interested in inductive terms which are well-behaved, i.e., parametric. Obviously this needs to scale to the whole translation, so that it needs to be a little involved. We first explicit the translation on the negative Definition 16 (Parametric Weaning). Assuming T is a selfalgebraic proto-monad, we define parametric weaning over the syntax of CC ω in Figure 6.

[ i ] := ret i+1 ((T i ), µ i ) [x] := x.π 1 [λx : A. M ] := λx : [[A]] ! . [M ] [M N ] := [M ] [N ] ! [Πx : A. B] := ret ((Πx : [[A]] ! . [[B]]), µ ΠAB ) [ i ] ε := λA : T i . (El A).π 1 → i [x] ε := x.π 2 [λx : A. M ] ε := λx : [[A]] ! . [M ] ε [M N ] ε := [M ] ε [N ] ! [Πx : A. B] ε := λf : Πx : [[A]] ! . [[B]]. Πx : [[A]] ! . [B] ε (f x) µ i := λA : T (T i ). bnd (T i ) i A (λX : T i . X) µ ΠAB := λ( f : T (Πx : [[A]] ! . [[B]])) (x : [[A]] ! ). hbnd (Πx : [[A]] ! . [[B]]) [B] f (λf : Πx : [[A]] ! . [[B]]. f x) [[A]] := (El [A]).π 1 [M ] ! := ([M ], [M ] ε ) [[A]]
On the [•] fragment, the translation is essentially the same as the non-parametric weaning, except that variables and function arguments are packed with their parametricity proof. This is typical of the thunking appearing in call-by-name translations, and is reminiscent of the forcing translation [START_REF] Jaber | The definitional side of the forcing[END_REF], which is why we use the same

[•] ! notation.
In what follows, for the sake of simplicity we will assume that the target theory validates definitional surjective pairing. It is technically not necessary, at a cost of a slightly less understandable translation, where [•]

! is primitive and [•] and [•] ε are derived from it. Proposition 14 (Substitution lemma). We have both

[M {x := N }] ≡ [M ]{x := [N ] ! } and [M {x := N }] ε ≡ [M ] ε {x := [N ] ! }.
Proof. By induction over M .

Corollary 1 (Computational soundness). If M ≡ N then

[M ] ≡ [N ] and [M ] ε ≡ [N ] ε .
Proposition 15 (Typing soundness). If Γ M : A then we have

[[Γ]] ! [M ] : [[A]] and [[Γ]] ! [M ] ε : [A] ε [M ]. As a consequence, [[Γ]] ! [M ] ! : [[A]] ! .
Proof. By induction over the typing derivation.

Remark 6. To extend the theory with some constant M : A, it is thus sufficient to provide a pair of terms [M ] :

[[A]] and [M ] ε : [A] ε [M ]
as all other definitions are derived.

As before, the previous lemmas state no more that the [•]

! translation gives rise to a syntactic model of CC ω . It is slightly more convoluted that the bare weaning translation, as it adds a predicate to types and ensure that all terms respect the predicate of their type.

Proposition 16. We have the following unfoldings.

•

[[ ]] ! ≡ ΣA : T . (El A).π 1 → • [[Πx : A. B]] ! ≡ Σf : Πx : [[A]] ! . [[B]]. Πx : [[A]] ! . [B] ε (f x) ∼ = Πx : [[A]] ! . [[B]] !
We now show how it actually extends to inductive types. We will focus on the simple example of booleans, because it already exhibits the trick, although the same technique scales to arbitrary inductive types.

Definition 17 (Boolean parametricity). We define the following inductive predicate over T bool • .

Inductive bool • ε : T bool • → := | true • ε : bool • ε (ret bool • true • ) | false • ε : bool • ε (ret bool • false • ) Definition 18.
We extend the parametric weaning translation as follows.

[bool] := ret

((T bool • ), µ bool ) [true] := ret bool • true • [false] := ret bool • false • [bool] ε := bool • ε [true] ε := true • ε [false] ε := false • ε µ bool := λ b : T (T bool • ). bnd _ _ b (λb. b)
It is not hard to check that typing soundness still holds with this extension. Proposition 17. The above translation preserves typing.

Luckily, through the translation, boxed inhabitants have more structure than just pertaining to the free algebra over bool • .

Proposition 18. We have [[bool]]

! ≡ Σb : T bool It is essential for the eliminator to have access to the parametricity proof of its argument. This is where the internal nature of our variant stands out. With external parametricity, the eliminator would only have access to a non-standard boolean b : T bool • and would not be able to do anything relevant with it without the storage operator restriction. Even though the parametricity proof of the eliminator would access it, it would already be too late.

This technique can be generalized effortlessly to any inductive type in a way similar to Bernardy's parametricity, leading to the following observation.

Theorem 3. The parametric weaning translation is a syntactic model of CIC. In addition, it preserves consistency.

Interestingly enough, the parametric part of the translation is quite independent from the effectful translation. It can actually be extended to other settings, such as call-by-name forcing. Moreover, it highlights a blind spot of parametricity: types.

The parametricity restriction enforces functions to be respectful, and inductive datatypes to be indeed inductively generated. Yet, the only constraint we put on types is that they wear a parametricity predicate on their elements. But the weaning translation did generate new types as soon as T is not the identity, as [[ ]] ≡ T . Thus there are new anomalous types modelled by the parametric weaning translation, so that it is larger than the original theory. Clearly, it is impossible in pure CIC to add a constraint on the shape of a type precisely because of parametricity. But here, we have more structure on types so that we could restrict them. For instance, we could enforce elements of T to be of the form ret A for some A to bar non-standard types and recover the original theory.

The usual parametricity translation simply does not put any constraint. We believe that this explains the mechanism hidden under the monotonicity condition of forcing, which preserves inductive types while allowing to expand universes as presheaves. Somehow, universes in type theory are underspecified.

B. BTT as a Modality

It is obvious that giving a model of CIC alone is not very exciting. The interesting bits come from the additional expressive power bestowed by this translation. In this section, we show that BTT can be injected into the parametric weaning translation thanks to the effect modality.

Definition 19 (Effect modality). We define the effect modality E : i → i in the source theory as follows.

[E] := λA :

[[ ]] ! . A.π 1 [E] ε := λ(A : [[ ]] ! ) (x : (El (A.π 1 )).π 1 ). unit
The proper way to understand the effect modality is that given a type A with the parametricity predicate A ε , it builds the same underlying type A but with the full predicate, so that any term of type

[[A]] is parametric for [E A] ε .
Example 1. For instance, we have

[[E bool]] ! ≡ Σb : T bool • . unit ∼ = T bool • .
Proposition 20. The effect modality has a few properties in the source theory that should be highlighted.

• It is definitionally idempotent, i.e., E (E A) ≡ E A.

• There exists a return operator η

E : ΠA. A → E A. • It is not functorial, as E (Πx : A. B) ∼ = Πx : A. E B.
In particular, E is not a self-algebraic monad. Nonetheless, it is possible to give an internal translation of BTT into the parametric weaning of CIC. 6 except that we replace uniformly all translations by their E-indexed variant, where

Definition 20 (Effectful translation). The effectful translation

[•] E is defined as [•] in Figure
[M ] ! E := ([M ] E , ()) [[A]] E := (El [A] E ).π 1 [[A]] ! E := Σx : [[A]] E . unit Note in particular that [•] ε does not appear in [•] E . Proposition 21. Assuming Γ M : A in BTT, then we have [[Γ]] ! E [M ] ! E : [[A]] ! E .
Proof. Essentially the same proof as in Proposition 3.

Definition 21 (Effectful quotation). For every term M from BTT, we extend the source theory with a term M whose translation is defined below.

[ M ] := [M ] E

[ M ] ε := () Definition 22. We define in the source theory the effectful element E : E i → i as follows.

[E ] := λA : [[E ]] ! . A.π 1

[E ] ε := λ(A : [[E ]] ! ) (x : (El (A.π 1 )).π 1 ). unit

Proposition 22. We have E (E A) ≡ E A.

The following theorem is then an immediate consequence of Proposition 21 obtained by unfolding the definitions. This shows that we can readily embed BTT into CIC as a kind of DSL. Obviously, the • operator satisfies a few rules that are not described here, but which follow from the definitions, e.g., Πx : A. B ≡ η E (Πx : E A . E B ). The major difference of this translation w.r.t. the direct inclusion of BTT into CIC as one would have obtained by Proposition 3 comes from the fact universes are translated transparently. Hence, we can reason about the effectful fragment as if it was part of the theory, and this can be used to mix effects with proofs in a consistent way.

VIII. RELATED WORK

The introduction of dependent types in mainstream programming languages is currently gaining traction, as witnessed by the growing community of Idris [START_REF] Brady | Idris, a general-purpose dependently typed programming language: Design and implementation[END_REF] for instance. This naturally raises the question of computational effects in a dependent setting. However, the literature on the topic is rather terse. To the best of our knowledge, apart from the work on forcing in type theory [START_REF] Jaber | The definitional side of the forcing[END_REF], there are only two very recent and overlapping lines of work that intersect with BTT, namely the independent description of a dependent CBPV by Ahman et al. [START_REF] Ahman | Dependent types and fibred computational effects[END_REF] and Vákár [START_REF] Vákár | A framework for dependent types and effects[END_REF].

Quite interestingly, the initial intuition given by Ahman et al. for their system is very similar to the fundamental idea of weaning that types must carry an algebra structure and that dependency is distributed over it. But, in the content of the paper, their presentation turns into a more ad-hoc system where dependency-introducing structures are duplicated between terms and computations, resulting in a syntax cancelling all the fundamental computational dualities of CBPV.

As for the systems described by Vákár, their limitations are clear through the prism of BTT. Vákár describes two systems, dCBPV -where dependence is restricted to values, and dCBPV + , which is an extension of the former. dCBPV -is compatible with BTT on the CBN fragment, but its limitation lies in its lack of expressivity. There are no universes and no dependent elimination on anything else than syntactical values, so that it is not even clear how to introduce a non-trivial conversion rule. dCBPV + is therefore proposed to extend dCBPV -with the so-called dependent Kleisli extension rule. It turns out that this rule essentially postulates in the logic that all predicates are linear, which is, as we have seen in Section VI, false in presence of effects. As a consequence, all models of dCBPV + are either pure or logically unsound.

All the examples he gives of the implementation of the Kleisli extension rule are actually an instance of Proposition 8.

On another line of work, the notion of (accessible) modalities in Homotopy Type Theory [START_REF] Univalent | Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF] is quite close to selfalgebraic monads. Indeed, the purpose of modalities is to reflect a subuniverse of the theory with extra logical properties, in the same way as self-algebraic monads are used to define new models of BTT with additional effects. However, such modalities are by definition idempotent, whereas self-algebraic monads, coming from functional programming, rarely are.

IX. CONCLUSION AND FUTURE WORK

In this paper, we have defined the first monadic translation of type theory, called weaning translation, that allows for a large range of effects in dependent type theory-such as exceptions, non-termination, non-determinism or writing operation. The weaning translation typically applies to a version of CIC with a restricted version of dependent elimination, called Baclofen Type Theory, which constitutes a good candidate for the definition of an effectful type theory. Finally, we have shown how to recover a translation of full CIC using parametricity techniques. The translation is available as a Coq plugin and all the examples have been formalized with it.

Our work opens a new line of research on the logical expressivity induced by the use of traditional computation monads in type theory. It also offers the possibility to program with and reason on effects in the same framework, without relying on additional axioms in the theory.

Fig. 1 .

 1 Fig. 1. Call-by-push-value (types only)

Fig. 2 .

 2 Fig. 2. Typing and computation rules of CCω and Σ-types

Fig. 3 .

 3 Fig. 3. Weaning Translation

Fig. 4 .

 4 Fig. 4. Storage operators for booleans, lists and equality.

Definition 4 .

 4 Assume an inductive type I with parameters (p 1 : P 1 ) . . . (p n : P n ) and indices (x 1 : X 1 ) . . . (x m : X m ), with constructors c 1 . . . c k . We define a new inductive I • with parameters (p 1 : [

Fig. 5 .

 5 Fig. 5. Examples of inductive types translation

Figure 5

 5 Figure 5 explicits the above translation on the prototypical examples, in a Coq-like syntax. Observe in particular how the the recursive argument of the cons • constructor is boxed under a monadic type, revealing a typical call-by-name behaviour. Definition 5 (Translation of inductive types). Given an inductive type I and its constructors c as before, we extend the [•] translation as follows: [I] := λ( p : [[ P ]]) ( x : [[ X]]). ret ((T (I • p x)), µ I )

Proposition 5 .

 5 eq_case • : [[ΠA (x : A) (P : A → ). P x → eq A x y → P y]] := λA x P p ê. hbnd _ _ ê (λe. match e with refl • _ _ ⇒ p) The eliminators satisfy the usual ι-rules definitionally.

Definition 13 .

 13 The delay monad is defined as CoInductive T (A : ) : := | here : A → T A | next : T A → T A with for instance El (here _ X) := X and (unit, λ_. ()) otherwise. It has dependent elimination in a direct way.

Proposition 11 .

 11 Assuming B is a free algebra, there exists a termY B : [[ΠA. ((A → B) → A → B) → A → B]] that satisfies a fixpoint equation (up to bisimilarity).Proof. The free algebra condition on B means indeed that we have [[B]] := T C for some C, so that we must build Y B : ΠA.

  It is then defined by coinduction in the same way as in Capretta's paper.

Definition 14 .

 14 We define the inductive type box as Inductive box (A : ) : := Box : A → box A together with its non-dependent eliminator box_case : Π(A : ) (P : ). (A → P ) → box A → P which both automatically admit a weaning translation.

Γ

  match M with true ⇒ N1 | false ⇒ N2 : C{z := M }

!Fig. 6 .

 6 Fig. 6. Parametric Weaning Translation

Theorem 4 .

 4 Assuming Γ M : A in BTT, then we have [[E Γ ]] ! [ M ] ! : [[E A ]]! in the target theory.

  Proposition 19. There exists a fully dependent eliminator over bool in the parametric weaning translation, that furthermore preserves usual ι-rules.Proof. It is implemented by dependent pattern-matching over the second component of b : [[bool]]! . Reduction rules are valid owing to the fact they apply to constructors.

• . bool • ε b.

This proposition amounts to say that [[bool]]

! is isomorphic to bool simply thanks to the second component. This allows to write full dependent elimination over booleans.

We call this structure a proto-monad because it does not have to satisfy the monadic laws. Only one rule for the interaction between El and ret is needed, but at the same time it is crucial that it holds definitionally rather than just Negative fragment:A, B, M, N ::= i | x | M N | λx : A. M | Πx : A. B Γ i < j Γ i : j Γ A : i Γ, x : A B : j Γ Πx : A. B : max(i,j) Γ, x : A M : B Γ Πx : A. B : i Γ λx : A. M : Πx : A. B Γ M : Πx : A. B Γ N : A Γ M N : B{x := N } Γ M : B Γ A : i Γ, x : A M : B • Γ A : i Γ, x : A Γ A : i Γ, x : A x : A Γ M : B Γ A : i Γ A ≡ B Γ M : A (λx : A. M ) N ≡ M {x := N } (congruencerules ommitted) Σ-types: A, B, M, N ::= . . . | Σx : A. B | M.π 1 | M.π 2 | (M, N ) Γ A : i Γ, x : A B : j Γ Σx : A. B : max(i,j) Γ M : Σx : A. B Γ M.π 1 : A Γ M : Σx : A. B Γ M.π 2 : B{x := M.π 1 }

In[START_REF] Jaber | The definitional side of the forcing[END_REF], this restricted version of CIC was referred to as CIC -.

This notion of linearity is mostly unrelated to linearity in the sense of linear use of variables.


V Martini-Laithier

I Graur

S Bernardini

K Aguir

P Perrier

M Bendahan

Ammonia detection by a novel Pyrex microsystem based on thermal creep phenomenon

Keywords: Gas sensor, Gas pumping, Thermal creep, Microfluidic, Gas detection, WO 3

Our research work aims to develop a microfluidic system for gas analysis by using an original principle of integrated pumping. This microsystem can detect ammonia and the gas flow parameters inside the channel can be also controlled. The proposed microdevice consists in a microchannel including an integrated gas sensor with a heater. The trioxide tungsten (WO 3 ) is implemented as a sensitive layer. The integrated heater is used for two reasons: to optimize the sensor response and to induce the gas pumping inside the microchannel by thermal creep phenomenon, therefore, no external pumping system is required. The study of the pumping effect generation has been realized by thermal and microfluidic simulations. Thermal simulations have been performed to estimate the thermal gradient along the microchannel. In addition, the microfluidic modelling allows us to determine the mass flow rate for different thermal gradient profiles, obtained from the thermal simulations. Finally, a complete Pyrex microsystem has been realized to detect ammonia. The existence of the thermal pumping has been demonstrated experimentally.

A c c e p t e d M a n u s c r i p t

Introduction

All control laboratories manipulate constantly standard gas analyzers for the atmospheric pollutant controls. These devices are precise to determine the concentration and the nature of gas samples, but they are bulky, slow, and very expensive. The development of microfluidic systems could be the solution to avoid the standard analyzer disadvantages.

Several devices are developed to improve the sensitivity of the microsystems for gas analysis. The authors of Ref. [START_REF] Ohira | Micro gas analyzers for environmental and medical applications[END_REF] have developed new chromatographic microcolumns which lead to enhance the selectivity including VOC (volatile organic compounds) separation [START_REF] Ohira | Micro gas analyzers for environmental and medical applications[END_REF][START_REF] Sanchez | Use of a chromatographic column to improve the selectivity of the SnO 2 gas sensors: first approach towards a miniaturised device and selective with hydrogen fluoride vapours[END_REF][START_REF] Chang | Microfabricated Gas Chromatograph for Sub-ppb Determinations of TCE in Vapor Intrusion Investigations[END_REF].

Many researches on preconcentrator realisation allow improving the sensitivity by increasing the gas concentration before detection [START_REF] Ohira | Micro gas analyzers for environmental and medical applications[END_REF][START_REF] Erickson | Integrated microfluidic devices[END_REF][START_REF] Zhu | Integrated microfluidic gas sensor for detection of volatile organic compounds in water[END_REF]. Other researchers [START_REF] Zhu | Integrated microfluidic gas sensor for detection of volatile organic compounds in water[END_REF][START_REF] Gupta | Thermal transpiration in zeolites: A mechanismfor motionless gas pumps[END_REF][START_REF] Sugimoto | Numerical analysis on gas separator with thermal transpiration in micro channel, 28th International symposium on rarefied gas dynamics[END_REF] use microreactors to modify the gas nature in order to increase the detection sensitivity. But all these systems need sampling or external pump to analyze gas.

Our work targets to develop and to test new microdevice for gas detection with an integrated pumping system to sample a pollutant before detection. This microsystem is composed of a metal oxide base sensor, which includes a platinum heater. This heater is used for two reasons: to optimize the sensor response and to create a temperature gradient along the channel surface and therefore the thermal creep phenomenon. The presence of the temperature gradient along the channel's surface launches the macroscopic gas movement inside microchannel, from the cold side to the hot side.

In this paper, we present the thermal creep phenomenon. This phenomenon has some technological applications such as a new pump without any moving parts [START_REF] Gupta | Thermal transpiration in zeolites: A mechanismfor motionless gas pumps[END_REF], or gas separation process in gas chromatography [START_REF] Sugimoto | Numerical analysis on gas separator with thermal transpiration in micro channel, 28th International symposium on rarefied gas dynamics[END_REF]. Then, we justify the choice of the microsystem's dimensions and the values of applied temperature gradient along their surfaces A c c e p t e d M a n u s c r i p t for gas transport inside the microsystem. Next, through the thermal simulation the best channel material is determined in order to assure the large enough temperature gradient along the channel's walls. The microfluidic simulation allows us to determine the mass flow rates through the microsystem. Finally, the details of the fabrication steps are given and the experimental results for ammonia detection are discussed.

Microfluidic model study

Thermal creep phenomenon

Reynolds has discovered the thermal creep phenomenon in 1878 showing the macroscopic movement of rarefied gas from the lower to the higher temperature zone. Indeed, when two reservoirs connected by a microchannel are maintained continuously at different temperatures and at the same pressure, a gas flows from the cold to the hot reservoirs (Fig. 1).

The gas rarefaction is characterized usually by the ratio between a molecular mean free path and a characteristic scale of the problem; this ratio is called the Knudsen number. A characteristic dimension of a microdevice is of the order of several micrometers, therefore a gas inside is rarefied (the Knudsen number is larger than 0.01) even at atmospheric pressure.

In presence of a thermal gradient inside the microdevices a gas displacement can be obtained in the gradient direction.

Recently, the mass flow rate through a micro-tube generated by the temperature gradient was measured in [START_REF] Rojas | Thermal transpiration flow: A circular cross-section micro-tube submitted to a temperature gradient[END_REF][START_REF] Rojas | Time-dependent experimental analysis of a thermal transpiration rarefied gas flow[END_REF] for several gases and various temperature differences. It was shown that the mass flow rate induced by the temperature gradient is proportional to the temperature gradient intensity. This mass flow rate depends also on the gas rarefaction, characterized by the Knudsen number, and so proportional to the characteristic scale of the problem. Therefore In the present study we use the thermal creep phenomenon to obtain the gas flow through a microchannel, where a sensor is integrated. Two open ends of the microchannel are maintained naturally at the atmospheric pressure and a heater integrated in one of channel's surfaces provides the temperature gradient. This heater is also used to increase the detection response performance.

Model

Our microsystem is composed of two parts: a support (A) and a cover (B) (Fig. 2). The support contains the platinum electrodes for electrical measurements, the metal oxide sensitive film (WO 3 ) and the platinum resistive heater device. The microchannel has a rectangular cross section with height h and width l, the microchannel length is equal to L, represented in Fig. 2. The cover contains the etched microchannel in which the sensor is inserted.

The sensor required to be heated for its detection performance. This sensor heating is also used to create the high thermal gradient inside the microchannel, which is essential for the gas pumping. In order to obtain this thermal creep phenomenon the control of two parameters are required: the gas flow regime inside the channel (slip regime) and the temperature difference between the two channels ends [START_REF] Sone | Flows Induced by Thermal Fields[END_REF].

The slip regime corresponds to a Knudsen number between 10 -3 and 10 -1 . As it was explained in Section 2.1, in order to obtain the slip flow regime [START_REF] Sone | Flows Induced by Thermal Fields[END_REF] inside the channel under atmospheric conditions, the channel height (characteristic scale of our case) was chosen to be equal to 10 µm. The microchannel width was chosen to be equal to 500 µm to insert the A c c e p t e d M a n u s c r i p t microsensors inside the microchannel extremity. The length choice was linked both to the value of the temperature gradient wished and to the flow rate estimation. All these dimensions are chosen to obtain the best microsystem performances [START_REF] Martini | Fabrication and characterization of gas detection microfluidic system[END_REF].

Thermal gradient simulations

Comsol Multiphysics software is used to determine the temperature gradient profile along the microchannel (Fig. 3) and it allows us to choose the best (in view of thermal properties) material for the substrate and for the cover.

We tested two materials with different thermal properties (silicon and Pyrex, compatibles with microtechnology processes). A geometric model (Fig. 3) was drawn from the previously chosen dimensions. The substrate was defined as a simple block of 700 µm thickness including the platinum heater. The electrical and thermal parameters, used to create this new sensor model, are more reliable and improve our previous model [START_REF] Martini | Fabrication and characterization of gas detection microfluidic system[END_REF] where these parameters have not been adjusted by the simulations.

In our present sensor model the heater is a thin film of platinum. The setting its thermal properties is one of the most important steps. The principal properties, which characterize the platinum layer, are the electric conductivity (σ) and the thermal conductivity (λ). These parameters are related through the Wiederman-Franz equation (eq. 1):

T T e k 3 π σ λ 2 B 2           ( 1
)
where λ is the thermal conductivity, σ is the electric conductivity, k B is the Boltzmann constant, e is the elementary electron charge and  is the Lorentz number (eq. 2) :

8 2 2 B 2 2.45.10 3e k π     W*Ω*K -2 (2)
A c c e p t e d M a n u s c r i p t

The platinum layer was deposited by magnetron sputtering to obtain a thickness of 80 nm. Previous tests allowed us to determine experimentally the electric conductivity value of the platinum layer depending of the temperature [START_REF] Martini | Microfluidic gas sensor with integrated pumping system[END_REF]. The corresponding thermal conductivity values are calculated from these experimental results on the electric conductivity using eq.

(1). These values, used for the platinum heater model, are presented in Table 1 for various temperatures [START_REF] Taine | Transferts Thermiques : Introduction aux transferts d'énergie[END_REF]. The difference between the bulk thermal conductivity values and our results is explained by the fact that we work with thin Pt films. The experimental data on the thermal conductivity of the platinum layer are used to simulate the thermal behaviours of the microsystem.

We studied the effect of the material properties for the sensor's support and then for the cover of the microsystem model using Comsol Multiphysics software. The first material studied was the silicon, which presents an important thermal conductivity (82.3 W*m*K -1 at 473K). The second one was the Pyrex, which has a low thermal conductivity (1.4 W*m*K -1 at 473K). In the first case these simulation results highlight that the high silicon thermal conductivity induced too important thermal losses to obtain a sufficient temperature gradient for all tested temperatures. In the second case, an important temperature gradient along the Pyrex substrate can be obtained. Thus, Pyrex was chosen to the microsensor support [START_REF] Martini | Fabrication and characterization of gas detection microfluidic system[END_REF].

We also used Comsol Multiphysics software to determine the cover material: Pyrex or silicon. The complete geometry including the microchannel was drawn and added to the Pyrex support. The cover was defined first in silicon then in Pyrex. An important thermal gradient was obtained for each case considering the temperature value along the x-axis direction, see Figure 4. But for Pyrex cover, the temperature decreases regularly along the microchannel and the thermal gradient is higher than for the silicon cover, as it is shown in Figure 4.

A c c e p t e d M a n u s c r i p t

To understand the influences of both the temperature difference at the channel ends and of the temperature gradient along the channel on the gas mass flow rate the microfluidic simulations were performed. By fitting these temperature gradient profiles we found the best equation describing the temperature variations along the microchannel surface (axe x in Fig. 3). Then, this information about the temperature distribution was used as the boundary conditions in the microfluidic model.

Gas mass flow rate simulations

In order to estimate the mass flow rate through the microchannel, the numerical simulations were carried out using the compressible Navier-Stokes equations subjected the velocity slip and temperature jump boundary conditions [START_REF] Méolans | Continuum analytical modelling of thermal creep[END_REF]. The microchannel is defined as a large rectangular channel connecting two reservoirs. The Knudsen number is fixed in the range [10 -3 ; 10 -2 ] and the same pressure is set in the both reservoirs to simulate the open into atmospheric pressure ends of the microdevice. The temperatures in both reservoirs and the temperature distribution along the channel's surfaces are taken from the thermal simulations described in the Section 2.3. Two materials, with different thermal properties, are studied for the channel cover: silicon and Pyrex. The temperature distributions obtained from the simulations with both materials are used as the boundary conditions for the microfluidic part for three heater temperature, see Table 2.

For the lower temperature of the heater, the mass flow rates through the channels with silicon and Pyrex covers have the similar values. However, when the heater temperature increases up to 623K the mass flow rate through the channel with Pyrex cover is 1.5 larger than for silicon cover. In the case of the silicon cover, the sudden temperature decrease and the small thermal gradient along the channel is not sufficient in order to provide the suitable gas circulation inside the microdevice. However, the Pyrex cover provides more important temperature gradient along the channel's cover (see Fig. 4) and therefore allows creating the more important gas flow rate through the channel, which leads to the better quality of the pollution analysis.

Experiments and discussion

Microsystem realization

The microsystem was realized with two Pyrex wafers. The wafers 1 and 2 are used to realize the support and the cover, respectively. The microsensors were deposed on the support. They are composed of platinum electrodes, platinum heater and a tungsten trioxide sensitive layer. The platinum layer thickness is 100 nm and was deposited by magnetron sputtering. Then WO 3 layer has a thickness of 80 nm and was deposited by reactive magnetron sputtering with an argon/oxygen mixture with ratio equal 1 [START_REF] Barsan | Conduction model of metal oxide gas sensors[END_REF]. A very thin titanium layer had been deposed before the platinum to enhance the adhesion on the Pyrex. To finish, the layers were annealed at 673K during 1h30.

The microchannel is etched into the cover. The Pyrex is a very strong material thus the ultrasound etching were used to cross through the wafer of 1000 µm and to define the windows allowing access to microsensors pads. Then, the microchannel has been etched by HF etching for a depth of 10 µm.

A c c e p t e d M a n u s c r i p t

To obtain the complete microsystem both wafers were bonded together by a technique similar to the thermo-compression performed at ambient temperature. A gold layer was deposed by rf sputtering magnetron on the cover wafer with a chrome adhesion layer. A gold layer was also deposed on the support wafer using a silicon shadow mask, which protects the microsensors. Then, these layers were quickly associated under primary vacuum. A high force of 4000 N was applied to bond the wafers. The bonding was improved with a hydraulic compression.

Microsensor ammonia response (microsensor alone without cover)

Gas detection was studied first with the gas sensor alone. The sensor performances were tested under diluted gases in dry air, at atmospheric pressure. The normalized sensor response was defined as S = R 0 /R g , where R 0 and R g are the sensor resistances in dry air and in target gas, respectively. We studied NH 3 detection at 25 ppm corresponding to the maximum level authorized at the working place and an ammonia sensor must clearly detect partial pressures significantly below this point.

In order to check the effect of operating temperature on the sensor response the microsensor alone has been tested through ammonia gas with several working temperatures from 423K to 523K.

To determine the best work temperature, we measured the detection response and the recovery time with a fixed ammonia concentration. The recovery time is defined as the time to reached 80% of the origin resistance R 0 after ammonia turn off. Figure 5 illustrates the response to 25 ppm of ammonia versus operating temperature. It shows a systematic response increase with increasing operating temperature up to 443K, but reverse tendency is observed above 443K. We can also notice that the recovery time decreases when temperature increases.

A c c e p t e d M a n u s c r i p t

The response and recovery time are directly related to the adsorption and desorption activation energies, respectively.

This behaviour can be explained by considering the temperature dependence coverage surface of chemisorbed species [START_REF] Guérin | Thermal modelling of a WO 3 ozone sensor response[END_REF]. At low temperature, desorption phenomenon is weak and a total coverage of the sites can be obtained easily making no reversible detection possible.

Conversely, at high temperature the efficiency of desorption mechanism increases and the system will be less sensitive. The coverage decreases with increasing temperature because the desorption rate rises faster than the adsorption rate. Thus, there is necessarily an optimum temperature at which the sensor reaches a maximum of sensitivity [START_REF] Guérin | Modeling of the conduction in a WO 3 thin film as ozone sensor[END_REF][START_REF] Bendahan | WO 3 sensor response according to operating temperature: Experiment and modeling[END_REF]. The best response is measured at 443K, but at this temperature the gas desorption kinetic is slow, which implies a high recovery time. At 523K the recovery time is short enough, but the response is lower.

We evaluated that the most adapted temperature would be between 463K and 493K, then, we have finally chosen 473K as the best compromise between a good sensitivity and fast recovery time.

Global microsystem gas characterization (microsensor with cover)

Remind that the aim of our project is to create a thermal pumping into the microchannel and detect the gas in the generated flow.

The microsystem with Pyrex cover is placed into the detection chamber. The sensor is heated at a temperature of 473K to optimize the ammonia detection, as it was explained in the end of previous Section. The gas is led by a nozzle into the microchannel input, i.e. in the opposite extremity of the heated gas sensor. The gas flow rate in the nozzle is 200 ml/min.

The microsystem is exposed at ammonia concentration of 50 ppm to forecast a visible response.

A c c e p t e d M a n u s c r i p t

The results show an electrical response corresponding to the ammonia detection.

Moreover, this response is reversible after dry air exposure. The microsensor tests have demonstrated that the recovery time is the longest one at this temperature. The gas flow rate and the microchannel volume are also low and amplify this phenomenon. These results demonstrate the possibility to detect ammonia with our microsystem; nevertheless, the electrical response is not sufficient to prove the gas pumping existence from the microchannel entrance to the microsensor. To prove it we have realised a specific detection cell (Fig. 6).

The cell's volume is around 8 ml. The gas goes into the gas cell and leaves the cell by a natural evacuation. The pressure equilibrium is conserved. The microsystem is placed between the cell and the outside. The microchannel output is placed outdoor of the cell and can exchange directly with the detection chamber. The microchannel input is indoor the cell.

The microsensor is biased and heated and then a pollutant flow is led into the cell. The sensitive layer resistance is measured to detect the ammonia through the microchannel gas flow. In this way, if the microsensor responds to the target gas, we can conclude that a gas flow exists in the microsystem and that the thermal pumping is efficient. We fixed the sensor's temperature at 473K. The ammonia was injected continuously in the cell. After several seconds an important resistance variation was measured. The total response time corresponds to the sensor response time (2 sec max) and the characteristic time of gas flowing microchannel. At this heater temperature the gas mass flow rate through the channel was evaluated at 2.47 10 -12 kg*s -1 (Tab. 2) and therefore the gas characteristic time is of the order of 10 sec. An example of the electric signal is presented in Figure 7.

These detections proved the existence of the thermal pumping into the microsystem. -The design of a novel microfluidic system for gas analyses with an integrated pumping system is presented -Thermal and mass flow rate device are simulated using Comsol Multiphysics software -We characterized the microfluidic device in ammonia environment -An experimental demonstration of thermal creep phenomenon was done

A

  c c e p t e d M a n u s c r i p t it is possible to adjust and to control the mass flow rate by modifying the thermal gradient intensity along the channel's surface or the geometrical characteristics of the microdevice.

A c c e p t e d M a n u s c r i p t

  The temperature distributions of the channel's cover in the case of Pyrex and silicon, obtained from thermal modelling and used in the fluidic simulation are shown on Fig.4.

A c c e p t e d M a n u s c r i p t 4 .

 4 ConclusionThe thermal and microfluidic studies let us estimate the best materials for our gas sensor microsystem. Using Comsol Multiphysics software, simulations were done to evaluate thermal gradient along the microchannel. The thermal simulations confirmed the temperature gradient existence required for the thermal creep phenomenon. Microfluidic simulations indicated that Pyrex is the best material for both the substrate and the channel cover. The cover was realized with Pyrex and experimental tests were performed to validate the model. Then, gas detection experiments with the WO 3 microsensor demonstrated a high response for the ammonia detection between 423K and 523K with an optimal work temperature around 473K. The ammonia detection possibility has been confirmed by the microsystem tests at 473K. This measurement is due to the thermal pumping existence demonstrated by the use of the fluidic cell. The future works goal to test interfering gas detections and to improve the selectivity of the microsystem using a channel network.

A c c e p t e d M a n u s c r i p t

Figure 1 :

 1 Figures :

Figure 2 :

 2 Figure 2: Microsystem description: support with microsensor (A) and cover with the

Figure 3 :

 3 Figure 3: Our microsystem simulated by Comsol Multiphysics software: Axe X and direction

Figure 4 :

 4 Figure 4: Profiles of the thermal gradient simulated along the microchannel from the heater to

Figure 5 :

 5 Figure 5: Response and recovery time temperature dependence (25 ppm of NH 3 ).

Figure 6 :

 6 Figure 6: Detection cell.

Figure 7 :

 7 Figure 7: Pyrex microsystem response for 50 ppm ammonia detection at 473 K in the detection cell.

A c c e p t e d M a n u s c r i p t

  Figure 2

  Figure 4

  Figure 5

Figure 6 A

 6 Figure 6

  Figure 7

Table 1 :

 1 his PhD degree from the University of Aix-Marseille in 1996 with a thesis on shape memory alloys thin films. He is specialized in thin films preparation and characterization for applications in microsystems. Since 1997, he is interested in gas microsensors based on inorganic and organic materials. was researcher from 1990 to 1994 and Senior Researcher from 1994 to 2002. Then, she moved to France as Associate Professor at Polytechnique University School of Marseille at Provence University, and appointed professor in 2009 at Mediterranean University in Marseille, France. Her current research interests include rarefied gas dynamics, High-speed flows, Micro flows, numerical simulations, No-equilibrium and non-stationary flow regimes. Standard and measured thermal and electrical conductivities of platinum, at different temperatures.

	Khalifa Aguir is a Professor at Aix Marseille University (France). He was awarded his
	Doctorat d'Etat ès Sciences degree from Paul Sabatier University, Toulouse (France) in 1987.
	He is currently the head of Microsensors Group at the Institute of Materials Microelectronic
	Nanosciences of Provence (IM2NP-CNRS) at Aix-Marseille University, Marseille (France).
	His principal research interests are now directed towards metal -oxide (WO 3 , SrTiO 3 , CuO)
	and organic thin films for gas sensors, flexible gas sensors, microsystems, selectivity
	enhancement strategies including surface modification of sensors, signal treatment, adsorption
	-desorption noise spectroscopy, modeling of sensor responses analysis, low noise amplifier
	Design and sensor electronics.
	Irina Graur is a Professor at Aix Marseille University (France). She studied in the
	Department of Computational Mathematics & Cybernetics from Moscow State University,
	where she received her master degree in 1984 and PhD in 1989. From 1989 to 1990, she was
	junior researcher at Keldysh Institute of Applied Mathematics USSR Academy of Sciences.
	She joined the Institute for Mathematical Modeling Russian Academy of Sciences where she

Pierre Perrier received his PhD from Provence University, France, in 1998. He became research engineer in the French National Center of Scientific Research (CNRS) at Provence University, France in 1999. His current research interests include instrumentation, signal treatment, bio-mecanic, and gas microfluidic experimentations (low and high speed flows).

Tables :

Table 2 :

 2 Mass flow rate calculated for both covers.

Table 1 T

 1

	(K)	Thermal conductivity (W.m.K -1 ) Platinum bulk	Electrical conductivity (S.m) Thin platinum film (experimental values)	Thermal conductivity (W.m.K -1 ) Thin platinum film (experimental values)
	293	71.5	3.84 10 6	27.5
	373	71.5	3.29 10 6	30.0
	473	72	2.78 10 6	32.2
	573	72.8	2.41 10 6	33.9
	673	73.8	2.26 10 6	35.1

Table 2 Heater temperature (K) 473 573 623 Mass flow rate with a silicon cover (10 -12 kg.s -1 )

 2

		2.42	3.90	4.69
	Mass flow rate with a	2.47	5.53	7.12
	Pyrex cover (10 -12 kg.s -1 )

Acknowledgements

The authors gratefully acknowledge for financial support in their research by the funding from "Region PACA -BDE n°648" and "Seres Environnement" company and from European Community's Seventh Framework Program (ITN -FP7/2007-2013) under grant agreement n° 215504. We would like to thank the MIMENTO Technological Center of Besançon and particularly Fabien AMIOT who was actively involved at the technological realization and A. Combes (Im2np) for technical support.