Pierre-Marie Pédrot

Nicolas Tabareau

Failure is Not an Option An Exceptional Type Theory

Keywords: | true : bool | false : bool Ind bool, = | true, bool, | false, bool, | bool∅ : E → bool ]]) : := | nil, list, A | cons, [[A]] → list

We define the exceptional translation, a syntactic translation of the Calculus of Inductive Constructions (CIC) into itself, that covers full dependent elimination. The new resulting type theory features callby-name exceptions with decidable type-checking and canonicity, but at the price of inconsistency. Then, noticing parametricity amounts to Kreisel's realizability in this setting, we provide an additional layer on top of the exceptional translation in order to tame exceptions and ensure that all exceptions used locally are caught, leading to the parametric exceptional translation which fully preserves consistency. This way, we can consistently extend the logical expressivity of CIC with independence of premises, Markov's rule, and the negation of function extensionality while retaining η-expansion. As a byproduct, we also show that Markov's principle is not provable in CIC. Both translations have been implemented in a Coq plugin, which we use to formalize the examples.

Introduction

Monadic translations constitute a canonical way to add effects to pure functional languages [START_REF] Moggi | Notions of computation and monads[END_REF]. Until recently, this technique was not available for type theories such as CIC because of complex interactions with dependency. In a recent paper [START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF], we have presented a generic way to extend the monadic translation to dependent types, using the weaning translation, as soon as the monad under consideration satisfies a crucial property: being self-algebraic. Indeed, in the same way that the universe of types i is itself a type (of a higher universe) in type theory, the type of algebras of a monad T ΣA : i . T A → A needs to be itself an algebra of the monad to allow a correct translation of the universe. However, in general, the weaning translation does not interpret all of CIC because dependent elimination needs to be restricted to linear predicates, that is, those that are intuitively call-by-value [START_REF] Munch-Maccagnoni | Models of a Non-Associative Composition[END_REF]. In this paper, we study the particular case of the error monad, and show that its weaning translation can be simplified and tweaked so that full dependent elimination is valid.

This exceptional translation gives rise to a novel extension of CIC with new computational behaviours, namely call-by-name exceptions. 3 That is, the type theory induced by the exceptional translation features new operations to raise and catch exceptions. This new logical expressivity comes at a cost, as the resulting theory is not consistent anymore, although still being computationally relevant. This means that it is possible to prove a contradiction, but, thanks to a weak form of canonicity, only because of an unhandled exception. Furthemore, the translation allows us to reason directly in CIC on terms of the exceptional theory, letting us prove e.g. that, assuming some properties on its input, an exceptional function actually never raises an exception. We thus have a sound logical framework to prove safety properties about impure dependently-typed programs.

We then push this technique further by noticing that parametricity provides a systematic way to describe that a term is not allowed to produce uncaught exceptions, bridging the gap between Kreisel's modified realizability [START_REF] Kreisel | Interpretation of analysis by means of constructive functionals of finite types[END_REF] and parametricity [START_REF] Bernardy | Realizability and parametricity in pure type systems[END_REF] inside type theory. This parametric exceptional translation ensures that all exceptions used locally are caught, thus ensuring consistency of the resulting theory. We exploit this computational extension of CIC to show various logical results over CIC.

Contributions.

-We describe the exceptional translation, the first monadic translation for the error monad for CIC, including strong elimation of inductive types, resulting in a sound logical framework to reason about impure dependently-typed programs. -We use parametricity to extend the exceptional translation, getting a consistent variant dubbed the parametric exceptional translation. -We show that Markov's rule is admissible in CIC and more generally, that classical logic is conservative over the type-theoretic version of Π 0 2 formulae. -We show that definitional η-expansion together with the negation of function extensionality is admissible in CIC. -We show that there exists a syntactical model of CIC that validates the independence of premises (which is known to be generally not valid in intuitionistic logic [START_REF] Avigad | Gödel's functional ("Dialectica") interpretation[END_REF]) and use it to recover the recent result of Coquand and Mannaa [START_REF] Coquand | The independence of Markov's principle in type theory[END_REF], i.e., that Markov's principle is not provable in CIC. -We provide a Coq plugin4 that implements both translations and with which we have formalized all the examples.

Plan of the paper. In Section 2, we describe the exceptional translation and the resulting new computational principles arising from it. In Section 3, we present the parametric variant of the exceptional translation. Section 4 is devoted to the various logical results resulting from the parametric exceptional translations. In Section 5, we discuss possible extensions of the translation with negative records and an impredicative universe. Section 6 describes the Coq plugin and illustrates its use on a concrete example. We discuss related work in Section 7 and conclude in Section 8.

The Exceptional Translation

We define in this section the exceptional translation as a syntactic translation between type theories. We call the target theory T , upon which we will make various assumptions depending on the objects we want to translate.

Adding Exceptions to CC ω

In this section, we describe the exceptional translation over a purely negative theory, i.e., featuring only universes and dependent functions, called CC ω , which is presented in Figure 1. This theory is a predicative version of the Calculus of Constructions [START_REF] Coquand | The Calculus of Constructions[END_REF], with an infinite hierarchy of universes i instead of one impredicative sort. We assume from now on that T contains at least CC ω itself. The exceptional translation is a simplification of the weaning translation [START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF] applied to the error monad. Owing to the fact that it is specifically tailored for exceptions, this allows to give a more compact presentation of it.

Let E : 0 be a fixed type of exceptions in T . The weaning translation for the error monad amounts to interpret types as algebras, i.e., as inhabitants of the dependent sum ΣA : i . (A + E) → A. In this paper, we take advantage of the fact that the algebra morphism restricted to A is always the identity. Thus every type just comes with a way to interpret failure on this type, i.e. types are intuitively interpreted as a pair of an A : i with a default (raise) function A ∅ : E → A. In practice, it is slightly more complicated as the universe of types itself is a type, so its interpretation must comes with a default function. We overcome this issue by assuming a term type i , representing types that can raise exceptions. This type comes with two constructors: TypeVal i which allows to construct a type i from a type and a default function on this type ; and another constructor TypeErr i that represents the default function at the level of type i . Furthermore, type i is equipped with an eliminator type_elim i and thus can be thought of as an inductive definition. For simplicity, we axiomatize it instead of requiring inductive types in the target of the translation. Definition 1. We assume that T features the data below, where i, j indices stand for universe polymorphism.

-

Ω i : E → i -ω i : Πe : E. Ω i e -type i : j , where i < j -TypeVal i : ΠA : i . (E → A) → type i -TypeErr i : E → type i -type_elim i,j : ΠP : type i → j . (Π(A : i ) (A ∅ : E → A). P (TypeVal i A A ∅ )) → (Πe : E. P (TypeErr i e))
→ ΠT : type i . P T subject to the following definitional equations:

type_elim i,j P p v p ∅ (TypeVal i A A ∅ ) ≡ p v A A ∅ type_elim i,j P p v p ∅ (TypeErr i e) ≡ p ∅ e
The Ω term describes what it means for a type to fail, i.e. it ascribes a meaning to sequents of the form Γ M : fail e. In practice, it is irrelevant and can be chosen to be degenerate, e.g. Ω := λ_ : E. unit.

In what follows, we often leave the universe indices implicit although they can be retrieved at the cost of more explicit annotations.

Before defining the exceptional translation we need to derive a term El5 that recovers the underlying type from an inhabitant of type and Err that lifts the default function to this underlying type.

Definition 2. From the data of Definition 1, we derive the following terms.

El i : type i → i := λA : type i . type_elim (λT : type i . i ) (λ(A 0 : i ) (A ∅ : E → A 0 ). A 0 ) Ω A Err i : ΠA : type i . E → El i A := λ(A : type i ) (e : E). type_elim El i (λ(A 0 : i ) (A ∅ : E → A 0 ). A ∅ e) ω A [ i] := TypeVal type i TypeErr i [x] := x [λx : A. M ] := λx : [[A]]. [M ] [M N ] := [M ] [N ] [Πx : A. B] := TypeVal (Πx : [[A]]. [[B]]) (λ(e : E) (x : [[A]]). [B] ∅ e) [A] ∅ := Err [A] [[A]] := El [A] [[•]] := • [[Γ, x : A]] := [[Γ]], x : [[A]] Fig. 2. Exceptional Translation
The exceptional translation is defined in Figure 2. As usual for syntactic translations [START_REF] Boulier | The next 700 syntactical models of type theory[END_REF], the term translation is given by [•] and the type translation, written [[•]], is derived from it using the function El. There is an additional macro [•] ∅ , defined using Err i , which corresponds to the way to inhabit a given type from an exception.

Note that we will often slightly abuse the translation and use the [•] and [[•]] notation as macros acting on the target theory. This is merely for readability purposes, and the corresponding uses are easily expanded to the actual term.

The following lemma makes explicit how [[•]] and [•] ∅ behave on universes and on the dependent function space.

Lemma 1 (Unfoldings). The following definitional equations hold:

-

[[ i ]] ≡ type i -[[Πx : A. B]] ≡ Πx : [[A]]. [[B]] -[ i ] ∅ e ≡ TypeErr i e -[Πx : A. B] ∅ e ≡ λx : [[A]]. [B] ∅ e
Proof. By unfolding and straightforward reductions.

The soundness of the translation follows from the following properties, which are fundamental but straightforward to prove.

Theorem 1 (Soundness). The following properties hold.

-[M {x := N }] ≡ [M ]{x := [N ]} (substitution lemma). -If M ≡ N then [M ] ≡ [N ] (conversion lemma). -If Γ M : A then [[Γ]] [M ] : [[A]] (typing soundness). -If Γ A : then [[Γ]] [A] ∅ : E → [[A]] (exception soundness).
Proof. The first property is by routine induction on M , the second is direct by induction on the conversion derivation. The third is by induction on the typing derivation, the most important rule being i : j , which holds because [ i ] ≡ TypeVal type i TypeErr i has type type j which is convertible to [[ j ]] by Lemma 1. The last property is a direct application of typing soundness and unfolding of Lemma 1 for universes.

We call T E the theory arising from this interpretation, which is formally defined in a way similar to standard categorical constructions over dependent type theory. Terms and contexts of T E are simply terms and contexts of T . A context Γ is valid is T E whenever its translation [[Γ]] is valid in T . Two terms M and N are convertible in T E whenever their translations [M ] and

[N ] are convertible in T . Finally, Γ T E M : A whenever [[Γ]] T [M ] : [[A]].
That is, the only way to extend T E is to add a new constant c of a given type A and to provide an inhabitant c E of the translated type [[A]]. Then the translation is extended with [c] := c E . The potential computational rules satisfied by this new constant are directly given by the computational rules satisfied by its translation. In some sense, the new constant c is just syntactic sugar for c E . Using T E , Theorem 1 can be rephrased in the following way.

Theorem 2. If T interprets CC ω then so does T E , that is, the exceptional translation is a syntactic model of CC ω .

Exceptional Inductive Types

The fact that the only effect we consider is raising exceptions does not really affect the negative fragment when compared to our previous work [START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF], but it sure shines when it comes to interpreting inductive datatypes. Indeed, as explained in the introduction, the weaning translation only interprets a subset of CIC, restricting dependent elimination to linear predicates. Furthermore, it also requires a few syntactic properties of the underlying monad ensuring that positivity criteria are preserved through the translation, which can be sometimes hard to obtain.

The exceptional translation diverges from the weaning translation precisely on inductives types. It allows a more compact translation of the latter, while at the same time providing a complete interpretation of CIC, that is, including full dependent elimination.

From now on, we assume that the target theory is a predicative restriction of CIC, i.e. that we can construct in it new inductive datatypes as we do in e.g. Coq [START_REF]The Coq Development Team: The Coq proof assistant reference manual[END_REF], but without considering an impredicative universe. That is, all the inductive types we consider in this section live in . As a matter of fact, we slightly abuse the usual nomenclature and simply call CIC this predicative fragment in the remainder of the paper. We refrain from describing the generic typing rules that extend CC ω into CIC, as they are fairly standard and would take up too much space. See for instance Werner's thesis for a comprehensive presentation [START_REF] Werner | Une Théorie des Constructions Inductives[END_REF]. Type and Constructor Translation As explained before, the intuitive interpretation of a type through the exceptional translation is a pair of a type and a default function from exceptions into that type. In particular, when translating some inductive type I, we must come up with a type

[[I]] together with a default function E → [[I]].
As soon as E is inhabited, that means that we need [[I]] to be inhabited, preferably in a canonical way. The solution is simple: just as for types where we freely added the exceptional case by means of the TypeErr constructor, we freely add exceptions to every inductive type.

In practice, there is an elegant and simple way to do this. It just consists in translating constructors pointwise, while adding a new dedicated constructor standing for the exceptional case. We now turn to the formal construction. Definition 3. Let I be an inductive datatype with parameters p 1 : P 1 , . . . , p n : P n ; indices i 1 : I 1 , . . . , i m : I m ; constructors c 1 : Π(a 1,1 : A 1,1 ) . . . (a 1,l1 : A 1,l1 ). I p 1 . . .

p n V 1,1 . . . V 1,m . . . c k : Π(a k,1 : A k,1 ) . . . (a k,l k : A k,l k ). I p 1 . . . p n V k,1 . . . V k,m
We define the exceptional translation of I and its constructors in Figure 3, where I • is the inductive type defined by

-parameters p 1 : [[P 1 ]], . . . , p n : [[P n ]]; -indices i 1 : [[I 1 ]], . . . , i m : [[I m ]]; -constructors c • 1 : Π(a 1,1 : [[A 1,1 ]]) . . . (a 1,l1 : [[A 1,l1 ]]). I • p 1 . . . p n [V 1,1 ] . . . [V 1,m ] . . . c • k : Π(a k,1 : [[A k,1 ]]) . . . (a k,l k : [[A k,l k ]]). I • p 1 . . . p n [V k,1 ] . . . [V k,m ] I ∅ : Π(i 1 : [[I 1 ]]) . . . (i m : [[I m ]]). E → I • p 1 . . . p n i 1 . . . i m
where in the recursive calls in the various A, we locally set Because of the syntactic positivity criterion, the only possibility for such a situation to occur in CIC is in the so-called nested inductive definitions. However, nested inductive types are essentially a programming convenience, as most nested types can be rewritten in an isomorphic way that is not nested.

[[I M 1 . . . M n N 1 . . . N m ]] := I • [M 1 ] . . . [M n ] [N 1 ] . . . [N m ].
Lemma 2. If I is given as in Definition 3, we have for any terms M , N

[[I M 1 . . . M n N 1 . . . N m ]] ≡ I • [M 1 ] . . . [M n ] [N 1 ] . . . [N m ].
This justifies a posteriori the simplified local definition we used in the recursive calls of the translation of the constructors. Theorem 3. For any inductive type I not using nested inductive types, the translation from Definition 3 is well-typed and satisfies the positivity criterion.

Proof. Preservation of typing is a consequence of Theorem 1. The restriction on nested types, which is slightly stronger than the usual positivity criterion of CIC, is due to the fact that I ∅ is not available in the recursive calls and thus cannot be used to build a term of type type via the TypeVal constructor.

Preservation of the positivity criterion is straightforward, as the shape of every constructor c k is preserved, and furthermore by Lemma 1 the structure of every argument type is preserved by [[•]] as well. The only additional constructor I ∅ does not mention the recursive type and is thus automatically positive.

Corollary 1. Type soundness holds for the translation of inductive types and their constructors.

Pattern-Matching Translation

We now turn to the translation of the elimination of inductive terms, that is, pattern matching. Once again, its definition originates from the fact that we are working with call-by-name exceptions. It is well-known that in call-by-name, pattern matching implements a delimited form of call-by-value, by forcing its scrutinee before proceeding, at least up to the head constructor. Therefore, as soon as the matched term (re-)raises an exception, the whole pattern-matching reraises the same exception. A little care has to be taken in order to accomodate for the fact that the return type of the pattern-matching depends on the scrutinee, in particular when it is the default constructor of the inductive type.

In what follows, we use the i 1 . . . i n notation for clarity, but compact it to i for space reason-when appropriate. Proof. Immediate, as the translation preserves the structure of the patterns.

The translation is also applicable to fixpoints, but for the sake of readability we do not want to fully spell it out, although it is simply defined by congruence (commutation with the syntax). As such, it trivially preserves typing and reduction rules. Note that the Coq plugin presented in Section 6 features a complete translation of inductive types, pattern-matching and fixpoints. So the interested reader may experiment with the plugin to see how fixpoints are translated.

Therefore, by summarizing all of the previous properties, we have the following result.

Theorem 4. If T interprets CIC, then so does T E , and thus the exceptional translation is a syntactic model of CIC.

Flirting with Inconsistency

It is now time to point at the elephant in the room. The exceptional translation has a lot of nice properties, but it has one grave defect.

Theorem 5. If E is inhabited, then T E is logically inconsistent.
Proof. The empty type is translated as

Ind empty • : := empty ∅ : E → empty •
which is inhabited as soon as E is.

Note that when E is empty, the situation is hardly better, as the translation is essentially the identity. However, when T satisfies canonicity, the situation is not totally desperate as T E enjoys the following weaker canonicity lemma.

Lemma 5 (Exceptional Canonicity). Let I be an inductive type with constructors c 1 , . . . , c n and assume that T satisfies canonicity. The translation of any closed term T E M : I evaluates either to a constructor of the form c • i N 1 . . . N li or to the default constructor I ∅ e for some e : E.

Proof. Direct application of Theorem 1 and canonicity of T .

A direct consequence of Lemma 5 is that any proof of the empty type is an exception. As we will see in Section 4.1, for some types it is also possible to dynamically check whether a term of this type is a correct proof, in the sense that it does not raise an uncaught exception. This means that while T E is logically unsound, it is computationally relevant and can still be used as a dependentlytyped programming language with exceptions, a shift into a realm where we would have called the weaker canonicity Lemma 5 a progress lemma. This is not the end of the story, though. Recall that T E only exists through its embedding [•] into T . In particular, if T is consistent, this means that one can reason about terms of T E directly in T . For instance, it is possible to prove in T that assuming some properties about its input, a function in T E never raises an exception. Hence not only do we have an effectul programming language, but we also have a sound logical framework allowing to transparently prove safety properties about impure programs.

It is actually even better than that. We will show in Section 3 that safety properties can be derived automatically for pure programs, allowing to recover a consistent type theory as long as T is consistent itself.

Living in an Exceptional World

We describe here what T E feels like in direct style. The exceptional theory feature a new type E which reifies the underlying type E of exceptions in T E . It uses the fact that for E, the default function (here of type E → E) can simply be defined as the identity function. Its translation is given by

[E] : [[ ]] := TypeVal E (λe : E. e).
Then, it is possible to define in T E a function raise : ΠA : . E → A that raises the provided exception at any type as

[raise] := λ(A : type) (e : E). Err A e.
As we have already mentioned, the reader should be aware that the exceptions arising from this translation are call-by-name. This means that they do not behave like their usual call-by-value counterpart. In particular, we have in T E raise (Πx : A. B) e ≡ λx : A. raise B e which means that exceptions cannot be caught on Π-types. We can catch them on universes and inductive types though, because in those cases they are freely added through an extra constructor which one can pattern-match on. For instance, there exists in T E a term catch bool : ΠP : bool → . P true → P false → (Πe : E. P (raise bool e)) → Πb : bool. P b defined by

[catchbool] := λP pt p f pe b. match b return λb. El (P b) with | true • ⇒ pt | false • ⇒ p f | bool∅ e ⇒ pe e
end satisfying the expected reduction rules on all three cases. In Section 6, we illustrate the use of the exceptional theory using the Coq plugin to define a simple cast framework as in [START_REF] Tanter | Gradual certified programming in Coq[END_REF].

[ i] ε := λA : [[ i]]. [[A]] → i [x] ε := xε [λx : A. M ] ε := λ(x : [[A]]) (xε : [[A]] ε x). [M ] ε [M N ] ε := [M ] ε [N ] [N ] ε [Πx : A. B] ε := λ(f : Πx : [[A]]. [[B]]). Π(x : [[A]]) (xε : [[A]] ε x). [[B]] ε (f x) [[A]] ε := [A] ε [[•]] ε := • [[Γ, x : A]] ε := [[Γ]] ε , x : [[A]], xε : [[A]] ε x

Kreisel Meets Martin-Löf

It is well-known that Reynolds' parametricity [START_REF] Reynolds | Types, abstraction and parametric polymorphism[END_REF] and Kreisel's modified realizability [START_REF] Kreisel | Interpretation of analysis by means of constructive functionals of finite types[END_REF] are two instances of the broader logical relation techniques. Usually, parametricity is used to derive theorems for free, while realizability constrains programs. In a surprising turn of events, we use Bernardy's variant of parametricity on CIC [START_REF] Bernardy | Realizability and parametricity in pure type systems[END_REF] as a realizability trick to evict undesirable behaviours of T E . This leads to the parametric exceptional translation, which can be seen as the embodiement of Kreisel's realizability in type theory. In this section, we first present this translation on the negative fragment, then extend it to CIC and finally discuss its meta-theoretical properties.

Exceptional Parametricity in a Negative World

The exceptional parametricity translation for terms of CC ω is defined in Figure 5.

Intuitively, any type A in T E is turned into a validity predicate A ε : A → which encodes the fact that an inhabitant of A is not allowed to generate unhandled exceptions. For instance, a function is valid if its application to a valid term produces a valid answer. It does not say anything about the application to invalid terms though, which amounts to a garbage in, garbage out policy. The translation then states that every pure term is automatically valid. This translation is exactly standard parametricity for type theory [START_REF] Bernardy | Realizability and parametricity in pure type systems[END_REF] but parametrized by the exceptional translation. This means that any occurrence of a term of the original theory used in the parametricity translation is replaced by its exceptional translation, using [•] or [[•]] depending on whether it is used as a term or as a type. For instance, the translation of an application

[M N ] ε is given by [M ] ε [N ] [N ] ε instead of just [M ] ε N [N ] ε .
Lemma 6 (Substitution lemma). The translation satisfies the following conversion:

[M {x := N }] ε ≡ [M ] ε {x := [N ], x ε := [N ] ε }.
Theorem 6 (Soundness). The two following properties hold.

-

If M ≡ N then [M ] ε ≡ [N ] ε . -If Γ M : A then [[Γ]] ε [M ] ε : [[A]] ε [M ].
Proof. By induction on the derivation.

We can use this result to construct another syntactic model of CC ω . Contrarily to usual syntactic models where sequents are straightforwarldy translated to sequents, this model is slightly more subtle as sequents are translated to pairs of sequents instead. This is similar to the usual parametricity translation.

-T p E Γ whenever T [[Γ]] and T [[Γ]] ε . -M ≡ T p E N whenever [M ] ≡ T [N ] and [M ] ε ≡ T [N ] ε . -Γ T p E M : A whenever [[Γ]] T [M ] : [[A]] and [[Γ]] ε T [M ] ε : [[A]] ε [M ].
Once again, Theorem 6 can be rephrased in terms of preservation of theories and syntactic models. This construction preserves definitional η-expansion, as functions are mapped to (slightly more complicated) functions.

Lemma 7. If T satisfies definitional η-expansion, then so does T p E .

Proof. The first component of the translation preserves definitional η-expansion because functions are mapped to functions. It remains to show that

[λx : A. M x] ε := λ(x : [[A]]) (x ε : [[A]] ε x). [M ] ε x x ε ≡ [M ] ε
which holds by applying η-expansion twice.

It is interesting to remark that Bernardy-style unary parametricity also leads to a syntactic model T p that interprets CC ω (as well as CIC), using the same kind of glueing construction. Nonetheless, this model is somewhat degenerated from the logical point of view. Namely it is a conservative extension of the target theory. Indeed, if Γ T p M : A for some Γ, M and A from T , then there we also have Γ T M : A, because the first component of the model is the identity, and the original sequent can be retrieved by the first projection. This is definitely not the case with the T p E theory, because the first projection is not the identity. In particular, because of Theorem 5, every sequent in the first projection is inhabited, although it is not the case in T itself if it is consistent. This means that parametricity can actually bring an additional expressivity power when it applies to a theory which is not pure, as it is the case here.

Ind boolε : bool • → := | trueε : boolε true • | falseε : boolε false • Ind listε (A : type) (Aε : [[A]] → ) : list • A → := | nilε : listε A Aε (nil • A) | consε : Π(x : [[A]]) (xε : Aε x) (l : list • A) (lε : listε A Aε l). listε A Aε (cons • A x l)
Ind eq ε (A : type) (Aε :

[[A]] → ) (x : [[A]]) (xε : Aε x) : Π(y : [[A]]) (yε : Aε y). eq • A x y → := | reflε : reflε A Aε x xε x xε (refl • A x)

Exceptional Parametric Translation of CIC

We now describe the parametricity translation of the positive fragment. The intuition is that as it stands for an exception, the default constructor is always invalid, while all other constructors are valid, assuming their arguments are.

Type and Constructor Translation Definition 6. Let I be an inductive type as given in Definition 3. We define the exceptional parametricity translation I ε of I as the inductive type defined by:

parameters [[p 1 : P 1 , . . . , p n :

P n ]] ε ; -indices [[i 1 : I 1 , . . . , i m : I m ]] ε , x : I p 1 . . . p n i 1 . . . i m ; -constructors c 1ε : Π[[ a 1 : A 1 ]] ε . I ε p 1 p 1ε . . . p n p nε [V 1,1 ] [V 1,1 ] ε . . . [V 1,m ] [V 1,m ] ε (c • 1 p a 1 ) . . . c kε : Π[[ a k : A k ]] ε . I ε p 1 p 1ε . . . p n p nε [V k,1 ] [V k,1 ] ε . . . [V k,m ] [V k,m ] ε (c • k p a k
). and we extend the translation as

[I] ε := I ε [c 1 ] ε := c 1ε . . . [c k ] ε := c kε.
Example 2. We give the exceptional parametric inductive translation of our running examples in Figure 6.

Note that contrarily to the negative case, the exceptional parametricity translation on inductive types is not the same thing as the composition of Bernardy's parametricity together with the exceptional translation. Indeed, the latter would also have produced a constructor for the default case from the exceptional inductive translation, whereas our goal is precisely to rule this case out via the additional realizability-like interpretation.

It is also very different from our previous parametric weaning translation [START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF], which relies on internal parametricity to recover dependent elimination, enforcing by construction that no effectful term exists. Here, effectful terms may be used in the first component, but they are required after the fact to have no inconsistent behaviour. Intuitively, parametric weaning produces one pure sequent, while exceptional parametricity produces two, with the first one being potentially impure and the second one assuring the first one is harmless.

Pattern-matching Translation

Definition 7. Let Q be the pattern-matching defined in Definition 4. We pose [Q] ε to be the pattern-matching

match [M ] ε return λ[[ i : I]] ε (x : I [X1] . . . [Xn] i1 . . . im).
(xε :

Iε [X1] [X1] ε . . . [Xn] [Xn] ε i1 i1ε . . . im imε x) [[R]] ε [Qx] with | c1ε a1,1 a1,1ε . . . a 1,l 1 a 1,l 1 ε ⇒ [N1] ε . . . | c kε a k,1 a k,1ε . . . a k,l k a 1,l k ε ⇒ [N k ] ε end
where Q x is the following pattern-matching that is Q where the scrutinee has been turned into the index variable of the parametricity predicate.

Lemma 8. With notations and typing assumptions from Definition 4, we have

[[Γ]] ε [Q] ε : [[R{ i := Y , x := M }]] ε [Q].
The exceptional parametricity translation can be extended to handle fixpoints as well, with a few limitations. Translating generic fixpoints uniformly is indeed an open problem in standard parametricity, and our variant faces the same issue. In practice, standard recursors can be automatically translated, and fancy fixpoints may require hand-writing the parametricity proof. We do not describe the recursor translation here though, as it is essentially the same as standard parametricity. Again, the interested reader may test the Coq plugin exposed in Section 6 to see how recursors are translated.

Packing everything together allows to state the following result.

Theorem 8. If T interprets CIC, then so does T p E , and thus the exceptional parametricity translation is a syntactic model of CIC.

Meta-Theoretical Properties of T p

E

Being built as a syntactic model, T p E inherits a lot of meta-theoretical properties of T . We list a few of interest below. Theorem 9. If T is consistent, then so is T p E .

Proof. Assume T p E M 0 : empty for some M 0 . Then by definition, there exists two terms M and M ε such that T M : empty • and T M ε : empty ε M . But empty ε has no constructor, and T is inconsistent.

More generally, the same argument holds for any inductive type.

Theorem 10. If T enjoys canonicity, then so does T p E .

Proof. The exceptional parametricity translation for inductive types has the same structure as the original type, so any normal form in T p E can be mapped back to a normal form in T .

Effectively Extending CIC

The parametric exceptional translation allows to extend the logical expressivity of CIC in the following ways, which we develop in the remainder of this section.

We show in Section 4.1 that Markov's rule is admissible in CIC. We already sketched this result in our previous paper [START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF], but we come back to it in more details. More generally, we show a form of conservativity of classical logic over the type-theoretic version of Π 0 2 formulae. In Section 4.2, we exhibit a syntactic model of CIC with satisfies definitional η-expansion for functions but which negates function extensionality. As far as we know, this was not known.

Finally, in Section 4.3, we show that there exists a model of CIC which validates the independence of premises. This is a new result, that shows that CIC can feature traces of classical reasoning while staying computational. We use this result in Section 4.4 to give an alternative proof of the recent result of Coquand and Mannaa [START_REF] Coquand | The independence of Markov's principle in type theory[END_REF] that Markov's principle is not provable in CIC.

Markov's Rule

We show in this section that CIC is closed under a generalized Markov's rule. The technique used here is no more than a dependently-typed variant of Friedman's trick [START_REF] Friedman | In: Classically and intuitionistically provably recursive functions[END_REF]. Indeed, Friedman's A-translation amounts to add exceptions to intuitionistic logic, which is precisely what T E does for CIC. Definition 8. A inductive type in CIC is said to be first-order if all the types of the arguments of its constructors, in its parameters and in its indices are recursively first-order. Example 3. The empty, unit and N types are first-order. If P and Q are firstorder then so is Σp : P. Q, P + Q and eq P p 0 p 1 . Consequently, the CIC equivalent of Σ 0 1 formulae are in particular first-order.

First-order types enjoy uncommon properties, like the fact that they can be injected into effectful terms and purified away. This is then use to prove the generalized Markov's Rule.

Lemma 9. For every first-order type p : P Q : where all P are first-order, there are retractions ι P , ι Q and θ P , θ Q s.t.:

p : P ι Q : Q → [[Q]]{ p := ι P p} p : P θ Q : [[Q]]{ p := ι P p} → Q + E.
Proof. The ι terms exist because effectful inductive types are a semantical superset of their pure equivalent, and the θ terms are implemented by recursively forcing the corresponding impure inductive term. One relies on decidability of equality of first-order type to fix the indices.

Theorem 11 (Generalized Markov's Rule). For any first-order type P and first-order predicate Q over P , if CIC Πp : P. ¬¬ (Q p) then CIC Πp : P. Q p.

Proof. Let M : Πp : P. ¬¬ (Q p). By taking E := Q p and apply the soundness theorem, one gets a proof

p : P [M ] : Πp : [[P ]]. ([[Q p]] → empty • ) → empty • .
But empty • ∼ = E ≡ Q p, so we can derive from [M ] a term M s.t.

p : P M : Πp : [[P ]]. ([[Q p]] → Q p + Q p) → Q p.
The proofterm we were looking for is thus no more than λp : P. M (ι P p) θ Q .

Function Intensionality with η-expansion

In a previous paper [START_REF] Boulier | The next 700 syntactical models of type theory[END_REF], we already showed that there existed a syntactic model of CIC that allowed to internally disprove function extensionality. Yet, this model was clearly not preserving definitional η-expansion on functions, as it was adding additional structure to abstraction and application (namely a boolean). Thanks to our new model, we can now demonstrate that counterintuitively, it is possible to have a consistent type theory that enjoys definitional η-expansion while negating internally function extensionality. In this section we suppose that E := unit, although any inhabited type of exceptions would work.

By Lemma 7, we know that the parametric exceptional translation preserves definitional η-expansion. It is thus sufficient to find two functions that are extensionality equal but intensionally distinct in the model. Let us consider to this end the unit → unit functions id ⊥ := λu : unit. u id := λu : unit. tt.

Theorem 12. The following sequents are derivable:

T p E Πu : unit. id ⊥ u = id u T p E id ⊥ = id → empty. Proof.
The main difference between the two functions is that id ⊥ preserves exceptions while id does not, which we exploit.

The first sequent is provable in CIC by dependent elimination and thus is derivable in T p E by applying the soundness theorem. To prove the first component of the second sequent, we exhibit a property that discriminates [id ⊥ ] and [id ], which is, as explained, their evaluation on the term unit ∅ tt. Showing then that this proof is parametric is equivalent to showing Π(p :

[[id ⊥ = id ]]) (p ε : [[id ⊥ = id ]] ε p). empty. But p ε actually im- plies [id ⊥ ] = [id ]
, which we just showed was absurd.

Independence of Premise

Independence of premise (IP) is a semi-classical principle from first-order logic whose CIC equivalent can be stated as follows.

Π(A : ) (B : N → ). (¬A → Σn : N. B n) → Σn : N. ¬A → B n (IP)
Although not derivable in intuitionistic logic, it is an admissible rule of HA. The standard proof of this property is to go through Kreisel's modified realizability interpretation of HA [START_REF] Kreisel | Interpretation of analysis by means of constructive functionals of finite types[END_REF]. In a nutshell, the interpretation goes as follows: by induction over a formula A, define a simple type τ (A) of realizers of A together with a realizability predicate • A over τ (A). Then show that whenever HA A, there exists some simply-typed term t : τ (A) s.t. t A. As the interpretation also implies that there is no t s.t. t ⊥, this gives a sound model of HA, which contains more than the latter. Most notably, there is for instance a term ip s.t. ip (¬A → ∃n. B) → ∃n. ¬A → B for any A, B. Intriguingly, the computational content of ip did not seem to receive a fair treatment in the literature. To the best of our knowledge, it has never been explicitly stated that IP was realizable because of the following "bug" of Kreisel's modified realizability.

Lemma 10 (Kreisel's bug). For every formula A, τ (A) is inhabited. In particular, τ (⊥) := unit.

We show that this is actually not a bug, but a hidden feature of Kreisel's modified realizability, which secretly allows to encode exceptions in the realizers. To this end, we implement IP in T p E by relying internally on paraproofs, i.e. terms raising exceptions, while ensuring these exceptions never escape outside of the locally unsafe boundary. The resulting T p E term has essentially the same computational content as its Kreisel's realizability counterpart. In this section we suppose that E := unit, although assuming E to be inhabited is sufficient.

To ease the understanding of the definition, we rely on effectful combinators that can be defined in T E . Definition 9. We define in T E the following terms.

fail : ΠA : . A [fail] := λA : [[ ]]. [A] ∅ tt isΣ : ΠA B. (Σx : A. B) → bool [isΣ] := λA B p. match p with | ex • _ _ ⇒ true • | Σ∅ _ ⇒ false • end is N : N → bool [is N ] := fix is N n := match n with | O • ⇒ true • | S • n ⇒ is N n | N∅ _ ⇒ false • end
It is worth insisting that these combinators are not necessarily parametric. While it can be shown that is Σ and is N actually are, fail is luckily not. The is Σ and is N functions are used in order to check that a value is actually pure and does not contain exceptions. Definition 10. We define ip in T E in direct style below, using the available combinators from Definition 9 and a bit of syntactic sugar.

ip : IP ip := λ(A : ) (B : N → ) (f : ¬A → Σn : N. B n). let p := f (fail (¬A)) in if isΣ N B p then match p with | ex n b ⇒ if is N n then ex _ _ n (λ_ : ¬A. b) else ex _ _ O (fail (¬A → B O)) end else ex _ _ O (fail (¬A → B O))
The intuition behind this term is the following. Given f : ¬A → Σn : N. B n, we apply it to a dummy function which fails whenever it is used. Owing to the semantics of negation, we know in the parametricity layer that the only way for this application to return an exception is that f actually contained a proof of A and applied fail to it. Therefore, given a true proof of ¬A, we are in an inconsistent setting and thus we are able to do whatever pleases us. The issue is that we do not have access to such a proof yet, and we do have to provide a valid integer now. Therefore, we check whether f actually provided us with a valid pair containing a valid integer. If so, this is our answer, otherwise we stuff a dummy integer value and we postpone the contradiction. This is essentially the same realizer as the one from Kreisel's modified realizability, except that we have a fancy type system for realizers. In particular, because we have dependent types, integers also exist in the logical layer, so that they need to be checked for exceptions as well. The only thing that remains to be proved is that ip also lives in

T p E . Theorem 13. There is a proof of T [[IP]] ε [ip].
Proof. The proof is straightforward but tedious, so we do not give the full details. The file IPc.v of the companion Coq plugin contains an explicit proof. The essential properties that make it go through are the following.

-T Π(n : N • ) (p 1 p 2 : N ε n). p 1 = p 2 -T Πn : N • . [is N ] n = true • ↔ N ε n -T Π(p q : [[¬A]]). [[¬A]] ε p → [[¬A]] ε q
Corollary 2. We have T p E IP.

Non-provability of Markov's Principle

From this result, one can get a very easy syntactic proof of the independence result of Markov's principle from CIC. Markov's principle is usually stated as ΠP : N → bool. ¬¬ (Σn : N. P n = true) → Σn : N. P n = true (MP)

An independence result was recently proved by Coquand and Mannaa by a semantic argument [START_REF] Coquand | The independence of Markov's principle in type theory[END_REF]. We leverage instead a property from realizability [START_REF] Troelstra | Metamathematical Investigation of Intuitionistic Arithmetic and Analysis[END_REF] that has been applied to type theory the other way around by Herbelin [START_REF] Herbelin | An intuitionistic logic that proves Markov's principle[END_REF].

Lemma 11. If S is a computable theory containing CIC and enjoying canonicity, then one cannot have both S IP and S MP.

Proof. By applying IP to MP, one easily obtains that S ΠP : N → bool. Σn : N. Πm : N. P m = true → P n = true.

Thus, for every closed P : N → bool, by canonicity there exists a closed n P : N s.t. S Πm : N. P m = true → P n P = true. But then one can decide whether P holds for some n by just computing P n P , so that we effectively obtained an oracle deciding the halting problem (which is expressible in CIC).

Corollary 3. We have CIC p E MP and thus also CIC MP.

5 Possible extensions

Negative Records

Interestingly, the fact that the translation introduces effects has unintented consequences on a few properties of type theory that are often taken for granted. Namely, because type theory is pure, there is a widespread confusion amongst type theorists between positive tuples and negative records. In the remainder of this section, we wil focus on the specific case of pairs, but the same arguments are generalizable to arbitrary records. Positive pairs Σx : A. B are defined by the inductive type from Figure 4. Negative pairs &x : A. B are defined as a primitive structure in Figure 7. We use the ampersand notation as a reference to linear logic. In CIC, it is possible to show that negative and positive pairs are propositionally isomorphic, because positive pairs enjoy dependent elimination. Nonetheless, it is a well-known fact in the programming folklore that in a call-by-name language with effects, the two are sharply distincts. For instance, in presence of exceptions, assuming M : Σx : A. B, one does not have in general

M ≡ ex A B (fst A B M ) (snd A B M )
where fst and snd are defined by pattern-matching. Indeed, if M is itself an exception, the two sides can be discriminated by a pattern-matching. Matching on the left-hand side results in immediate reraising of the exception, while matching on the right-hand side succeeds as long as the arguments of the constructor are not forced. Forcefully equating those two terms would then result in a trivial equational theory.

Such a phenomenon is at work in the exceptional translation. It is actually possible to interpret negative pairs through the translation, but in a way that significantly differs from the translation of positive pairs. In this section, we assume that T contains negative pairs. Definition 11. The translation of negative pairs is given in Figure 8.

It is straightforward to check that the definitions of Figure 8 preserve the conversion and typing rules from Figure 7. The same translation can be extended to any record. We thus have the following theorem. Theorem 14. If T has negative records, then so has T E .

It is enlightening to look at the difference between negative and positive pairs through the translation, because now we have effects that allow to separate them clearly. Indeed, compare

[[&x : A. B]] ≡ &x : [[A]]. [[B]] with [[Σx : A. B]] ∼ = E + Σx : [[A]]. [[B]].
Clearly, if E is inhabited, then the two types do not even have the same cardinal, assuming A and B are finite. Furthermore, their default inhabitant is not the same at all. It is defined pointwise for negative pairs, while it is a special constructor for positive ones. Finally, there is obviously not any chance that [[Σx : A. B]] satisfies definitional surjective pairing in vanilla CIC, as it has two constructors. The trick is that the two types are externally distinguishible, but are not internally so, because T E is a model of CIC + & and thus proves that they are propositionally isomorphic.

It is possible to equip negative pairs with a parametricity relation defined as a primitive record which is the pointwise parametricity relation of each field, which naturally preserve typing and conversion rules.

Theorem 15. If T has negative records, then so has T p E .

Impredicative Universe

All the systems we have considered so far are predicative. It is nonetheless possible to implement an impredicative universe * in T E if T features one. We only allude to the construction here, a detailed account can be found in the Appendix. Intuitively, it is sufficient to ask for an inductive type prop living in i for all i, which is defined just as type, except that its constructor PropVal corresponding to TypeVal contains elements of * rather than . Then one can similarly define El * and Err * acting on prop rather than type. One then slightly tweaks the [[•]] macro from Figure 2 by defining it instead as

[[A]] := El * [A] if A : * El [A] otherwise
and similarly for type constructors. With this modified translation, one obtains a soundness theorem for CC ω .

Theorem 16. The exceptional translation is a syntactic model of CC ω + * .

Likewise, the inductive translation is amenable to interpret an impredicative universe, with one major restriction though.

Theorem 17. The exceptional translation is a syntactic model of CIC + * without the singleton elimination rule.

Indeed, the addition of the default constructor disrupts the singleton elimination criterion for all inductive types. Actually, this criterion is very fragile, and even if T E satisfied it, Keller and Lasson showed that the parametricity translation could not interpret inductive types in * for similar reasons [START_REF] Keller | Parametricity in an impredicative sort[END_REF], and T p E would face the same issue.

6 The Exceptional Translation in Practice The first command produces only [list], while the second produces [list] ε . But the main interest of the translation is that we can exhibit new constructors. For instance, the raise operation described in Section 2.4 is defined as Effect Definition Exception : Type := fun E ⇒ TypeVal E E id. Effect Definition raise : ∀ A, Exception → A := fun E (A : type E) ⇒ Err A.

Usecase: A Cast Framework

We can use the ability to raise exception to define partial function in the exceptional layer. For instance, given a decidable property (described by the type class below), it is then possible to define a cast function from A to Σ (a : A). P a returning the converted value if the property is satisfied and raising an exception otherwise (using an inhabitant cast_failed of Exception).

Using this cast mechanism, it is easy to definition a function list_to_pair from lists to pairs by first converting the list into a list size two, using the impure function cast (list A) (fun l ⇒ List.length l = 2) and then recovering a pair from a list of size two using a pure function.

In the exceptional layer, it is possible to prove the following property Definition list_to_pair_prop A (x y : A) : list_to_pair [x ; y] = (x,y).

in at least two way. One can perfectly prove it by simply raising an exception at top level, or by reflexivity-using the fact that list_to_pair [x ; y] actually reduces to (x,y).

However, there is a way to distinguish between those two proofs in the target theory, here Coq, by stating the following lemma which can only proven for the proof not raising an exception.

Definition list_to_pair_prop_soundness A x y :

list_to_pair_prop • A x y = eq_refl • _ _ _ := eq_refl _.
where underscores represent arguments inferred by Coq.

Related Work

Adding dependency to an effectful language. There are numerous works on adding dependent types in mainstream effectful programming languages. They all mostly focused on how to appropriately restrict effectful terms from appearing in types. Indeed, if types only depend on pure terms, the problem of having two different evaluations of the effect of the term (at the level of types and at the level of terms) disappear. This is the case for instance for Dependent ML of Xi and Pfenning [START_REF] Xi | Dependent types in practical programming[END_REF], or more recently for Casinghino et al. [START_REF] Casinghino | Combining proofs and programs in a dependently typed language[END_REF] on how to combine proofs and programs when programs can be non-terminating. The F programming language of Swamy et al. [START_REF] Swamy | Dependent types and multi-monadic effects in F*[END_REF] uses a notion of primitive effects including state, exceptions, divergence and IO. Each effects is described through a monadic predicate transformer semantics which allows to have a pure core dependent language to reason on those effects. On a more foundational side, there are two recent and overlapping lines of work on the description of a dependent call-by-push-value (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]. Those works also use a purity restriction for dependency, but using the CBPV language, deals with any effect described in monadic style. On another line of work, Brady advocates for the use of algebraic effects as an elegant way to allow combing effects more smoothly than with a monadic approach and gives an implementation in Idris [START_REF] Brady | Idris, a general-purpose dependently typed programming language: Design and implementation[END_REF].

Adding Effects to a dependently-typed language. Nanevski et al. [START_REF] Nanevski | Hoare type theory, polymorphism and separation[END_REF] have developed Hoare type theory (HTT) to extend Coq with monadic style effects. To this end, they provide an axiomatic extension of Coq with a monad in which to encapsulate imperative code. Important tools have been developed on HTT, most notably the Ynot project [START_REF] Chlipala | Effective interactive proofs for higher-order imperative programs[END_REF]. Apart from being axiomatic, their monadic approach does not allow to mix effectful programs and dependency but is rather made for proving inside Coq properties on simply typed imperative programs.

Internal translation of type theory. A non-axiomatic way to extend type theory with new features is to use internal translation, that is translation of type theory into itself as advocated for by Boulier et al. [START_REF] Boulier | The next 700 syntactical models of type theory[END_REF]. The presentation of parametricity for type theory given by Bernardy and Lasson [START_REF] Bernardy | Realizability and parametricity in pure type systems[END_REF] can be seen as one of the first internal translation of type theory. However, this one does not add any new power to type theory as it is a conservative extension. Barthe et al. [START_REF] Barthe | CPS translations and applications: The cube and beyond[END_REF] have described a CPS translation for CC ω featuring call-cc, but without dealing with inductive types and relying on a form of type stratification. A variant of this translation has been extended recently by Bowman et al. [START_REF] Bowman | Type-preserving CPS translation of σ and π types is not not possible[END_REF] to dependent sums using answer-type polymorphism Πα : . (A → α) → α. A generic class of internal translation has been defined by Jaber et al. [START_REF] Jaber | The definitional side of the forcing[END_REF] using forcing, which can be seen as a type theoretic version of the presheaf construction used in categorical logic. This class of translation works on all CIC but for a restricted version of dependent elimination, identical to the Baclofen type theory [START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF]. Therefore, to the best of our knowledge, the exceptional translation is the first complete internal translation of CIC adding a particular notion of effect.

Conclusion and Future Work

In this paper, we have defined the exceptional translation, the first syntactic translation of the Calculus of Inductive Constructions into itself, adding effects and that covers full dependent elimination. This result in a new type theory, which features call-by-name exceptions with decidable type-checking and a weaker form of canonicity. We have shown that although the resulting theory is inconsistent, it is possible to reason on exceptional programs and show that some of them actually never raise an exception by relying on the target theory. This provides a sound logical framework allowing to transparently prove safety properties about impure dependently-typed programs. Then, using parametricity, we have given an additional layer at the top of the exceptional translation in order to tame exceptions and preserves consistency. This way, we have consistently extended the logical expressivity of CIC with independence of premises, Markov's rule, and the negation of function extensionality while retaining ηexpansion. Both translations have been implemented in a Coq plugin, which we use to formalize the examples. One of the main direction of future work is to investigate whether other kind of effects can give rise to an internal translation of CIC. To that end, it seems promising to look at algebraic presentation of effects. Indeed, the recent work on the non-necessity of the value restriction policy for algebraic effects and handlers of Kammar and Pretnar [START_REF] Kammar | No value restriction is needed for algebraic effects and handlers[END_REF] suggests that we should be able to perform similar translations on CIC with full dependent elimination for other algebraic effects and handlers than exceptions.

One could also hope that the exceptional translation is a model of CIC + * too. Although we will not give the full details, we argue here that is almost the case... but not quite. The only thing we have to do is to provide a translation for inductive types living in * together with their pattern-matching. Definition 17. The translations from Definitions 3 and 4 can be carried out in presence of an impredicative universe in a similar way, by applying the changes from Definition 16 and changing TypeVal into PropVal for inductive types living in * .

For the same reason as their predicative counterpart, this translation preserves typing, but for a critical detail.

Theorem 21. The exceptional translation is a syntactic model of CIC + * without the singleton elimination rule.

Proof. It is not hard to adapt the arguments to prove that typing is preserved similarly. Failure of preservation of singleton elimination is discussed below.

Singleton elimination is a key feature of CIC + * that acts as an escape hatch to make information flow from * to . This rule can be formalized as follows: pattern-matching over a term in an inductive type in * whose return clause is in is forbidden, except if the two following conditions are met:

1. The inductive type being matched over has at most one constructor. 2. If it has one, all its arguments live in * .

It is very simple to check why the exceptional translation breaks singleton elimination. First, it adds a new default constructor, so that any type with one constructor has now two. The only types that may preserve singleton elimination have thus no constructors, i.e. they are empty. But the default constructor of any inductive type takes as an argument a term of type E, which lives in . Therefore, no translated inductive satisfy the singleton elimination criterion.

This means that, although the translation can interpret an impredicative universe, there is no way to make any information flow from the latter to any predicative universe. Somehow, the two worlds are completely disconnected.

•Fig. 1 .

 1 Fig. 1. Typing rules of CCω

[Fig. 3 .

 3 Fig. 3. Inductive Type Translation

Example 1 .

 1 We give a few representative examples of the inductive translation in Figure 4 in a Coq-like syntax. They were chosen because they are simple instances of inductive types featuring parameters, indices and recursion in an orthogonal way. For convenience, we write Σ A (λx : A. B) as Σx : A. B.

Fig. 4 .

 4 Fig. 4. Examples of Translations of Inductive Types

Definition 4 .

 4 Assume an inductive I as given in Definition 3. Let Q be the well-typed pattern-matching defined as Lemma 4. The translation preserves ι-rules.

Fig. 5 .

 5 Fig. 5. Parametricity over Exceptional Translation

Definition 5 .

 5 The theory T p E is defined by the following data. -Terms of T p E are pairs of terms of T . -Contexts of T p E are pairs of contexts of T .

Theorem 7 .

 7 If T interprets CC ω then so does T p E . That is, the parametric exceptional translation is a syntactic model of CC ω .

Fig. 6 .

 6 Fig. 6. Examples of Parametric Translation of Inductive Types

  match x return λ(i1 : I1) . . . (im : Im) (x : I X1 . . . Xn i1 . . . im). R with | c1 a1,1 . . . a 1,l 1 ⇒ N1 . . . | c k a k,1 . . . a k,l k ⇒ N k end

ΓFig. 7 .Fig. 8 .

 78 Fig. 7. Negative pairs

  6.1 Implementation as a Coq PluginThe (parametric) exceptional translation is a translation of CIC into itself, which means that we can directly implement it as a Coq plugin. This way, we can use the translation to extend safely Coq with new logical principles, so that typechecking remains decidable.Such a Coq plugin is simply a program that, given a Coq proof term M , produces the translations [M ] and [M ] ε as Coq terms. For instance, the translations of type list, given in Figures4 and 6, are obtained by typing the following commands, which define each one new inductive type in Coq.

	Effect Translate list.
	Parametricity Translate list.

The fact that the resulting exception are call-by-name is explained in detailed in[START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF] using a call-by-push-value decomposition. Intuitively, it comes from the fact that CIC is naturally call-by-name.

The plugin is available at https://github.com/CoqHott/exceptional-tt.2A, B, M, N ::= i | x | M N | λx : A. M | Πx : A. B Γ, ∆ ::= • | Γ, x : A Γ i < j Γ i : j Γ M : B Γ A : Γ, x : A M : B Γ A : i Γ, x : A B : j Γ Πx : A. B : max(i,j) Γ M : B Γ A : A ≡ B Γ M : A Γ,x : A M : B Γ Πx : A. B : Γ λx : A. M : Πx : A. B Γ M : Πx : A. B Γ N : A Γ M N : B{x := N }

The notation El refers to universes à la Tarski in Martin-Löf type theory.

match M return λ(i1 : I1) . . . (im : Im) (x : I X1 . . . Xn i1 . . . im). R with | c1 a1,1 . . . a 1,l 1 ⇒ N1 . . . | c k a k,1 . . . a k,l k ⇒ N k end

-Positive tuples are defined as a one-constructor inductive type, introduced by this constructor and eliminated by pattern-matching. They do not (and in general cannot, for typing reasons) satisfy definitional η-laws, also known as surjective pairing.-Negative records are defined as a record type, introduced by primitive packing and eliminated by projections. They naturally obey the definitional ηlaw. 20 A, B, M, N ::= . . . | &x : A. B | M, N | M.π1 | M.π2 Γ 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}

Class Decidable (A : Type) := dec : A + (not A). Definition cast A (P : A → Type) (a:A) {Hdec : Decidable (P a)} : Σ (a : A). P a := match dec (P a) with | inl p ⇒ (a ; p) | inr _ ⇒ raise cast_failed end.

CIC becomes fairly blurry at this point about the specification of positivity for records, as the only reference is the Coq implementation. There is no formal proof that it is a sound system whatsoever, and in practice a few surprises arose like the inconsistency of definitional η-laws for co-inductive types.

Proof. Mostly a consequence of Theorem 1 applied to all of the premises of the pattern-matching rule. The only thing we have to check specifically is that the branch for the default constructor I ∅ is well-typed as

which is also due to Theorem 1 applied to R.

A Appendix

A.1 Negative Records

In this section we describe the generic translation of negative records, that is, structures defined by their projections and satisfying definitional η-laws.

We define the exceptional translation of R and its constructors in Figure 9, where R • is the record type defined by

where in the recursive calls in the various A, we locally set

We give examples of this translation in Figure 10 in a Coq-like syntax. For completeness, we show that we can also handle co-inductive records.

Remark that in particular, the default value is defined pointwise, e.g.

which is completely different from the default value one would have obtained in the one-constructor inductive type case.

It is straightforward to check that this translation preserves both typing and reduction rules, as well as positivity conditions in the absence of nested record types 6 . This translation can be extended to the parametric case in a generic way. Once again, there is fundamental difference with the inductive case. Instead of enforcing parametricity through an index, the parametric exceptional translation of records has an additional parameter, and parametricity is ensured pointwise for every projection. We define this formally below. Definition 13. Let the record type R be defined as above. We define the exceptional parametricity record translation R ε as the record

We give examples of the parametric translation in Figure 11.

The parametricity translation can be shown to preserve typing and reduction.

Theorem 19. If T has negative records, then so has T p E .

A.2 Impredicative Universe

Although we only considered predicative universes up to now, it is actually possible to interpret an impredicative universe through the exceptional translation. Rules for manipulation of an impredicative universe are given in Figure 12. We assume in this section that T features an impredicative universe. It is not very difficult to adapt the translation to account for such a sort. We simply require that T features the following additional structure, which is the equivalent of type for an impredicative universe. Definition 14 (Exceptional Prop). We assume that T features the data below, where the i index stands for universe polymorphism.

prop : i -PropVal : ΠA : * .

subject to the following definitional equations:

The prop type is just an inductive type (in !), but is once again posited instead of declared as such for the sake of simplicity. Also, Ω * serves the very same purpose for * as Ω i does for i and can be taken to be degenerate in the same way.

Just as for exceptional types, it is possible to derive the following functions.

Definition 15. We derive the following definitions. In order to properly extend the translation to interpret CC ω + * , one would technically need to annotate λ, Π and context variables with the sort they are supposed to live in so that the translation operates at the level of pure terms instead of derivations. While doable, this would be cumbersome, and as we only want to show a proof of concept, we stick to an intuitive but slightly wrong presentation here.

Definition 16 (Exceptional Translation of CC ω + * ). The translation is defined as in Figure 2, except that we override the following macros.

[ * ] := TypeVal prop PropErr

Note that this translation would not be able to interpret a cumulativity relation of the form * ⊆ i , as this would require prop ≤ type i which is not the case if we implement them as distinct inductive types. Here, this does not matter as we did not endow CC ω with such a cumulativity relation. Proof. We only have to specifically check the following properties, the rest is a variation over Theorem 1.


A Levisse

B Giraud

J P Noël

M Moreau

J M Portal

SneakPath Compensation Circuit for Programming and Read Operations in RRAM-based CrossPoint Architectures

Keywords: CrossPoint, NonVolatile Memory, RRAM, compensation circuit, Multiple Level Cell

Passive crossbar memories based on resistive switching bit-cells are today seen as the most promising candidates for flash memories replacement. However, inherent sneak currents through unselected devices lead to low operating margins and over-consumption during read and programing operations. Crossbar memory simulations with bit-cells based on two terminal nonlinear selectors, also show degraded performances due to sneak path currents, leading to nonfunctional memories. Thus, peripheral circuits have to be designed in order to mitigate the sneak currents that impact memory operations. In this paper, we propose a dynamic sneak current compensation circuit for SET and read operations, enabling multi-level cell programming. This circuit is simulated using CMOS 130nm Bulk core process with OxRAM and tunnel barrier-based selector bit-cell.

I. INTRODUCTION

While conventional non-volatile memories (NVM) turn out to be more and more costly and complex to co-integrate with conventional CMOS process, emerging back-end of line resistive switching memories (RRAM) are becoming more and more attractive for high density NVM [START_REF] Lee | Scaling trends and challenges of advanced memory technology[END_REF]. Oxide-based RRAM (OxRAM) are one of the most encouraging RRAM technologies due to non-exotic materials, high scalability and fast switching [START_REF] Benoist | Advanced CMOS Resistive RAM Solution as Embedded Non-Volatile Memory[END_REF]. The conventional 1T1R bit-cell architecture provides good performances but it suffers from a high silicon surface due to access transistor since the bit-cell area has to be as small as possible in order to reduce as maximum the manufacturing cost. In this context, RRAM-based crossbar memories appear to be a promising candidate thanks to an ultradense structure (4F²) and 3D stackability [START_REF] Kawahara | An 8 Mb Multi-Layered Cross-Point ReRAM Macro With 443 MB/s Write Throughput[END_REF].

It has been demonstrated that RRAM bit-cell with linear behavior in crossbar memories leads to an unacceptable overconsumption, degraded read performance and limited array size due to inherent sneak currents through unselected RRAM bitcells (Sneak-Path, SP) [START_REF] Liang | Cross-Point Memory Array Without Cell Selectors-Device Characteristics and Data Storage Pattern Dependencies[END_REF]. To reduce the SP issues, non-linear RRAM devices have been intensively studied [START_REF] Chen | A Comprehensive Crossbar Array Model With Solutions for Line Resistance and Nonlinear Device Characteristics[END_REF]. These nonlinear devices are realized by stacking a RRAM with a nonlinear element to form a 1 Selector / 1 RRAM (1S1R) bit-cell, as illustrated in Fig. 1. Different structures of selectors are reported in the literature [START_REF] Woo | Electrical and Reliability Characteristics of a Scaled (~30nm) Tunnel Barrier Selector (W/Ta2O5/TaOx/TiO2/TiN) with Excellent Performance (JMAX > 107A/cm2)[END_REF] [7] [START_REF] Cha | Nanoscale (~10nm) 3D vertical ReRAM and NbO2 threshold selector with TiN electrode[END_REF], each having specific physical and electrical characteristics to mitigate the SP and reduce its impact. The selector purpose is to reach an ultra-low current in the off-state and a steep transition to the on-state with a high current.

To achieve a high-capacity RRAM-based crossbar array, the SP effect has to be reduced as much as possible. To mitigate the SP, polarization schemes are applied on the unselected elements of the array, but they are not sufficient to fully counterbalance its impact on operations. Therefore, a peripheral circuitry has to be designed in order to better compensate the SP effect. Sampling-based SP compensation circuits using Analog-to-Digital converters (ADC) are studied in the literature [START_REF] Liu | A 130.7-mm 2-Layer 32-Gb ReRAM Memory Device in 24-nm Technology[END_REF] [START_REF] Baek | A Reliable Cross-Point MLC ReRAM with Sneak Current Compensation[END_REF]. The fact that the sampled SP current is compensated using programmable current limitation implies that a large peripheral circuit is needed to ensure a sufficient ADC precision. This approach is performed in 2 steps: firstly the SP is sampled and in a second time, the programing is done.

In this paper, the SP impact on programming operations is studied and a novel SP compensation circuit is proposed. The presented circuit provides immunity to SP, which can be used for Multi-Level Cell (MLC) programming, and also for precise read operation. The SP is dynamically monitored and compensated in order to provide a one-step programming operation. The presented circuit is also studied for use as a sense amplifier on MLC programming operations.

Section II describes the RRAM device model, the selector device and the simulation methodology used in this work. Section III focuses on the proposed circuit during programing operation, whereas Section IV deals with its use for read operations. Finally, Section V draws the conclusions and perspectives.

II. BIT-CELL MODELING AND ARRAY BIASING SCHEME

Two dedicated 1S1R models are considered for simulations: an HfO2/Ti-based bipolar OxRAM compact model calibrated on silicon data [START_REF] Bocquet | Robust compact model for bipolar oxide-based resistive switching memories[END_REF] and a Ta2O5/TaOx/TiO2 tunnel barrier-based selector model [START_REF] Woo | Electrical and Reliability Characteristics of a Scaled (~30nm) Tunnel Barrier Selector (W/Ta2O5/TaOx/TiO2/TiN) with Excellent Performance (JMAX > 107A/cm2)[END_REF]. An array of 1S1R bit-cells with post-layout parasitic elements is simulated using Eldo simulator (Fig. 1). Concerning technology, 130nm CMOS Bulk technology from STMicroelectronics is considered. During a read or write operation in a crossbar array, SP currents degrade the operation efficiency (read margin reduction and write current control reduction) [12] [13]. Fig. 1 shows the programming current through the selected bit-cell and the SP current through the unselected ones. To overcome this issue, specific wordline (WL) and bitline (BL) polarization schemes are used (Fig. 2). The selected WL (SWL) is polarized at Vselect and the selected BL (SBL) is pulled to the ground. Intermediate voltages (Vselect/2) are applied to unselected WLs (UWL) and BLs (UBL). This commonly used polarization scheme is named ½ bias in the literature [START_REF] Zhang | Selector Design Considerations and Requirements for 1S1R RRAM Crossbar Array[END_REF]. The ½ bias is used in rest of the paper.

Fig. 2:

Diagram of crossbar array with detailed polarization scheme for SP mitigation. This polarization scheme is the best in terms of power efficiency because almost all the array is not concerned with SP [START_REF] Zhang | Selector Design Considerations and Requirements for 1S1R RRAM Crossbar Array[END_REF].

III. SNEAKPATH COMPENSATION CIRCUIT FOR PROGRAMMING

OPERATIONS

As described in Fig. 2, the SWL current is the sum of the SP current and the selected bit-cell current. Thus, during a SET operation, current control on the selected bit-cell is hard to reach due to the SP effect [START_REF] Baek | A Reliable Cross-Point MLC ReRAM with Sneak Current Compensation[END_REF]. Considering a constant programing current on the SWL, when the array size increases, the programing current decreases as shown in Fig. 4-a. This programming current degradation can be compensated while increasing the current reference value (Iref). However, this approach leads to an increase of programming current variability due to the unselected bit-cell resistance states. Regardless how the Iref compensation is done (compensation on the 50%LRS-50%HRS array as shown Fig. 4b), it leads to a larger distribution of the programing current. Moreover, it has been demonstrated that lower is the programming current, wider is the programmed resistance values distribution [START_REF] Garbin | Modeling of OxRAM Variability from Low to High Resistance State using a Stochastic Trap Assisted Tunneling-based Resistor Network[END_REF]. This shows that the SP has to be considered as a major constraint in the SET circuit conception. Fig. 5 presents the proposed circuit architecture to overcome the SP issues during SET operations. Compensation can be done using 50%HRS-50%LRS array. In this case, with a low SP current (full HRS array) the programming current is increased. Oppositely, the programming current is reduced in a full LRS array. This leads to an increased variability of the reached resistance. During a programing phase, UWLs and UBLs are polarized to half of the programing voltage. This polarization scheme limits SP currents to the SWL and SBL. The current provided by the SWL contains two distinct contributions: the programing current (IPROG) and the parasitic current pulled by unselected BLs (IUBL). Considering IPROG_REF as a current reference corresponding to the targeted programing current, it is possible to compare IPROG + IUBL to IPROG_REF + IUBL. When it passes over IPROG_REF, the COMP_OUT signal switches from 0 to VDD. This process stops the programing operation and limit the current flowing through the selected bit-cell. LDOs are connected to the SWL and UBLs in order to control the voltages applied in the array. The consumed current is measured with current mirrors connected to the LDOs. Currents mirrors can also be cascoded to provide a better current copy. The two currents (IPROG_REF + IUBL and IPROG + IUBL) are read with the VCOMP+ and VCOMPsignals. These voltages are compared with a differential amplifier.

Simulation results are presented in Fig. 6. We compare the proposed structure (Fig. 5) to circuits shown in Fig. 3. The proposed circuit provides SP immunity and thus a fine control of the programming current. Fig. 6: Programing current evolution in the selected bit-cell vs array size (considering a crossbar array with a square form factor). The proposed circuit (Fig. 5) is neither impacted by the array size nor by the resistance state (LRS or HRS) of unselected bit-cells in the array.

IV. SNEAKPATH COMPENSATION CIRCUIT FOR MLC READ OPERATIONS

In a large crossbar array and due to SP, reading different resistance level on the same bit-cell can be difficult to operate without increasing significantly the read consumption [START_REF] Lee | Comprehensive Methodology for ReRAM and Selector Design Guideline of Cross-point Array[END_REF]. The proposed SP compensation circuit can be advantageously used to increase the read precision. This section presents a way to read a MLC bit-cell in crossbar arrays based on the circuit concept presented in Fig. 5. V. CONCLUSISON This paper presents a SP compensation circuit to overcome SET and read operation issues in the RRAM-based crossbar memory circuits. SP impact on programming operation precision is detailed and an innovative circuit is proposed to solve this issue. The presented circuit enhance the immunity to SP currents which enables the design of larger arrays (here, with the considered selector, a 256BL array can be designed). For MLC operations, we demonstrated that a SP compensation circuit is mandatory and showed the operation of a 2 data bits bit-cell using the presented circuit. In order to improve read operations, a read circuit, based on the programming compensation circuit and optimized for MLC operation, is proposed. The presented structures opens the way for MLC operation in crosspoint array which is an efficient way to increase the memory density.

VI. RÉFÉRENCES

Fig. 1 :

 1 Fig. 1: Crossbar architecture based on 1S1R bit-cell. The bitcell consists of two devices: an HfO2/Ti-based bipolar RRAM and a Ta2O5/TaOx/TiO2 tunnel barrier-based selector.

Fig. 3

 3 Fig. 3 shows a programing circuit containing two blocks: a simple current mirror and a voltage regulation (Low DropOut Regulator -LDO).

Fig. 3 :

 3 Fig. 3: Schematic diagram of a programming architecture. It contains a current mirror and a LDO regulator. The LDO part is added in order to maintain the SET voltage on the SWL.

Fig. 4 :

 4 Fig. 4: (a) Programing current reduction due to SP as a function of array size. (b) For each array size, the current reference (Iref) is increased to compensate the SP.Compensation can be done using 50%HRS-50%LRS array. In this case, with a low SP current (full HRS array) the programming current is increased. Oppositely, the programming current is reduced in a full LRS array. This leads to an increased variability of the reached resistance.

Fig. 5 :

 5 Fig. 5: Schematic diagram of the proposed programing circuit providing SP immunity with fine SET current tuning. Multiplexers are based on full analog switches; MUX control signals activate only the selected WL and BL in SMUX. Complemented addresses activate all the switches in UMUX except the selected ones.

Fig. 7

 7 Fig. 7 presents a one-cycle read circuit based on Fig.5. Several current references (Iref0-2) are added to the SP (IBL) and are compared to the read current (IWL). For a 2 data-bits MLC RRAM, 3 different references are used to read the 4 different resistances states. D<0-2> bits are generated comparing the V_Iread to the 3 references V_Iref_0-2. Fig 8-a shows the resistance distributions obtained with 1000 Monte-Carlo simulations per programming current. CMOS variability and state of the unselected resistances are taken into account in

Fig. 7 :

 7 Fig. 7: Schematic diagram of the proposed circuit for read MLC (3 bits) in 1 cycle using ½ bias polarization scheme. The READ_pulse signal activates the selected WL LDO.

Fig. 8 :

 8 Fig. 8: (a) Read current distribution (1000 Monte Carlo samplings) for the circuit presented in Fig. 5 with detailed choice of the current references. (b) Correspondence table between resistance state and output code (D<0-2>). (c) Transient evolution of D<0-2> during a read pulse.


Mathieu Moreau

Daniela Munteanu

Jean-Luc Autran

Florence Bellenger

Jérôme Mitard

Michel Houssa

Quantum Simulation of C-V and I-V Characteristics in Ge and III-V Materials/High-κ MOS Devices

We present a one-dimensional simulation study of the capacitance-voltage (C-V) and currentvoltage (I-V) characteristics in MOS devices with high mobility semiconductors (Ge and III-V materials) and non-conventional gate stack with high-κ dielectrics. The C-V quantum simulation code self-consistently solves the Schrödinger and Poisson equations and the electron transport through the gate stack is computed using the non-equilibrium Green's function formalism (NEGF). Simulated C-V characteristics are successfully confronted to experimental data for various MOS structures with different semiconductors and dielectric stacks. Simulation of I-V characteristics reveals that gate leakage current strongly depends on gate stacks and substrate materials and predicts low leakage current for future CMOS devices with high mobility materials and high-κ dielectrics.

INTRODUCTION

In order to improve complementary metal-oxide-semiconductor (CMOS) technology performances for future technological nodes (sub 22-16 nm), high mobility (high-µ) semiconductors with high permittivity (high-κ) dielectric-based gate stacks have been recently considered to replace the historical SiO 2 /Si structure [1].

Due to low values of the carrier conductivity effective masses in both valence and conduction bands, which leads to higher hole and electron mobilities than in Si, Ge and III-V materials are seriously considered in recent works to respectively enhance p-MOSFET and n-MOSFET performances, especially the on-state current in high-performance logic applications. Moreover, the introduction of high-κ dielectrics can reduce tunneling current through the gate stack while maintaining control of the current in the channel by the gate even for structures with very low equivalent oxide thickness (EOT) [START_REF] Houssa | High-κ Gate Dielectrics[END_REF].

However, the fabrication of high-κ/Ge (or III-V) devices in terms of surface passivation between gate oxide and channel material is still not well controlled and remains a challenge to meet ITRS roadmap requirements. Over the past few years, countless techniques and materials have been used to manufacture devices (GeO 2 [START_REF] Delabie | [END_REF][START_REF] Xie | IEDM 08 Proceedings[END_REF][START_REF] Nakakita | IEDM 08 Proceedings[END_REF], La 2 O 3 [START_REF] Andersson | ESSDERC 09 Proceedings[END_REF], Ga 2 O 3 (Gd 2 O 3 ) [START_REF] Lin | [END_REF], Al 2 O 3 [8], HfO 2 /SiO 2 /Si [START_REF] Mitard | IEDM 08 Proceedings[END_REF], HfO 2 [START_REF] Bai | [END_REF]); all these technologies lead to complicated structures with multi layer gate stacks, for which it is difficult to precisely extract key parameters and predict future performances.

In this context, we present a one-dimensional (1D) simulation study of capacitance-voltage and current-voltage characteristics in MOS devices with high-µ channel materials and multi layer high-κ gate stacks. We self-consistently solve Poisson and Schrödinger equations to compute the quantum carrier density and we use it to calculate the capacitance and the gate leakage current as a function of the applied gate voltage.

THEORETICAL DETAILS

The simulation code is based on the 1D self-consistent numerical solving of the Poisson and Schrödinger equations coupled with the computation of the high/low frequency capacitance and the calculation of the gate current in MOS devices.

In order to calculate the "quantum" carrier (electrons and holes) densities, we have to solve the time-independent, effective mass 1D Schrödinger equation. The numerical solution of this equation is obtained by using the three-point finite-difference scheme applied to a non-uniform mesh along x-axis (figure 1) [START_REF] Raynaud | Structure and Electronic Properties of Ultrathin Dielectric Films on Silicon and Related Structures[END_REF]12]. The total quantum electron and hole densities (2D gas) are obtained as in [START_REF] Raynaud | Structure and Electronic Properties of Ultrathin Dielectric Films on Silicon and Related Structures[END_REF] and used to solve the 1D Poisson equation with a material-dependent dielectric constant (ε i ) along the grid.

Once the Schrödinger-Poisson system is solved, the resulting quantum carrier density in the substrate is used for calculating the low and high-frequency capacitance of the structure [12]. The gate current density is evaluated from the 2D carrier gas in the inversion regime using the formalism presented in [13,14], where the carrier transmission probability is calculated with the Wentzel-Kramers-Brillouin (WKB) classical approximation.

Metal

Oxides Semiconductor

1 ox C E ∆ 2 ox C E ∆ 2 ox V E ∆ 1 ox V E ∆
However, quantum-mechanical effects markedly affect the transport of carrier and the WKB approximation is not able to perfectly describe quantum reflections against abrupt electrical potential variations as it is the case in MOS devices with multi layer gate stacks [15]. Thus, we have also computed the gate current using a full quantum-mechanical approach, namely the nonequilibrium Green's function (NEGF) formalism [16]. This method solves the Schrödinger equation with open boundary conditions, taking into account both wave-function reflections and attenuations on the potential barrier (figure 1), and was adapted for metal-insulator-metal (MIM) structures [15,17] with an effective-mass depending on the position along a 1D grid in the transport direction.

The main material parameters used in simulations are presented in Table I. It is important to note that these constants (dielectric constant, effective mass…) strongly depend on the fabrication process and are not exactly known, especially for dielectric materials. Thus, the values in the simulation code can be adapted in order to improve the fit between experimental and simulation results. I). The discretization of the 1D structure using a uniform mesh in oxides and nonuniform mesh in semiconductor is also represented. [START_REF] Delabie | [END_REF]18,19] of different semiconductors and dielectric materials used for MOS device simulation. The band offsets between oxides and semiconductors (not shown here) are the same as in reference [20] except for Ge/GeO 2 interface [18].

Table I. Main material parameters

EG (V) ε/ε0 m *

RESULTS AND DISCUSSION

We first illustrate C-V characteristics by comparing, in figure 2, our simulated results and experimental data [START_REF] Delabie | [END_REF] for high-frequency curves in two different double-layer gate stacks with a p-doped Ge substrate. Simulated and experimental data are in good agreement in depletion and accumulation regimes, which show the possibility to use the simulated curves to extract oxide material parameters such as dielectric constant, interfacial layer physical thickness and flat-band voltage [12]. We have also adapted our simulation code to calculate C-V characteristics for different III-V semiconductors. Figure 3 compares simulation results for various Al 2 O 3 /III-V materials MOS devices (T Al2O3 = 2.3 nm, i.e. EOT = 1.0 nm) for which the gate work function is equal to 5 eV for all structures. We can see in this figure that the depletion zone strongly depends on the semiconductor bandgap, i.e. smaller is the bandgap and shorter is the depletion zone thickness (in terms of gate voltage). Moreover, the very low effective density of state in the conduction band of III-V semiconductors is clearly evidenced in inversion regime, which leads to low capacitance values in C-V characteristics.

Figures 4 and5 show the I-V curves of the structures related to figures 2 and 3, respectively. The gate current curves in double-layer gate stacks with Ge substrate (figure 4) show very low values principally due to a large physical thickness of high-κ layer (HfO 2 and Al 2 O 3 ), which strongly reduces the tunneling current. The gate current in experimental devices (not shown here) seems to be higher probably due to different additional conduction mechanisms, such as trapassisted conduction in the high-κ layer (which is not taken into account in our simulation code). However, we observe that the conduction band offset between the two oxide layers is one of the main parameters influencing the gate leakage tunneling current. Indeed, the conduction band offset between Al 2 O 3 and GeO 2 is higher than the case between HfO 2 and GeO 2 [18], which leads to higher gate current for Al 2 O 3 /GeO 2 structure. We also show in figure 5 (the gate current of structures of figure 3 is plotted) that the substrate material is also crucial to reduce the gate current. In other words, semiconductors with very low bandgap (InAs or InSb) give high currents (besides we do not take into account band-to-band tunneling, which will additionally increase the current) whereas GaAs and InP seems to be very promising substrate materials in terms of low leakage current.

1,E-10 In order to study the influence of oxide material parameters, we now present results concerning MIM capacitors using a full quantum-mechanical calculation (NEGF formalism). Figure 6 compares the tunneling transmission probability through the gate stack between NEGF and WKB calculations for a double-layer gate stack [SiO 2 (6 Å) + HfO 2 (20.5 Å)]. We can observe that classical (WKB) and quantum (NEGF) calculation lead to significant differences between the two transmission curves due to strong potential discontinuities (metal/insulator and insulator/insulator band offset) [16]. The quantum reflections are clearly revealed when the energy-resolved LDOS is plotted (insert of figure 6). The LDOS structure presents a subband energy splitting similar to those corresponding to a quantum well, formed by the barrier discontinuities at the insulator boundaries. The peaks in the transmission probability correspond to a resonant tunneling condition due to a reinforced DOS at the considered energy levels [16,17].

1,E-09 1,E-08 1,E-07 1,E-06 1,E-05 1,E-04 1,E-03 1,E-02 1,E-01 1,E+00 1,E+01 1,E+02 1,E+03 1,E+04 1,E+05 1,E+06 0 1 2 3 Gate current density (A/cm 2 ) Gate Voltage V G (V) HfO 2 /GeO 2 /p-Ge Al 2 O 3 /GeO 2 /p-Ge
We finally plot, in figure 7, the evolution of gate current density as a function of EOT for different MIM structures at V G = 1 V. From these results, we clearly see that the gate current depends on several parameters such as oxide band offsets or dielectric constants. The best way to reduce the leakage current seems to be using dielectric materials with a high permittivity value and a very low band offset between the high-κ and interfacial layers. One can also observe that simulated double-layer gate stacks always give better results than the single SiO 2 layer.

CONCLUSION

We developed a 1D numerical simulation code for the calculation of the C-V and I-V characteristics of MOS devices with high-µ materials and high-κ gate stack. The code selfconsistently solves the Schrödinger and Poisson equations and the resulting quantum carrier density in the substrate is used to calculate the capacitance of the structure. The electron transport through the gate stack is treated using the NEGF formalism. Comparison with C-V experimental data shows that the code can be used to extract the value of key parameters in MOS structures with arbitrary multi layer high-κ gate stacks. Simulation of I-V characteristics reveals that gate leakage current strongly depends on gate stacks and substrate materials. These results also predict promising performances in terms of low leakage current confirming the possibility of enhancing CMOS performances with high-µ materials and high-κ gate stacks.

Figure 1 .

 1 Figure 1. Schematic band diagram of a MOS structure (p-type semiconductor) for V G > 0 and the main physical parameters used in the simulation (listed in TableI). The discretization of the 1D structure using a uniform mesh in oxides and nonuniform mesh in semiconductor is also represented.

Figure 2 .

 2 Figure 2. Comparison between experimental data [3] (symbol) and simulated (line) C-V curves for HfO 2 /GeO 2 /p-Ge (black, Φ M = 4.83 eV) and Al 2 O 3 /GeO 2 /p-Ge (red, Φ M = 4.50 eV) MOS structures (N A = 10 17 cm -3 , T HfO2 = T Al2O3 = 4.0 nm, T GeO2 = 1.4 nm).

Figure 3 .

 3 Figure 3. Simulated C-V characteristics for five different III-V p-doped semiconductors (N A = 10 17 cm -3 ) with an Al 2 O 3 gate dielectric layer of 2.3 nm (EOT = 1.0 nm) and Φ M = 5 eV (fixed for all structures).

Figure 4 .

 4 Figure 4. Simulated I-V characteristics for the same devices as figure 2.

Figure 5 .

 5 Figure 5. Simulated I-V characteristics for the same devices as figure 3. In this figure, V FB is fixed at 0 V for all structures.

Figure 6 .

 6 Figure 6. Carrier transmission probability calculated using WKB and NEGF formalisms as a function of energy in MIM capacitor with a double-layer gate stack SiO 2 (6 Å) + HfO 2 (20.5 Å). The insert show energyresolved LDOS and energy band diagram.

Figure 7 .

 7 Figure 7. Calculation of gate current density (NEGF formalism) vs EOT for different MIM devices [SiO 2 , SiO 2 or GeO 2 + HfO 2 (long dash), SiO 2 or GeO 2 + Al 2 O 3 (short dash)] with T SiO2 = 6 Å or T GeO2 = 10 Å in double-layer gate stacks at V G = 1 V.

ACKNOWLEDGMENTS

This work was supported by the CNRS International Project of Scientific Collaboration (PICS) between IM2NP, Marseille, France and IMEC, Leuven, Belgium.