Pierre-Yves Strub

Coq Modulo Theory

Coq Modulo Theory (CoqMT) is an extension of the Coq proof assistant incorporating, in its computational mechanism, validity entailment for user-defined first-order equational theories. Such a mechanism strictly enriches the system (more terms are typable), eases the use of dependent types and provides more automation during the development of proofs.

CoqMT improves over the Calculus of Congruent Inductive Constructions by getting rid of various restrictions and simplifying the type-checking algorithm and the integration of first-order decision procedures. We present here CoqMT, and outline its meta-theoretical study. We also give a brief description of our CoqMT implementation.

Introduction

Theorem provers like Coq [START_REF]Coq-Development-Team: The Coq Proof Assistant Reference Manual -Version 8[END_REF] based on the Curry-Howard isomorphism enjoy a mechanism which incorporates computations within deductions. This allows replacing the proof of a proposition by the proof of an equivalent proposition obtained from the former thanks to possibly complex computations. Adding more power to this mechanism leads to a calculus which is more expressive (more terms are typable), which provides more automation (more deduction steps are hidden in computations) and eases the use of dependent data types in proof development.

Coq was initially based on the Calculus of Constructions (CC) of Coquand and Huet [START_REF] Coquand | The Calculus of Constructions[END_REF], which is an impredicative type theory incorporating polymorphism, dependent types and type constructors. At that time, computations were restricted to β-reduction: other forms of computations were encoded as deductions.

The Calculus of Inductive Constructions of Coquand and Paulin [START_REF] Coquand | Inductively defined types[END_REF][START_REF] Werner | Une Théorie des Constructions Inductives[END_REF][START_REF] Giménez | Structural recursive definitions in type theory[END_REF] introduced inductive types and their associated elimination rules. CIC allows for example the definition of Peano natural numbers based on the two constructors 0 and S along with the ability to define addition by induction: x + 0 → x and x + S(y) → S(x + y). This mechanism allows the system to identify the expressions x + S(S(y)) and S(x + y) + S(0), but fails in identifying x + S(y) and S(x) + y. This forbids users to easily define functions on dependent data-types (like the reverse function on lists) as the types list(n + 1) and list(1 + n) will not be convertible either.

In the 90's, new attempts to incorporate user-defined computations as rewrite rules were carried out. This resulted in the definition of the Calculus of Algebraic Constructions [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF]. By introducing the correct rewriting rules, the calculus is able to identify terms like x + S(y) and S(x) + y. Although quite powerful (CAC captures CIC [START_REF] Blanqui | Inductive types in the calculus of algebraic constructions[END_REF]), this paradigm does not yet fulfill all needs, as it fails to identify open terms like x + y and y + x.

Further steps in the direction of integrating first-order theories into the Calculus of Constructions are Stehr's Open Calculus of Constructions (OCC) [START_REF] Stehr | The Open Calculus of Constructions: An equational type theory with dependent types for programming, specification, and interactive theorem proving (part I and II)[END_REF] and Oury's Extensional Calculus of Constructions (ECC) [START_REF] Oury | Extensionality in the calculus of constructions[END_REF]. OCC allows the use of an arbitrary equational theory in conversion. ECC can be seen as a particular case of OCC in which all provable equalities can be used in conversion, which can also be achieved by adding the extensionality and Streicher's axiom [START_REF] Hofmann | The groupoid model refutes uniqueness of identity proofs[END_REF] to CIC, hence the name of this calculus. Unfortunately, strong normalization and decidability of type checking are lost in ECC and OCC.

In a preliminary work, we designed a new, rather restrictive framework, the Calculus of Congruent Constructions, which incorporates the congruence closure algorithm [START_REF] Nelson | Fast decision procedures based on congruence closure[END_REF] in CC's conversion, while preserving the good properties of the calculus. We then defined the Calculus of Inductive Congruence Constructions (CCIC [START_REF] Blanqui | Building decision procedures in the calculus of inductive constructions[END_REF][START_REF] Strub | Type Theory and Decision Procedures[END_REF]), which was our first answer to the problem of incorporating validity entailment of an equational first-order theory T in the computation mechanism of the Calculus of Inductive Constructions. This calculus partially solved the problem but contained too many ad-hoc restrictions to be implementable in practice. In particular, the procedure could not be invoked to solve goals occurring below eliminators.

Problem. The main question investigated in this paper is the incorporation of a general mechanism invoking a decision procedure for solving conversiongoals of the form Γ ⇒ U = V in the Calculus of Inductive Constructions which uses the relevant information available from the current context Γ of the proof. This mechanism should be simple enough to be implementable in practice.

Theoretical contribution. Our theoretical contribution is the definition and the meta-theoretical study of a new version of the Calculus of Congruent

Inductive Constructions (called CoqMT). Not only is the new formulation much simpler, but we succeeded in addition to remove most ad-hoc restrictions of CCIC. In particular, conversion now contains the entire equational theory T . We show that we keep all the desired properties of such a calculus: subject reduction, strong normalization of reduction, logical consistency and decidability of type-checking.

Practical contribution. We implemented CoqMT, a new version of Coq based on the Calculus of Inductive Congruent Constructions. We also formally defined our calculus in Coq, and started its formal meta-theoretical study. 2We assume the reader familiar with typed λ-calculus [START_REF] Barendregt | Lambda calculi with types[END_REF] and rewriting [START_REF] Dershowitz | Rewrite systems[END_REF]. Due to the lack of space, we restrict our presentation to the Calculus of Constructions with two inductive types, natural numbers and lists depending on their size. The only embedded theory is the theory of Presburger arithmetic. This version captures all technical and theoretical problems encountered in the development of the full version of the calculus.

From now on, T designates the first-order theory of Presburger arithmetic, built from the function symbols 0, S and + and on the equality predicate =. By extension, we write T for the set of first-order terms belonging to the theory T . If

E = {t 1 = u 1 , . . . , t n = u n } is a finite set of equations in T (or T -equations) and t = u is a T -equation, we write T , E t = u if t 1 = u 1 ∧ • • • ∧ t n = u n ⇒ t = u is a valid formula in T .

Syntax and notations

Definition 1 (Terms). The set of CoqMT pseudo-terms is defined by: t, u, T, U, . . .

::= s ∈ { , } | x ∈ X | f ∈ Σ | •[t : e T ]. u | u v | λ[x : e? U ]. v | ∀(x : e? U ). V | Elim(t : Q){f 0 , f S } | = | refl T (t)
where Σ = {0, S, +, nil, cons, nat, list}, e denotes an extracted equation, a notion to be explained later. The notation e? denotes either an extracted equation e or the symbol ⊥. To ease the reading, we allow us to omit the ⊥ symbol.

Pseudo-terms of CoqMT are made of the usual terms of the Calculus of Constructions: variables, sorts, abstraction λ[x : U ]. v, dependent product ∀(x : U ). V . Binders can be optionally decorated with an extracted equation e. For dealing with equalities and natural numbers, the following symbols are added: nat is the type of natural numbers, whereas 0, S and + are resp. the zero, successor and addition symbols. Similarly, = is the (dependent) equality predicate ( = T t 1 t 2 or t 1 =T t 2 denotes that t 1 and t 2 are two equal terms of type T ), while refl T (t) denotes the proof by reflexivity of t =T t. Also, to illustrate the use of integrating Presburger arithmetic in CoqMT, we add symbols for dealing with dependent lists: list is the type of dependent lists, whereas nil and cons are its constructors. The construction Elim(t : Q){f 0 , f S } denotes the usual recursor for natural numbers. Its semantic is detailed later when defining the reduction relation of our calculus.

A major novelty of CoqMT is the new symbol We still need to clarify what is an extracted equation. As our calculus will incorporate the validity entailment of T in its conversion along with T -equations extracted from the environment, we first need a process to convert CoqMT terms into T terms: this is called algebraisation. For CoqMT terms containing only symbols relative to nat and variables, algebraisation is simply the process of currying symbols: from S x + 0, we can extract the T -term S(x) + 0 -note the font change. Unfortunately, due to substitution occurring in β-reduction, extracting only this kind of terms is not sufficient. Indeed, when substituting x by a arbitrary term t in the previous example, we first abstract t in the expression S t + 0 by a fresh variable (say y), and then do the algebraisation. Here, we obtain the T -term S(y) + 0 with y abstracting t.

Definition 2 (Algebraic context). A context is said algebraic if it is of the form C

A ::= 0 | S C A | • n + • p | • n ,

Definition 3 (Pre-algebraic term). A pseudo-term

t is pre-algebraic if it is of the form C A [1 ← t 1 , . . . , n ← t n ].
If none of the t i 's are pre-algebraic, we say that C A is the maximal algebraic cap of t and {t 1 , . . . , t n } are the aliens of t.

For example, the term (S t) + u is pre-algebraic. We can take

• 1 + • 2 as algebraic context with the instantiation [1 ← S t, 2 ← u].
This context is not maximal. Assuming t and u not headed by a symbol of T (and hence not being pre-algebraic), (S • 1 ) + • 2 is the maximal algebraic cap of (S t) + u, and t, u are its two aliens.One can remark that a pseudo-term has exactly one maximal algebraic cap and the set of aliens is uniquely defined. Note that we consider the variables of a CoqMT term as aliens.

Definition 4 (Algebraisation). For any term t, an algebraisation of t is a pair (C, I) s.t. t = C[I].

If C is the maximal algebraic cap of t, we say that (C, I) is the maximal algebraisation of t.

Definition 5 (Extracted equation). An extracted equation is a

4-tuple (C 1 , C 2 , I 1 , I 2 ) (written (C 1 = C 2 , I 1 , I 2 )) s.t. C 1 and C 2 are algebraic context and I 1 , I 2 are context instantiations. For example, (• 1 + • 2 = 0, [1 ← t, 2 ← u], []) is an extracted equation.
By replacing holes with fresh variables and currying, we obtain the T -equation x + y = 0 which can be used in a conversion check. Context instantiations allows us to related the extracted equations to CoqMT types: the extracted equation

(• 1 + • 2 = 0, [1 ← t, 2 ← u], []) will be extractable from a CoqMT term T if and only if T is of the form (• 1 + • 2 )[1 ← t, 2 ← u] = 0[] i.e. of the form t + u = 0.
When extracted equations are pure, i.e. the instantiations fill holes with variables only, we simplify our notations by giving the instantiated extracted equations instead of the 4-tuple. For example, we write x + 0 = S 0 for the extracted equation (

• 1 + 0 = S 0, [1 ← x], []).
Definition 6 (Substitution). We denote by tθ with θ = {x ← w} the term obtained by substituting in t all free occurrences of x by w -including the term appearing in the extracted equations:

f θ = f sθ = f ( = θ) = ( =) xθ = w yθ = y when x = y (•[t : e T ]. u)θ = •[tθ : eθ T θ]. uθ (u v)θ = (uθ) (vθ) (λ[x : e? U ]. v)θ = λ[x : e?θ U θ]. vθ (∀(x : e? U ). v)θ = ∀(x : e?θ U θ). vθ (Elim(t : Q){f 0 , f S })θ = Elim(tθ : Qθ){f 0 θ, f S θ} (refl T (t))θ = refl T θ (tθ) (C 1 = C 2 , I, J )θ = (C 1 = C 2 , Iθ, J θ) ⊥ θ =⊥ [i ← t i ]θ = [i ← t i θ]
Regarding variables capture, we here assume the Barendregt convention.

Notation 1. By { #» t i } 1≤i≤n , or simply #» t , we denote the terms t 1 t 2 • • • t n .
We write T → e? U for ∀(x : e? T ). U when x is not free in T . When using sequences, we write for the empty sequence and x :: xs for the cons operation. The notation [x 1 , x 2 , . . . , x n ] denotes x 1 :: x 2 :: • • • :: .

Converting terms

Our conversion relation is split in two parts. The first part is a rewriting relation → βιT , which includes β-reduction and the Martin-Löf recursor reduction for natural numbers, so called ι-reduction. Our reduction → βιT differs from the standard → βι by its ability to operate modulo the theory T . For example, the term Elim((x + (S 0)) + y : Q){f 0 , f S }, which is head-normal for → βι , is head-reducible for → βιT . Actually, our definition of → βιT is such that Elim((x + (S 0)) + y : Q){f 0 , f S } (resp. Elim(S (x + y) : Q){f 0 , f S }) → βιThead-reduces (resp. → βι -head-reduces) to the same term f S (x + y) Elim(x + y : Q){f 0 , f S }. The second part of our conversion relation is the extension of the validity entailment of T , E to the set of CoqMT pseudo-terms, where E is a set of extracted equations. We call this the T -congruence relation. This Tcongruence will be parametrized by its ability to use the equations in E or not. We write ≡ E for the T -congruence having the ability to use the equations of E, and ≡ ⊥ E for the other one. For example, if from E we can use the equation x = (S 0), ≡ E will be such that x + x ≡ E (S (S 0)), whereas x + x and S (S 0) will not be convertible using ≡ ⊥ E . We start with the definition of the reduction relation → βιT . (From now on, for ease of notations, we write → for → βιT ) We achieve the reduction modulo by applying a normalization function to terms being in deconstruction position [START_REF] Courtieu | Normalized types[END_REF][START_REF] Petcher | Deciding joinability modulo ground equations in operational type theory[END_REF]. For that, we introduce a function norm T normalizing first-order T -terms as found in Shostak's method for combining decision procedures [START_REF] Shostak | An efficient decision procedure for arithmetic with function symbols[END_REF]:

1. T t = norm T (t),
2. the variables of norm T (t) appear in t, 3. norm T is involutive, 4. sub-terms of a normalized term are normalized.

We lift the norm T function to pre-algebraic terms as follows:

Definition 7 (T -normalization). Let t = C[I] a CoqMT term with maximal algebraic context C, and I = [1 ← t 1 , . . . , n ← t n ]. Let J = [1 ← x 1 , . . . , n ←
x n ] where all the x i 's are pairwise different, and not free in the t i 's. The Tnormalization of t, written norm(t), is defined as:

norm(t) = norm T (t[J ]){x 1 → t 1 } • • • {x n → t n }.
For example, assuming norm((x + S(0)) + y) = S(x + y), then norm((u + (S 0)) + u ) = S (u + u ). We could have defined a stronger normalization function in which sub-expressions are abstracted by the same variable when they are in the same equivalence class of the conversion relation of the calculus. This would have lead to a mutual definition of normalization, rewriting and conversion, a possibility explored in an unpublished work with a heavy price. We now have all the ingredients for defining our reduction relation:

Definition 8 (Reduction). The rewriting relation → is the smallest relation stable by context and substitution s.t.:

(β) (•[ # » w : e W ]. λ[x : U ]. v) u → •[ # » w : e W ]. v{x ← u} (ι 0 ) Elim(t : Q){f 0 , f S } → f 0 if t is pre-algebraic, and norm(t) = 0 (β-E) (•[ # » w : e W ]. λ[x : e U ]. v) u → •[ # » w : e W ]. •[u : e U ]. v{x ← u} (ι S ) Elim(t : Q){f 0 , f S } → f S v Elim(v : Q){f 0 , f S } if t is pre-algebraic,
(•[ # » w : e W ]. λ[x : U ]. v) u → • •[ # » w : e W ]. ((λ[x : U ]. v) u) (1) → β •[ # » w : e W ]. v{x ← u} (2)
where reduction (1) is the action of moving the bullet expression hiding the βredex, whereas reduction (2) is the standard β-reduction. This remark applies to (β-E) also. Rule (β-E) has an additional role: the introduction of an equation marker as is clear for its instance (λ[x : This problem already appeared in [START_REF] Strub | Type Theory and Decision Procedures[END_REF], and was solved by forbidding the application of annotated λ-abstractions to other terms. At that time, we thought the problem could be by-passed by locking such problematic β-redexes. Although our calculus is more general than a calculus where problematic β-redexes are locked (the latter can be easily encoded in the former), its study is much easier: locking β-redexes leads to normal terms containing β-redexes, and hence the standard proof of consistency based on cut elimination does not apply anymore.

e U ]. v) u → •[u : e U ].
The two last rules deal with reduction of Martin-Löf like recursors. Usual reduction rules for elimination of nat are:

Elim(0 : Q){f 0 , f S } → f 0 Elim(S t : Q){f 0 , f S } → f S t Elim(t : Q){f 0 , f S }
As said, reduction is done modulo the theory T through the use of norm. For example, the term Elim((x + (S 0)) + y : Q){f 0 , f S } which is normal for the standard ι-reduction will reduce to f 0 using ι 0 , as norm((x + (S 0)) + y) = S(x + y). Reduction also contains the recursor rules for lists which are identical to the corresponding ones in the Calculus of Inductive Constructions, and do not play any critical role in our definition.

Notation 2. We write

≤ -→, * -→, *
←→ for resp. the reflexive, reflexive-transitive and equivalence closure of →. We write t→ ↓ u if t has a unique normal form equal to u.

We move now to the definition of our conversion relation. We start explaining how T -validity entailment makes use of pre-algebraic terms and extracted equations, via the notion of (T , E)-consequence. Let us assume the following two extracted equations of z 1 + z 2 = 1 and S(z 3 ) = 1 are the two extracted equations of E where holes are replaced by pairwise disjoint fresh variables. Hence, z 1 (resp. z 2 and z 3 ) abstracts t (resp. u and t ), from t * ←→ t (resp. u * ←→ u ), we add the equation z 1 = z 3 (resp. z 2 = z 4 ) to the set of available equations, via the set V. x + z 4 = S(x) (the conclusion of the T -entailment) is the algebraisation of x + u = S x.

E: i) (• 1 + • 2 = S 0, [1 ← t, 2 ← u], []),
We now describe formally the notion of (T , E)-consequence. Let {J i } 1≤i≤n be a set of instantiations and V a set of equations between variables. We say that {J i } i abstracts {(C i , I i )} i accordingly to V and R if:

1. for any i ∈ {1..n}, k, J i associates a fresh variable x i,k to the k th hole of C i , 2. (x i,p = x j,q ) ∈ V implies t i,p R t j,q Definition 10 ((T , E)-consequence).

Let E = [(C l i = C r i , I l i , I r i ) | 1 ≤ i ≤ n
] be a sequence of extracted equations, and t, u two CoqMT terms of the form C l 0 [I l 0 ] and C r 0 [I r 0 ] respectively. Let R be any binary relation on CoqMT terms. We say that (t = u) is a (T , E)-consequence modulo R if there exists a set {J α i } i,α of context instantiations and a set V of equations between variables s.t.

1. T , {C l i [J l i ] = C r i [J r i ]}, V C l 0 [J l 0 ] = C r 0 [J r 0 ], 2. {J α i } i,α abstracts {(C α i , I α i )} i,α accordingly to V and R.
We introduce two variants of conversion: a strong one which can use the equations of E, and a weak one which cannot. Doing this is crucial for the logical consistency proof of our calculus in the presence of strong recursors (i.e. construction of types by induction). Assume the function f (n) := Elim(n :

Q){nat, λ[ : nat]. λ[T : ]. T → nat}, i.e. a function s.t. f (n) = n times nat → • • • → nat.
If we allow the use of any equation in the conversion of n of f (n), for example the equation 0 = S 0, then f (0) would be convertible to f (1) which respectively →-reduce to nat and nat → nat. Having nat convertible to nat → nat would then allows us to type-check the term (λ[x : nat]. x x) (λ[x : nat]. x x), which is not strongly-normalizing.

Restricting conversion under recursors is not enough: let A = (λ[x : nat]. f (x)) t, in which f is defined as above. If we allow t to be convertible to 0 and S 0, since A → β f (t), we are back to the previous example. We called strong such problematic terms. Of course, we want a syntactic characterization of non-strong terms. The following lemma gives one which is convenient for its use in the context of dependent data types: Lemma 1. Terms headed by constructor and inductive symbols (hence 0, S, nil, cons, list) are non-strong. We call them weak.

We now define the T -congruence ≡ b E :

Definition 11. The T -congruence ≡ b E , b ∈ { , ⊥} is given in Figure 1.
The T -congruence is defined as follows. First, our notion of (T , E)consequence is included through the [Ded] rules. In the case of a weak conversion, the [Ded ⊥ ] rule does not use extracted equations, and uses the empty relation for aliens comparison. The rules [•], [Lam], [Elim] and [Prod] are congruence rules. Of course, when crossing a binder annotated with an extracted equation, the set of available equations must be updated (this was already the case in [START_REF] Strub | Type Theory and Decision Procedures[END_REF]). Note also that in the definition of conversion for recursors, the term in deconstructing position can only be converted using weak conversion. There

[Refl] t ≡ b E t [Trans] t1 ≡ b E t2 t2 ≡ b E t3 t1 ≡ b E t3 [AppW ] t, u are weak terms t ≡ E u ∀i, ti ≡ E ui t t1 • • • tn ≡ E u u1 • • • un [AppS ] ∀i, ti ≡ ⊥ E ui t1 • • • tn ≡ b E u1 • • • un [Lam] U ≡ b E U v ≡ b E v λ[x : U ]. v ≡ b E λ[x : U ]. v [Prod] U ≡ b E U v ≡ b E v ∀(x : U ). v ≡ b E ∀(x : U ). v [Lam-E] U ≡ b E U v ≡ b e::E v e ≡ b E e λ[x : e U ]. v ≡ b E λ[x : e U ]. v [Prod-E] U ≡ b E U v ≡ b e::E v e ≡ b E e ∀(x : e U ). v ≡ b E ∀(x : e U ). v [•] t ≡ b E t T ≡ b E T U ≡ b e::E U e ≡ b E e •[t : e T ]. U ≡ b E •[t : e T ]. U [Eq] ∀i, ti ≡ b E ui ∀i, t i ≡ b E u i e1 = (C = C , [i ← ti], [i ← t i ]) e2 = (C = C , [i ← ui], [i ← u i ]) e1 ≡ b E e2 [Ded ] t = u is a (T , E)-consequence modulo * ←→ • ≡ b E • * ←→ t ≡ E u [Ded ⊥ ] t = u is a (T , ∅)-consequence modulo the empty relation t ≡ ⊥ E u [Elim] t ≡ ⊥ E t Q ≡ b E Q f0 ≡ b E f 0 fS ≡ b E f S Elim(t : Q){ #» f } ≡ b E Elim(t : Q ){ #» f }

CoqMT typing

Contrary to our previous calculus [START_REF] Strub | Type Theory and Decision Procedures[END_REF], extracted equations are now directly accessible via annotations. Although this greatly simplifies the definition of the calculus by removing the CCIC complex notion of extraction, one must verify some consistency properties between the extracted equations and the terms which are annotated with. For example, from the term x = S t, one wants x = S y to be a valid extractable equation (with y abstracting t), but not x = 0. Allowing the extraction of x = 0 from x = S t would allow users to prove x = S t and x = 0 without the use of any assumptions, thus leading to a non-consistent system.

Definition 12 (E-extractability).

Let (C 1 = C 2 , I, J ) be an extracted equation and T a term. We say that e is extractable from

T if T is convertible, using ∼ E , to C 1 [I] = C 2 [J ].
Before defining our typing judgment, we are left to define our typing environments. As usual, typing environments bind variables to types, but with two modifications. First, as for λ-expressions and dependent products, bindings can be optionally annotated with extracted equations. Second, typing environments will also contain equation markers.

Definition 13 (Typing environment). The set of typing environments is defined by Γ, ∆

::= | Γ, [x : e? T ] | Γ, •[t : e? T ].
Definition 14 (Typing judgement). For any environment Γ , let ∼ Γ defined as ∼ E where E is the set of all extractable equations appearing in Γ . Typing rules of CoqMT are given in Figure 2.

The rules for = and nat symbols are identical to the ones of CIC -for lack of space, we omit the rules for lists. Several modifications are made to the pure Calculus of Constructions rules. First, when adding to a typing environment Γ a new binding annotated by an extracted equation e (rules [Weak], [Weak-•] and [Var]), we check that e is indeed extractable, hence making sure that we do not extract inconsistent equations from a consistent typing environment.

Moreover, the rule for application has been duplicated, as for β-reduction. For the two rules, we allow the left hand-side to have a product type modulo the presence of equation markers. This is for the non-interference of reduction as discussed before and is very similar to the equation markers we found in the (β) and (β-E) in the definition of → rules. The second one, [App-E], handles the case where a term annotated by an equation is applied. As for the (β-E) rule which handles the case where an extracted equation annotating a λ-abstraction has disappeared, [App-E] handles the case of for dependent products with the very same technique.

We also add two rules for typing equation markers. One is a weakening style rule and allows the user to add extracted equations to the environment. The second allows markers to be moved from terms and types to the environment.

The conversion rule is of course updated to use the relation ∼ Γ .

Meta-theoretical properties

The meta-theory of our calculus is carried out in a similar way as that of CC or CIC. As usual, the logical consistency is proved in three steps. First, we prove the subject reduction property stating that the reduction relation is correct w.r.t. typing: if Γ t : T and t → t , then Γ t : T . In the second step, we prove that the reduction relation is strongly normalizing for well-typed terms. In the last step, we prove that there exists a term which is non-typable in the empty environment.

[Sort]

: [Var] Γ T : s x ∈ dom(Γ ) e? is extractable from T Γ, [x : e? T ] x : T [Weak] x ∈ dom(Γ ) e? is extractable from V Γ t : T Γ V : s Γ, [x : e? V ] t : T [Weak-•] x ∈ dom(Γ ) e is extractable from T Γ t : T Γ u : U Γ, •[t : e T ] u : U [App] Γ u : U Γ t : •[ # » t : e T ]. ∀(x : U ). V Γ t u : •[ # » t : e T ]. V {x ← u} [App-E] Γ u : U Γ t : •[ # » t : e T ]. ∀(x : e U ). V Γ t u : •[ # » t : e T ]. •[u : e U ]. V {x ← u} [Lam] Γ, [x : e? U ] v : V Γ ∀(x : e? U ). V : s Γ λ[x : e? U ]. v : ∀(x : e? U ). V [Prod] Γ U : s1 Γ, [x : e? U ] V : s2 Γ ∀(x : e? U ). V : s2 [•] e is extractable from T Γ, •[t : e T ] u : U Γ t : T Γ •[t : e T ]. u : •[t : e T ]. U [Conv] Γ t : T Γ U : s T ∼Γ U Γ t : U [0] 0 : nat [S] S : nat → nat [+] +: nat → nat → nat [nat] nat : [Refl] Γ t : T Γ reflT (t) : t =T t [Eq] Γ =: ∀(T : ). T → T → [Elim]

Subject reduction

The subject reduction proof requires the following property:

∀(x : e U ). V ∼ E ∀(x : e U ). V ⇒ U ∼ E U ∧ V ∼ e::E ∧e ∼ E e
called product compatibility [START_REF] Barbanera | Modularity of strong normalization and confluence in the algebraic-lambda-cube[END_REF]. Usually, conversion coincides with the closure by equivalence of reduction, and product compatibility is then an immediate consequence of the confluence property of reduction. In CCIC, product compatibility was obtained via a complex sequence of definitions and lemmas. It is much simpler here. The proof is structured as follows.

We first prove confluence of →. The proof follows the method of Tait for β-reduction [START_REF] Barendregt | The Lambda Calculus. Its Syntax and Semantics[END_REF]: we define a parallel reduction ⇒ s.t. (→ * ) = (⇒ * ), and prove its confluence as in Tait's proof. Let us give the definition for the case of (ι 0 ) reduction: Elim(t : Q){f 0 , f S } ⇒ f 0 if t ⇒ t , f 0 ⇒ f 0 and norm(t ) = 0. We then prove the key property of T -congruence, called coherence in [START_REF] Jouannaud | Completion of a set of rules modulo a set of equations[END_REF] Such a property is crucially based on the fact that our reduction is done modulo the theory. For example, the term Elim((x + (S 0)) + y : Q){f 0 , f S } is convertible to Elim(S (x + y) : Q){f 0 , f S } and reducible using the (ι S ) rule. Thanks to the use of the norm function, we can conclude that 3a), and then that ∼ E is transitive (i.e. * -→ • ≡ E • * ← -is transitive -see Figure 3b). Product compatibility for ∼ * E is then reduced to the product compatibility of ∼ E , which itself is reduced to the product compatibility of → and ≡ b E , two properties which are immediate.

∼ E is equal to * -→ • ≡ E • * ← -(See Figure

Strong normalization

In [START_REF] Strub | Type Theory and Decision Procedures[END_REF], we prove strong normalization of CCIC by an embedding into a variation of the Calculus of Algebraic Constructions [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF][START_REF] Blanqui | Inductive types in the calculus of algebraic constructions[END_REF]. Due to the use of reduction modulo, this is no more possible. Proof of strong normalization of → is now obtained by adapting the proof for CIC to our calculus, which is based on Coquand and Gallier's extension to the Calculus of Constructions of Tait and Girard's computability predicate technique. The idea is to define an interpretation for each type and to prove that each well-typed term belongs to the interpretation of its type. The main difficulty is to define the interpretation for type constructed by induction. For the case of natural number, the CIC interpretation of Elim(t :

Q){f 0 , f S } is the one of f 0 if t→ ↓ 0 the one of f S u Elim(u : Q){f 0, f S } if t→ ↓ S u

an arbitrary value otherwise

We simply adapt this definition by modifying the condition t→ ↓ 0 (resp. t→ ↓ S u) by t→ ↓ u with norm(u) = 0 (resp. t→ ↓ v with norm(v) = S u). The rest of the proof is the same. The interpretation of the equation marker •[t : e T ]. U is that of U . From strong normalization, we then deduce consistency as usual, by proving that there is no normal proof of false in the empty environment: Theorem 1. If Γ t : T , then t is strongly normalizable. Hence, there is no proof of 0 = S 0 in the empty environment.

Here, the choice of 0 = S 0 follows from the fact that ¬(0 ∼ S 0). (Remember that is the empty sequence)

Decidability

Decidability is split in two parts. First, assuming decidability of the conversion relation, we shows decidability of the typing judgement. We define a syntax oriented (hence decidable) relation

Γ i t : T s.t. if Γ t : T then Γ i t : T with T ∼ * Γ T .
The definition of i is usually done by removing the conversion rule from [Conv] and integrating it in the rules for application (See Figure 4). All this is routine.

[App] (On the other hand, our initial formulation eased the meta-theoretical study) Finally, using again the key lemma used for subject reduction, we can prove that CoqMT conversion can be decomposed in a reduction phase followed by a T -congruence phase: Lemma 3. Let t and u be two strongly normalized terms and E a set of extracted equations composed only of strongly normalized terms. Then t ∼ E u if and only if t ↓ ≡ b E ↓ u ↓ -where w ↓ is the normal form of w Theorem 2. The conversion ∼ is decidable on strongly normalizing terms.

Γ u : U U ∼Γ U Γ t : •[ # » t : e T ]. ∀(x : U ). V Γ t u : •[ # » t : e T ]. V {x ← u} [App-E] Γ u : U U ∼Γ U Γ t : •[ # » t : e T ]. ∀(x : e U ). V Γ t u : •[ # » t : e T ]. •[u : e U ]. V {x ← u}

Implementation

A new version of Coq based on this work, called CoqMT, is available on the author's website 3 . CoqMT allows a user to dynamically load any decision procedure for a first-order theory in the conversion of the system. It does not implement yet the mechanism of equations extraction. Full commented examples can be found in the source release of CoqMT (/test-suite/dp/* ).

Conclusions and future work

We have defined a new version of the Calculus of Congruent Inductive Constructions, called CoqMT, allowing the use of decision procedures in its conversion rule.

We drastically simplified the definition of CCIC, notably by removing almost all ad-hoc restrictions introduced in [START_REF] Strub | Type Theory and Decision Procedures[END_REF]. In particular, based on this, a formal proof of CoqMT in Coq is in development. As of today, an implementation of CoqMT allowing the use of decision procedures in the conversion rule is available. The implementation of the extraction mechanism is to be released soon. More details, along with all sources, can be found on the author's page. We now discuss interesting extension of this work.

We expect to remove the presence of equation markers in types by the use of sub-typing. In our work, non-interference of equation markers has only be addressed, in an ad-hoc manner, for β-reduction and typing of application. Extending this ad-hoc method to all constructions of the calculus would lead to an over-complicated definition. Introducing sub-typing s.t. •[t : e T ]. A is a subtype of A could lead to a calculus where a term of type ∀(x : A). B is applicable to a term of type •[t : e T ]. A for free.

Reduction modulo theory T does not use any extracted equation so that inconsistencies at the extracted equations level do not break logical consistency. A work-around would be to only use, during reduction, a subset of extracted equations which is consistent by construction. Although the idea is quite straightforward, due to the high dependency between weak and strong conversion, reduction modulo and consistency of extracted equation, we have not yet succeeded to obtain a workable definition. We hope solving this problem in a near future.

The link between first order theories and Coq symbols is a one-to-one mapping: each first-order symbol is mapped to a Coq constructor. We want to add a notion of view to break this restriction. This would allow e.g. to map Presburger arithmetic to a Coq binary representation of natural numbers. This could be extended to view dependent data-types as first order data-types with constraints. For example, assuming we embed the first-order theories of lists along with Presburger arithmetic in CoqMT, Coq dependent lists could be viewed by the theories as standard lists plus arithmetical constraints on their lengths.

Finally, we want to extend the extraction from equations to arbitrary firstorder propositions (like ordering on natural numbers), or even add the ability to extract first-order formulas.

Acknowledgment: we thank Gilles Barthe and Jean-Pierre Jouannaud for useful discussions.

  and norm(t) = S v Rule (β) (resp. (β -E) could have been split in two more basic actions:

  v{x ← u}. Equation markers are essential for the subject reduction property: consider for example the term (λ[p : x=0 T ]. refl(x)) t. Being a proof of reflexivity, refl(x) has type x = x. Using the extracted equation x = 0, our conversion rule should allow us to derive [x : nat][p : x=0 T ] refl(x) : x = 0, and hence [x : nat] (λ[x : x=0 T ]. refl(x)) t : x = 0 as well. Without the introduction of equation markers, β-reduction would yield (λ[x : x=0 T ]. refl(x)) t → β refl(x) of type x = x which is not convertible to x = 0 anymore since the equation x = 0 has been lost. Adding the equation marker (•[t : x=0 T ]. ) at root position solves the problem by reintroducing the extracted equation x = 0.

  and ii) (S • 1 = S 0, [1 ← t ], []); with t * ←→ t . Then, for any u s.t. u * ←→ u , we say that x + u = S x is a (T , E)-consequence modulo * ←→ as the entailment T , z 1 +z 2 = 1, S(z 3 ) = 1, V x+z 4 = S(x) holds, taking V = {z 1 = z 3 , z 2 = z 4 }:

Fig. 1 :

 1 Fig. 1: CoqMT T -congruence relation are two rules for application. As explained, applications headed with a weak term can be converted using strong conversion. Otherwise, weak conversion must be used. Finally, the rule [Eq] is used to convert extracted equations: two extracted equations are convertible if they contain the same algebraic cap and have pairwise convertible aliens. The conversion ∼ E of CoqMT, w.r.t. a set E of extracted equations, is simply defined as ( * ←→ • ≡ E • * ←→).

Γ t :Fig. 2 :

 2 Fig. 2: CoqMT typing relation

Fig. 3 :

 3 Fig. 3: Transitivity of → -(C) is application of confluence, and (K) of our key lemma

Fig. 4 :

 4 Fig. 4: Application rule for i

  •[t : e T ]. u, called extracted equation marker or simply equation marker. It aims at carrying the equation e available for conversion -the terms t and T being present for typing purposes. Definitions to come ensure that this construction does not interfere with reduction: if substituting u in a term creates redexes, substituting •[t : e T ]. u in the same term should create the same kind of redexes at the same positions.

  and not reduced to • n , where • n denotes a hole with index n ∈ N. By convention, two different holes in a context cannot have the same index. If C A is an algebraic context whose maximal holes index is n, we write C A [1 ← t 1 , . . . , n ← t n ] the term obtained by replacing the i th hole of C A by t i . We call context instantiation the construct [1 ← t 1 , . . . , n ← t n ], and denote by the letters I, J instantiation variables. A pre-algebraic term is simply a term which can be obtained by instantiation of an algebraic context.

:

  Lemma 2. For any terms t, u, and set of extracted equation E, if t ≡ b E u and t → t , then there exists a term u s.t. u

	≤ -→ u and t ≡ b E u .

This work was partly supported by the ANR ANR-08-BLAN-0326-01

This development is available at http://strub.nu/research/coqmt/

http://pierre-yves.strub.nu/research/coqmt/


L&echaniz-Laguna Dupuis

potential pathogenic role, skeletal muscle pathophysiological events might be

Lowermotorneuron(LMN)degenerationoccursinseveraldiseasesthataffectpatients fromneonatestoelderlyandcaneitherbegeneticallytransmittedoroccursporadically. AmongdiseasesinvolvingLMNdegeneration,spinalmuscularatrophy(SMA)andspinal bulbarmuscularatrophy(Kennedy'sdisease,SBMA)arepuregeneticdiseaseslinkedto loss of the SMN gene (SMA) or expansion of a polyglutamine tract in the androgen receptorgene(SBMA)whileamyotrophiclateralsclerosis(ALS)caneitherbeofgenetic originoroccursporadically.Inthisreview,ouraimistoputforwardthehypothesisthat muscle fiber atrophy and weakness might not be a simple collateral damage of LMN degeneration,butinsteadthatmusclefibersmaybethesiteofcrucialpathogenicevents inthesediseases.InSMA,theSMNgenewasshowntoberequiredformusclestructure and strength as well as for neuromuscular junction formation, and a subset of SMA patients develop myopathic pathology. In SBMA, the occurence of myopathic histopathologyinpatientsandanimalmodels,alongwithneuromuscularphenotypeof animalmodelsexpressingtheandrogenreceptorinmuscleonlyhasleadtotheproposal

1) Introduction: lower motor neuron degeneration affects first neuromuscularjunctions

Voluntary locomotion is governed by motor units, composed of lower motor neurons (LMNs) (alpha-motor neurons) that innervate skeletal muscle fibers and control their (Kennedy'sdisease,SBMA) [START_REF] Katsuno | Pathogenesis, animal models and therapeutics in spinal and bulbar muscular atrophy (sbma)[END_REF]andamyotrophiclateralsclerosis(ALS) [START_REF] Brooks | Natural history of amyotrophic lateral sclerosis[END_REF].

During LMN degeneration, NMJs are progressively destroyed, leading to fully denervated muscle fibers and neurogenic figures in histopathology. The figure 1 presents typical histopathological and electrophysiological results obtained in patients afflicted with a LMN degeneration. One is able to observe that muscle fibers of these patients display spontaneous denervation activities as judged in electromyography (figure 1A). Histopathology shows the occurence of small grouped, angulated fibers (figure 1B-D). It is thought that reinnervation of muscle fibers by the same motor neuron leads to these grouped fibers. NMJ destruction during LMN degeneration is associatedwiththedegenerationoflowermotorneuroncellbodies,hencetheirname andawidelyacceptedparadigmwasthatLMNdeathwasthecauseofNMJdestruction inthesepathologies.Indeed,muscledenervationbynervetransectionleadstoroughly similar histopathological figures, suggesting that in LMN degeneration, the same cause (disruption of the nerve to muscle communication) leads to the same consequence (muscle denervation). However, recent histopathological evidences suggest that Dupuis,L&Echaniz-Laguna,A 4/4 grouped atrophic fibers are highly homogenous in type in polyneuropathies, but heterogenousinLMNdegeneration [START_REF] Baloh | Frequent atrophic groups with mixed-type myofibers is distinctive to motor neuron syndromes[END_REF].Thereasonforthisdyscrepancyisunknown,but might indeed reflect profound differences in the mechanisms of denervation/reinnervationbetweenpurelydenervatingdiseasesanddiseaseswithLMN degeneration.

Inthisreview,wewouldliketoputforwardthehypothesisthatmusclefibersmightnot bethecollateraldamagesofLMNdegeneration,butrather,oneoftheirmurderers.For this,wewillfirstdescribehowmuscleisinvolvedinthepatterninganddevelopmentof fully functional NMJs and how muscle participates in the pathology of ALS, SBMA and SMA.Wewillalsogiveinsightsintohowdrugsmighttargetmusclepathophysiological events or target motor neurons but be delivered through muscles to treat LMN degeneration.

2) Muscleandmotorneuron:apeertopeerdialogtoestablishneuromuscular junctions

The establishment of neuromuscular synapses is a highly controlled developmental event. Motor axons, emerging from the embryonic spinal cord, contact newly formed myofibers around E13. It was long known that motor neurons and muscles are interdependantfortheirdevelopment.Indeed,duringdevelopment,motorneuronsdie if deprived of their target muscle [START_REF] Henderson | Motoneuron survival factors: Biological roles and therapeutic potential[END_REF][6][START_REF] Hendersonce | Neurotrophins promote motor neuron survivalandarepresentinembryoniclimbbud[END_REF][START_REF] Henderson | Denervation increases a neuritepromotingactivityinextractsofskeletalmuscle[END_REF]. Conversely, muscle development is arrested in the absence of motor neurons. A neurocentric view of the development of NMJs long prevailed and postulated that this process was mainly driven by motor neurons, with musclefibersbeingpassiveplayersofNMJdevelopment.Indeed,motorneuronssecrete averyactiveisoformoftheglycoproteinagrin(neuralagrin),thatissufficienttocluster nicotinic acetylcholine receptors on the myofiber [9, 10] through a complex receptor pathway involving the tyrosine kinase Musk and a co-receptor LRP4 [START_REF] Zhangb | MeiL:Lrp4servesasacoreceptorof agrin[END_REF][START_REF] Kimn | BurdenSJ:Lrp4isareceptorforagrinandformsacomplexwithmusk[END_REF]. In this model,thepresenceofagrinsecretedbythenerveissufficienttoclusterAchRandform

NMJs. However, in the absence of nerves, clusters of nicotinic acetylcholine receptors still form in the correct , central, region of the developping muscle [START_REF] Lin | Distinct roles of nerveandmuscleinpostsynapticdifferentiationoftheneuromuscularsynapse[END_REF][START_REF] Yang | Patterning of muscle acetylcholine receptor gene expression in the absence of motor innervation[END_REF]. Moreover, diaphragmmusclesfromE14embryosculturedinthepresenceofrecombinantagrinas wellasmusclesfromtransgenicmiceoverexpressingaminiaturisedformofagrininthe whole muscle fiber retain the formation of AchR clusters in their central region [START_REF] Lin | The role of nerve-versus musclederived factors in mammalian neuromuscular junction formation[END_REF].

Conversely,thetransientmuscleoverexpressionofaconstitutivelyactiveformofErbB2

widened the zone of AchR transcription and of the region where NMJs formed [START_REF] Vock | Evidence for muscle-dependent neuromuscularsynapticsitedeterminationinmammals[END_REF].

Altogether, these data show that the site where NMJs form in skeletal muscle is prepatterned by muscle cells, independantly of nerve derived cues such as agrin. In the current model, NMJs thus form through a dialog between muscle and motor neurons, muscle driving the zone where NMJs will form and neurons strengthening the newly formedcontactsbythesecretionofagrin.

ThispathwayofNMJdevelopmenthasbeenlargelystudiedinthecontextofcongenital myasthenic syndromes in which mutations in Musk [START_REF] Chevessierf | Towardsthemolecular Dupuis,L&Echaniz-Laguna,A 29/29 elucidation of congenital myasthenic syndromes: Identification of mutations in musk[END_REF], or more recently in agrin [START_REF] Huze | Identification of an agrin mutation that causes congenital myasthenia and affects synapsefunction[END_REF] werefound.Uptonow,thereisnodocumentedassociationbetweenthispathwayand LMN degeneration. However, it is striking to note that a mutation in Musk, when introduced in knockin mice, not only leads to the full phenotypic spectrum of myasthenic syndrome, but also to denervation of endplates and molecular features of denervation [START_REF] Chevessier | A mouse model for congenital myasthenic syndrome due to musk mutations reveals defects in structure and function of neuromuscular junctions[END_REF].Inlinewiththis,therecentlydescribedmutationinagrininapatient with congenital myastheniav [START_REF] Huze | Identification of an agrin mutation that causes congenital myasthenia and affects synapsefunction[END_REF] leads to not only to post-synaptic defects but also to pre-synapticpathologysuggestingthattheAgrin/Muskpathwaymightalsobeinvolved inthemaintenanceofNMJsinadultsand,thuspotentiallyinLMNdegeneration.

3) Musclepathogenicroleinspinalmuscularatrophy

3-1) spinalmuscularatrophy

Childhoodspinalmuscularatrophy(hereaftercalledspinalmuscularatrophy,SMA)isa child-onset motor neuron disease involving mutations in the survival of motor neuron gene [START_REF] Lefebvre | Identificationandcharacterizationofaspinal muscularatrophy-determininggene[END_REF].SMApatientsaredividedinthreeclinicalgroupsaccordingtotheseverityof Inthehumangenome,theSMNgeneisduplicatedwithahighlyhomologouscopycalled

SMN2.BothSMNandSMN2genesareexpressedandonlyfivenucleotidesaredifferent

between both genes. We showed that even the promoter sequences and activities of these two genes were strikingly similar [START_REF] Echaniz-Lagunaa | MelkiJ:Thepromotersofthesurvival motorneurongene(smn)anditscopy(smnc)sharecommonregulatoryelements[END_REF]. Importantly, only SMN1 deletions cause SMA,whileupto5%ofindividualsarelackingtheSMN2gene.Thesubtledifferencein nucleotide sequence between SMN1 and 2 has no effect on the encoded open reading frame but profound effects on SMN2 splicing. Indeed, one of the nucleotides divergent betweenSMN1andSMN2createsanewsplicingsiteinSMN2mRNAbyskippingexon7.

Thus,theSMN1geneproducesexclusivelyfulllengthfullyfunctionaltranscripts,while thetranscriptsderivedfromSMN2lackexon7.Mostimportantly,theamountofSMN2

protein are strikingly invertly correlated with the clinical severity of disease [START_REF] Lefebvre | The role of the smn gene in proximalspinalmuscularatrophy[END_REF][START_REF] Lefebvres | Correlation between severity and smn protein level in spinal muscular atrophy[END_REF],

suggesting that SMN2 is a modifying gene in SMA. Thus, SMA is caused by SMN1 mutation and the severity of the disease is linked to the potential compensation by SMN2 protein products. That SMA is caused by the lack of full-length SMN proteins is largely substantiated by the evidence that ablating specifically the exon 7 in motor neuronsleadtomotorneurondegenerationinmice [START_REF] Cifuentes-Diazc | Deletion of murine smn exon 7 directed to skeletal muscle leads to severe musculardystrophy[END_REF][START_REF] Cifuentes-Diaz | Neurofilament accumulation at the motor endplate andlackofaxonalsproutinginaspinalmuscularatrophymousemodel[END_REF][START_REF] Frugiert | Nuclear targeting defect of smn lacking the c-terminus in a mouse model of spinalmuscularatrophy[END_REF].

3-2) ahousekeepingfunctionforSMNprotein?

WhatisthefunctionofSMN,lostinSMA,thatmightleadtomotorneurondegeneration? SMNformsalargemultiproteincomplexwithatleast7otherproteins(calledgemins) both inthecytoplasmandinthenucleuswhereitisconcentrated inastructurecalled gems (for "gemini of coiled bodies"), associated with Cajal bodies[27]. This complex including SMN and gemins appears crucial for the biogenesis of small nuclear ribonucleoprotein particles (snRNPs) [START_REF] Fischer | The smn-sip1 complex has an essential role in spliceosomalsnrnpbiogenesis[END_REF][START_REF] Liuq | DreyfussG:Thespinalmuscularatrophydiseasegene product,smn,anditsassociatedproteinsip1areinacomplexwithspliceosomalsnrnp proteins[END_REF][START_REF] Meister | FischerU:Smnrpisanessentialpre-mrnasplicingfactorrequiredfortheformationof thematurespliceosome[END_REF] that are involved in the splicing of pre-mRNA.ConsistentwithakeyroleinRNAmetabolism,theablationofexon7ofSMNin eithermuscleorneuronleadstostrongup-regulationofanumberofgenesinvolvedin pre-mRNA splicing, ribosomal RNA processing, or RNA decay [START_REF] Olaso | Activationofrnametabolism-relatedgenesinmousebutnothumantissuesdeficientin smn[END_REF]. Furthermore, a recent study used exon microarray in SMA mice and observed widely distributed splicing defects in numerous mRNAs [START_REF] Zhangz | DreyfussG:Smndeficiency causestissue-specificperturbationsintherepertoireofsnrnasandwidespreaddefects insplicing[END_REF]. Interestingly, while splicing defects were prominentlyobservedinallthetissuesstudied,thegenesthatwereabnormalyspliced were different between tissues, suggesting that the selectivity of SMA for the neuromuscularsystemisexplainedbytissuespecificalterationsinmRNAsplicing.

Dupuis,L&Echaniz-Laguna,A 7/7

3-3) SMNisrequiredformusclefunction TheSMNproteinisubiquitouslyexpressedandthetissuespecificablationofSMNleads to drastic alterations in the physiology of the targeted tisue [START_REF] Cifuentes-Diazc | Deletion of murine smn exon 7 directed to skeletal muscle leads to severe musculardystrophy[END_REF][START_REF] Cifuentes-Diaz | Neurofilament accumulation at the motor endplate andlackofaxonalsproutinginaspinalmuscularatrophymousemodel[END_REF][START_REF] Frugiert | Nuclear targeting defect of smn lacking the c-terminus in a mouse model of spinalmuscularatrophy[END_REF][START_REF] Vittejm | MelkiJ:Deletionofmurinesmnexon7directedtoliverleadsto Dupuis,L&Echaniz-Laguna,A 30/30 severe defect of liver development associated with iron overload[END_REF]. A number of studieshaveconvincinglyshownthatSMNexpressionwasrequiredformusclestructure and function. In vitro, Shafey and collaborators demonstrated that SMN knockdown in C2C12 myoblasts lead to decreased myoblast proliferation and impaired myotube fusion [START_REF] Shafey | Hypomorphic smn knockdown c2c12 myoblasts reveal intrinsic defects in myoblast fusion and myotube morphology[END_REF]. Consistently, in vivo, exon 7 ablation of the SMN gene in mouse skeletal muscle leads to a massive muscle dystrophy and death of the animals [START_REF] Cifuentes-Diazc | Deletion of murine smn exon 7 directed to skeletal muscle leads to severe musculardystrophy[END_REF] and RNAi knockdownofSMNindrosophilamusclesisletalindrosophilainamuchmoresevere waythanneuronalknockdown [START_REF] Chang | Modeling spinal muscular atrophyindrosophila[END_REF].Thesestudieswereallbasedontheknock-downor knock-out of the SMN gene, a situation much more drastic of what occurs in real pathological situations. Their relevance for the human pathology is however strengthenedbytheworkofArnoldandcollaborators [START_REF] Arnold | Reduced expression of nicotinic achrs in myotubes from spinal muscular atrophyipatients[END_REF]thathadpreviouslyobserved decreased proliferation and impaired fusion of type I SMA myoblasts. More recently, Martínez-Hernández and collaborators showed that myotubes of fetuses affected with type I SMA were smaller and with abnormal arrangements suggesting delayed developmentalmaturation [START_REF] Martinez-Hernandezr | The developmental pattern of myotubes in spinal muscular atrophy indicatesprenataldelayofmusclematuration[END_REF].Importantly,aboutaquarterofSMAtype3arereported

to have a dystrophic phenotype with high serum creatine kinase (CK) levels and "myopathic"histopathology [START_REF] Muqitmm | Phenotypicvariabilityinsiblingswithtype iiispinalmuscularatrophy[END_REF].Thus,SMNisrequiredfornormalmusclestructureand developmenteitherinexperimentalsituationsorinSMApatients.

The function of SMN in muscle is likely to be related to sarcomeric structure. In drosophila bearing an hypomorphic allele of SMN, Rajendra and collaborators in 2007observedaseveredisorganizationofmusclefilamentsassociatedwithdecreased actinexpression [START_REF] Rajendra | A drosophilamelanogastermodelofspinalmuscularatrophyrevealsafunctionforsmnin striatedmuscle[END_REF].Indeed,SMNhypomorphdisplayedasimilarphenotypethanflies withablationofonemuscleisoformofactin.TheseauthorssuggestedafunctionforSMN in sarcomere formation since both endogenous and transgenic SMN localized to the sarcomeric region of fly muscle. Such a function was further suggested by the work of Walker and collaborators [START_REF] Walker | Smn complexlocalizestothesarcomericz-discandisaproteolytictargetofcalpain[END_REF]. Indeed, not only SMN, but also its associated proteins localize to the sarcomeric Z-disc in both cardiac and skeletal myofibrils of the mouse.

This localization of the SMN complex appeared independent of its role in pre-mRNA splicingsincesnRNPsthemselveswerenotfoundinthesarcomere.SMAmutantmuscles exhibit numerous morphological defects, including vacuoles and altered Z-disc spacing

3-4) SMAisadevelopmentalpathologyofNMJs

Recent evidence suggest that the SMA pathology begins at NMJs. Indeed, Kariya and collaboratorsusedsevere-andmild-SMN2expressingmousemodelsofSMAaswellas material from human patients to understand the initial stages of neurodegeneration in thehumandisease [START_REF] Kariya | Reduced smn protein impairs maturation of the neuromuscularjunctionsinmousemodelsofspinalmuscularatrophy[END_REF].Inthesestudies,theearliestdefects appearattheNMJ.Indeed, lack of SMN protein lead to the failure of post-natal development of the NMJ. In particular, NMJs of SMA mice showed impaired maturation of acetylcholine receptor (AChR) clusters into 'pretzels' that were reflected in functional deficits at the NMJ characterized by intermittent neurotransmission failures. Similar results were also reportedbyKongandcollaboratorswhichobservedimmaturityofNMJsinSMAmiceas assessed for instance by persistance of embryonic gene expression, reduced postsynaptic apparatus and electrophysiological abnormalities [START_REF] Kongl | Impaired synaptic vesicle release and immaturity of neuromuscular junctionsinspinalmuscularatrophymice[END_REF]. Importantly, the pre-synapticpathologyofsevereSMAmiceisdissociatedfromthepost-synapticpathology, suggestingthatbotheventsmightbeindependent [START_REF] Murray | Selective vulnerability of motor neurons and dissociation of pre-and post-synaptic pathologyattheneuromuscularjunctioninmousemodelsofspinalmuscularatrophy[END_REF].Thesedataareindeedconsistent with earlier studies showing reduced expression of AchR genes in SMA myocytes [START_REF] Arnold | Reduced expression of nicotinic achrs in myotubes from spinal muscular atrophyipatients[END_REF].

Altogether,SMAshouldnowbeviewedasadevelopmentalNMJsynaptopathy

3-5) SMAasaglobalneuromuscularpathology

GiventhatSMNhasacrucialfunctioninmuscle,andthatSMApathologyisinitiatedat theneuromuscularsynapse,onecouldhypothesizethatSMAisindeedamuscledisease spreading to the motor neuron. Indeed, muscle knockdown of SMN leads to a more drastic phenotype than neuronal knockdown in Drosophila [START_REF] Chang | Modeling spinal muscular atrophyindrosophila[END_REF]. This is however not true in all animal models, since SMN ablation is partially rescued by neuronal but not Dupuis,L&Echaniz-Laguna,A 9/9 muscle transgenic expression in the nematode [START_REF] Briese | Deletion of smn-1, the caenorhabditis elegans ortholog of the spinal muscularatrophygene,resultsinlocomotordysfunctionandreducedlifespan[END_REF]. Furthermore, overexpression of SMNinskeletalmusclesdidnotallowtherescueofthephenotypeofsevereSMAmice, whileamorewidespreadoverexpressionincludinghighlevelsinneuronsandlowlevels in muscle strongly alleviated the phenotype of these mice [START_REF] Gavrilinato | BurghesAH:Neuronalsmnexpressioncorrectsspinalmuscular atrophy in severe sma mice while muscle-specific smn expression has no phenotypic effect[END_REF]. However, it should be kept in mind that the transgenic overexpression of SMN2 in these animals might be sufficientonitsowntofullyrescuethemusclephenotype.Inthissituation,oneshould notexpectanevenmoreincreasedsurvivalofthemiceafterincreasingSMNexpression.

Inanycase,thebunchoflitteraturecurrentlyavailablestronglysuggeststhatSMAisa global neuromuscular pathology, involving pathological events in muscle and neurons, andpotentiallyanumberofothercelltypes(figure2). DifferentanimalmodelsofSBMAhavebeengeneratedintherecentyears.Inparticular, expansions of CAG repeats have been introduced in knock-in mice [START_REF] Yu | Androgen-dependent pathology demonstrates myopathic contribution to the kennedy diseasephenotypeinamouseknock-inmodel[END_REF][START_REF] Yu | Abnormalitiesofgermcellmaturationandsertolicellcytoskeletoninandrogenreceptor 113 cag knock-in mice reveal toxic effects of the mutant protein[END_REF][START_REF] Albertellima | RobinsDM:Replacingthemouseandrogen receptorwithhumanallelesdemonstratesglutaminetractlength-dependenteffectson physiologyandtumorigenesisinmice[END_REF] or in transgenic mice [START_REF] Brien | Castration restores function and neurofilament alterations of aged symptomaticmalesinatransgenicmousemodelofspinalandbulbarmuscularatrophy[END_REF][START_REF] Katsuno | Testosterone reduction prevents phenotypic expression in a transgenic mouse model of spinal and bulbar muscular atrophy[END_REF][START_REF] Katsunom | SobueG:Transgenicmousemodelsofspinaland bulbarmuscularatrophy(sbma)[END_REF][START_REF] Katsuno | Leuprorelin rescues polyglutamine-dependent phenotypes in a transgenic mousemodelofspinalandbulbarmuscularatrophy[END_REF]. For instance, male mice with a 113 polyglutamine tract in the Dupuis,L&Echaniz-Laguna,A 10/10 endogenousARdeveloppedanSBMA-likeneuromuscularpathology,withearlymuscle pathology but late spinal cord disease and relatively spared motor neurons. In this mouse model, there was prominent early death of males caused by obstruction of the urinary tract [START_REF] Yu | Androgen-dependent pathology demonstrates myopathic contribution to the kennedy diseasephenotypeinamouseknock-inmodel[END_REF]. Interestingly, affected males display several signs of androgen insensitivity,as commonlyobservedinSBMA.

4) MusclepathogenicroleinKennedy'sdisease

ThephysiologicalfunctionofthemutantproteininSBMAisextremelywelldocumented.

The AR is a transcription factor, whose transcriptional activity is activated by testosterone or dihydrotestosterone [START_REF] Lee | Recent advances in androgen receptor action[END_REF]. After ligand activation, AR drives the expression of its target genes, including key factors for muscle growth, male reproductivefunctionandmalesecondarysexualphenotypes [START_REF] Mooradianad | KorenmanSG:Biologicalactionsofandrogens[END_REF].Thelackoffunctional AR protein leads to testicular feminization and complete infertility in both mice and humans [64,65]. In skeletal muscle, AR is especially required for the maintenance in musclemassandfibertype [START_REF] Ophoffj | VanderschuerenD:Androgensignalinginmyocytescontributes tothemaintenanceofmusclemassandfibertyperegulationbutnottomusclestrength orfatigue[END_REF]aswellasmusclestrengthinmales [START_REF] Macleanhe | Impairedskeletalmuscledevelopmentandfunctioninmale,butnot female,genomicandrogenreceptorknockoutmice[END_REF].

Studiesinanimal modelsindicatethathormonalligandsarecrucial forthedevelopment of SBMA. First, only male transgenic mice develop an SBMA-like phenotype. Second, castration of transgenic males alleviates the phenotype while testosterone-treated females develop the pathology [START_REF] Brien | Castration restores function and neurofilament alterations of aged symptomaticmalesinatransgenicmousemodelofspinalandbulbarmuscularatrophy[END_REF][START_REF] Katsunom | SobueG:Transgenicmousemodelsofspinaland bulbarmuscularatrophy(sbma)[END_REF][START_REF] Katsuno | Leuprorelin rescues polyglutamine-dependent phenotypes in a transgenic mousemodelofspinalandbulbarmuscularatrophy[END_REF]. This is reminiscent of the absence of phenotype of women carriers of SBMA mutations [50,[START_REF] Sobueg | MitsumaT:Subclinical phenotypic expressions in heterozygous females of x-linked recessive bulbospinal neuronopathy[END_REF]. Consistently, a phase 2 clinical trial has recently suggested that androgen deprivation by leuprorelin acetate maybebeneficialtopatients [START_REF] Banno | Phase 2 trial of leuprorelin in patients with spinal and bulbar muscular atrophy[END_REF]Thus,SBMAisduetoatoxicgainoffunctioninmutant ARunmaskedbythepresenceoftheligand.

4-2) MyopathicpathologyinSBMA

Studies in both patients and mice have shown that, apart from lower motor neuron degeneration, SBMA patients display myopathic features. In particular, SBMA patients showedCKelevationinmusclebiopsies [START_REF] Sorarug | Spinal and bulbar muscular atrophy: Skeletal muscle pathologyinmalepatientsandheterozygousfemales[END_REF].Recently,wedescribedafamilywithearly onset and rapidly progressive SBMA mimicking muscle dystrophy [START_REF] Echaniz-Laguna | A family with early-onset and rapidly progressive x-linked spinal and bulbar muscular atrophy[END_REF]. and showed prominent and lethal myotonic discharges [START_REF] Yu | Androgen-dependent pathology demonstrates myopathic contribution to the kennedy diseasephenotypeinamouseknock-inmodel[END_REF]. Thus, while SBMA was considered as a pure motor neuron disorder, recent research reevaluated this notion andshowedthatSBMAisamixedconditioninvolvingnotonlyneurogenicdenervation, butalsomyopathicfeatures.

4-3) AmyogenicoriginforKDrelatedmotorneurondegeneration?

These findings prompted to test the hypothesis that LMN pathology of SBMA patients indeed resulted from a myogenic pathology. This idea is further supported by the crucialroleofARintheskeletalmuscle [START_REF] Mooradianad | KorenmanSG:Biologicalactionsofandrogens[END_REF][64][65]andbytheintriguingobservationthat AR accumulates at NMJs [START_REF] Monks | Androgen receptor immunoreactivity in skeletal muscle: Enrichment at the neuromuscular junction[END_REF]. Indeed, the pathology of animal models of SBMA is primarilymuscular,withbothneurogenicandmyogenicpathologyoccuringlongbefore motor neuron degeneration is observed [START_REF] Yu | Androgen-dependent pathology demonstrates myopathic contribution to the kennedy diseasephenotypeinamouseknock-inmodel[END_REF]. Indeed, in most SBMA animal models, there is no detectable motor neuron degeneration [START_REF] Yu | Androgen-dependent pathology demonstrates myopathic contribution to the kennedy diseasephenotypeinamouseknock-inmodel[END_REF][START_REF] Brien | Castration restores function and neurofilament alterations of aged symptomaticmalesinatransgenicmousemodelofspinalandbulbarmuscularatrophy[END_REF][START_REF] Katsuno | Testosterone reduction prevents phenotypic expression in a transgenic mouse model of spinal and bulbar muscular atrophy[END_REF]. Most importantly, the musclespecificoverexpressionofanon-expandedARleadstoaSBMA-likephenotype.

In this model, the phenotype was androgen dependent, witha pathology strictly affecting males but alleviated by castration [START_REF] Monksda | Overexpression of wild-type androgen receptor in muscle recapitulates polyglutaminedisease[END_REF]. Importantly, mice present with a pathology not restricted to muscle (muscle necrosis) but also show axonal loss and denervationrelatedchangesingeneexpressionbutnotlossofMNcellbodies [START_REF] Monksda | Overexpression of wild-type androgen receptor in muscle recapitulates polyglutaminedisease[END_REF].Last, the pathology did not affect females except when treated with testosterone, and the cessation of testosterone treatment in females allows complete recovery of the phenotype [START_REF] Johansen | Recovery of function in a myogenic mouse model of spinal bulbar muscular atrophy[END_REF]74]. These studies thus provide the convincing proof of principle that SBMA might be a LMN degeneration of muscle origin [74] (figure 3). Further work is neededtodelineatethemechanismslinkingmuscleARandNMJdenervation,aswellas thepathogenicroleofpolyglutamineexpansion.

Dupuis,L&Echaniz-Laguna,A 12/12

5) Musclepathogenicroleinamyotrophiclateralsclerosis

5-1) Amyotrophiclateralsclerosis

Amyotrophic lateral sclerosis (ALS) is the most frequent LMN degeneration of adult onset. ALS worldwide incidence is estimated to be of 1-3 new cases per 100000 individuals, which ranks ALS as the most frequent neurodegenerative disease after Alzheimer's and Parkinson's diseases [START_REF] Brooks | Natural history of amyotrophic lateral sclerosis[END_REF]. [START_REF] Greenwaymj | Ang mutations segregate with familial and 'sporadic' amyotrophic lateral sclerosis[END_REF], vapb [START_REF] Nishimura | A mutation in the vesicletrafficking protein vapb causes late-onset spinal muscular atrophy and amyotrophic lateralsclerosis[END_REF], dynactin [START_REF] Puls | Mutant dynactinin motorneurondisease[END_REF][START_REF] Munchc | LudolphAC:Pointmutationsofthep150subunitofdynactin (dctn1)geneinals[END_REF],

andmorerecentlytdp43[8286],fus [START_REF] Kwiatkowski | Mutations in the fus/tls gene on chromosome 16 cause familial amyotrophic lateral sclerosis[END_REF][START_REF] Ticozzin | Analysis of fus gene mutation in familial amyotrophic lateral sclerosis within an italian cohort[END_REF]andfig4[89]havebeengeneticallylinkedto familial forms of ALS, but how these specific mutations lead to ALS is currently unknown [START_REF] Lagier-Tourenne | Rethinking als: The fus about tdp-43[END_REF].TherecentdescriptionofamousemodeloverexpressingmutantTDP-43

will hopefully lead to new insights in the field [START_REF] Wegorzewskai | BalohRH:Tdp-43mutanttransgenic micedevelopfeaturesofalsandfrontotemporallobardegeneration[END_REF]. On the contrary, the mechanisms underlyingALSlinkedtomutationsinthesod1gene,thefirstandmajorgenelinkedto familialALSin1993,havebeenextensivelystudied[75-77].Itisinterestingtonotethat variations in the SMN1 and 2 genes involved in SMA have been reported to be a risk factorinALSalso [START_REF] Corciap | AndresC:Theimportanceof thesmngenesinthegeneticsofsporadicals[END_REF][START_REF] Corciap | Smn1 gene, but not smn2, is a risk factor for sporadic als[END_REF][START_REF] Corcia | AndresC:Abnormalsmn1genecopynumberisasusceptibilityfactorforamyotrophic lateralsclerosis[END_REF][START_REF] Veldinkjh | Smn genotypes producing less smn protein increasesusceptibilitytoandseverityofsporadicals[END_REF][START_REF] Veldinkjh | Homozygous deletion of the survival motor neuron 2 gene is a prognosticfactorinsporadicals[END_REF][START_REF] Echaniz-Laguna | Homozygous exon 7 deletion of the smn centromeric gene (smn2): A potential susceptibility factor for adult-onset lower motor neuron disease[END_REF]. InSBMA,recentworksuggestedthatthemuscleoverexpressionofAR,evennotbearing an expanded polyglutamine tract could lead to the pathology [START_REF] Monksda | Overexpression of wild-type androgen receptor in muscle recapitulates polyglutaminedisease[END_REF]. Could mSOD1 expression in muscle also lead to such a concept in ALS? Indeed, the transgenic overexpression of mSOD1 was sufficient to induce severe muscle atrophy associated with significant reduction in muscle strength, sarcomere disorganization, significant changes in mitochondria morphology and disposition, and disorganization of the sarcotubular system. The authors involved several signalling pathways, including autophagyandoxidativestressinthedeleteriouseffectsofmusclemSOD1expression.

However,whilemuscle-restrictedmSOD1expressionpromotespinalcordastrocytosis and inflammation, no motor neuron loss was observed. Thus, in this study, muscle Intriguingly,theknock-downofmSOD1inmuscledidnotappeartobesufficienttoslow down the pathology [116,117]. This suggests either that muscle mSOD1 expression is not key in the pathology, or that even the small remaining amounts of mSOD1 in knocked down muscles were sufficient to lead to their toxic effects, or that the knock downoccuredtoolateinanimallifespantoyielditsprotectivepotential.Inall,muscle appears to be one of the sites of mSOD1 toxicity, although it remains elusive whether NMJdestructionisprimarilydrivenbymusclemSOD1expression.

5-5) MuscleenergymetabolismabnormalitiesasacauseofNMJdestruction

WhatcouldbethemechanismsunderlyingmuscletoxicitytomotorneuronsinALS?We In all, skeletal muscle is involved in ALS through an increase in its metabolic rate, precipitating systemic defects in energy homeostasis, such as leanness. Muscle might also directly influence NMJ stability through energy metabolism defects and yet unknownsignallingpathways(figure4).

6) Muscleasadrugtargetinlowermotorneurondiseases

The previous results in either SMA, SBMA or ALS point to muscle being an active contributor to these pathologies. Based on these studies, a number of therapeutic strategieshavebeenproposedtotargetmusclepathology(figure5).

In

8) Conclusion

As a conclusion, when considering all the data discussed above, one may hypothesize thatLMNdegenerationmaybe"synaptopathies"ratherthan«motorneurondiseases».

As such, one should focus on designing treatments to strengthen and stabilize the remaining NMJs and/or to stimulate the generation of newly formed NMJs.

  contraction.MyelinatedaxonsoftheLMNscontactmusclefibersonadiscreteregionof the fiber, highly speciallized, called the neuromuscular junction (NMJ). A number of pathologiestargetthiscriticalregion.First,myasthenicsyndromesaffecttheefficacyof synaptic transmission through either immunological or genetic processes. In these pathologies,theabsolutenumberofNMJsremainroughlythesamebuttheirefficacyto triggeramuscleactionpotentialinresponsetomotorneuronstimulationisdecreased leadingtofatigablemuscleweakness.NMJsarealsoaffectedduringlowermotorneuron degeneration.Inthisreview,wewillfocusonpathologiesinvolvingLMNdegeneration, butsparingsensoryinnervation.Thisgroupofdiseasesaffectspatientsfromneonatesto elderly people and can either be genetically transmitted or occur sporadically in a family.Thetable1summarizestheclinicalfeaturesofthediseaseswewillfocusonin thisreview,namelyspinalmuscularatrophy(SMA)[1],spinalbulbarmuscularatrophy

  4-1) Kennedy'sdiseaseSpinal and bulbar muscular atrophy (SBMA), or Kennedy's disease, is a purely genetic LMNdegenerationcausedbyexpansionofaCAGrepeatinthefirstexonoftheandrogen receptor(AR)gene,leadingtoanARproteinwithanexpandedpolyglutamine(polyQ) tract[START_REF] Spada | Androgen receptor gene mutations in x-linked spinal and bulbar muscular atrophy[END_REF]. Like in other triplet repeat disorder, including Huntington's disease, the disease develops only in individuals bearing an expansion of the polyQ tract over a certainthreshold(>36Gln)andthelengthofthepolyQiscorrelatedwithanumberof clinicalparameters[START_REF] Suzuki | Cag repeat size correlates to electrophysiological motor and sensory phenotypes in sbma[END_REF][START_REF] Rhodesle | Clinical features of spinal andbulbarmuscularatrophy[END_REF].SBMAisanX-linked,genderspecificdiseasesinceonlymale carriers of a pathogenic mutation are affected. The phenotype of females carrying a pathogenicalleleisabsentorverymildevenifhomozygousforanexpandedCAGrepeat[50,[START_REF] Sobueg | MitsumaT:Subclinical phenotypic expressions in heterozygous females of x-linked recessive bulbospinal neuronopathy[END_REF].SBMApatientsdevelopproximalmuscleweakness,fasciculations, andatrophy, alongwithlowermotorneurondegenerationinthebrainstemandspinalcord[START_REF] Katsuno | Pathogenesis, animal models and therapeutics in spinal and bulbar muscular atrophy (sbma)[END_REF][START_REF] Atsutan | Natural history of spinal and bulbar muscular atrophy (sbma): A study of 223japanesepatients[END_REF].A subsetofpatientsalsodisplayadditionalfeatures , associatedwithandrogendysfunction such as androgen insensitivity, oligozoospermia or azoospermia, testicular atrophy, feminizedskinchanges,andgynecomastia[START_REF] Arbizu | A family with adult spinal and bulbar muscular atrophy, x-linked inheritance and associated testicular failure[END_REF][START_REF] Casella | Significance of the polyglutamine tractpolymorphismintheandrogenreceptor[END_REF].

  mSOD1 expression was not sufficient to support full blown ALS[114]. A very recent Dupuis,L&Echaniz-Laguna,A 15/15 studyconfirmedandsignificantlyextendedthisinitialwork.WongandMartincreated transgenic mice overexpressing either wild type or two mutations in the SOD1 cDNA under the control of the skeletal muscle actin promoter[115]. These authors, in a manner consistent with Dobrowolny and collaborators, found important clues for this overexpression triggering localized oxidative stress and subsequent muscle atrophy. Most interestingly, they found NMJ denervation and animals developped paresis and motorneurondegeneration.Inthisstudy,

  haveshownthattheneuriteoutgrowthinhibitorNogo-Aismassivelyexpressedinthe skeletal muscle of mSOD1 mice and ALS patients [118-120]. Importantly, Nogo-A ablationincreasedmSOD1micelifespanwhileitsoverexpressioninmusclefiberslead toNMJshrinkage[119].Thesefindingsprovidetheproofofprinciplethatalterationsin musclegeneexpressionareabletomodulatethediseaseprocessinmSOD1mice. From a more general point of view, our work suggests that abnormalities in muscle energymetabolismmightthedirectcause.Weandothershaveobservedthatmusclesof mSOD1 mice display decreased cellular levels of ATP[121, 122], along with increased expression of mitochondrial uncoupling proteins and of markers of both lipid and carbohydrate use[123, 124]. Indeed, as previously mentioned, mitochondrial dysfunctionoccuredinmusclesofmSOD1mice,and,toalesserextent,inmusclesofALS patients[103].ThesefindingssuggestedthatmusclesofALSpatientsandmSOD1mice Dupuis,L&Echaniz-Laguna,A 16/16 show an exacerbation of their energy metabolism. To determine whether this was sufficienttoleadtomotorneurondegeneration,westudiedtheneuromuscularsystemof mice overexpressing the mitochondrial uncoupling protein 1 in their muscles, as a model of muscle restricted hypermetabolism. These animals displayed age-dependent deterioration of the NMJ that correlated with progressive signs of denervation and a mild late-onset motor neuron pathology[125]. Furthermore, NMJ regeneration and functional recovery were profoundly delayed following injury of the sciatic nerve and crossing these mice with mSOD1 mice exacerbated ALS-like pathology[125]. Thus, a muscle restricted mitochondrial defect is sufficient to generate motor neuron degeneration. 5-5) ALSasasystemicpathology Muscle hypermetabolism of mSOD1 mice has broad consequences on the overall energetic physiology of these animals, and provides clues for a potential therapeutic strategy.Indeed,mSOD1miceshowbodyweightdeficitascomparedtowildtypesdue toanincreaseinthebasalmetabolicrate,asareflectofmusclehypermetabolism[123]. Furthermore,energymetabolism,especiallylipidmetabolism,wasstrikinglyalteredin these animals[126]. We sought to determine whether correcting energy deficit of mSOD1 mice could delay their pathology and fed these mice with a diet enriched in saturated fats. High fat fed mSOD1 mice lived longer and showed reduced muscle denervation associated with improved motor neuron survival, a finding recently confirmedbyMattson'sgroupinanothermSOD1strain[123,127]. ALSpatientsalsoshowabnormalitiesintheirsystemicenergyhomeostasis.Couratier's group has found an increased energy expenditure in these patients, similar to what observed in mSOD1 mice[128-132]. Most importantly, ALS patients show increased blood lipid levels and hyperlipemia was associated with increased survival [133]and betterrespiratorycapacityinthesepatients.However,thetranslationfrommSOD1mice toALSpatientsisnotstraightforwardsincepatientsshowanimportanttrendtobecome insulinresistant[134].Intheseconditions,theincreaseinenergyintake,intheformof an high fat diet, might precipitate insulin resistance and worsen patient outcome. Potential therapeutic strategies based on nutrition should take this trend to insulin resistanceintoaccount. Dupuis,L&Echaniz-Laguna,A 17/17

Figure3

  Figureandlegendstofigures:

Figure5: targetingskeletalmuscleinLMNdegeneration A

 targetingskeletalmuscleinLMNdegeneration Figure5:targetingskeletalmuscleinLMNdegeneration A potential therapeutic treatment for LMN degeneration might target deleterious processesoccuringinmuscleitself.

delivery route to cure motor neurons in lower motor neuron diseases

	7) muscleinjectionsofviralvectorsretrogradelytransportedtomotorneurons.Thismode of delivery achieved what remains probably the most impressive protective effect in Muscle a a WhileskeletalmuscleisinvolvedinatleastsomeofthekeypathogeniceventsinLMN mSOD1 mice. Thus, muscle might not only be a tissue to target, but also a route to
	degeneration,onecouldalsoconsidertousemuscleasawaytotargetmotorneurons deliverdrugsortreatments.
	(figure6).Forinstance,localproductionofneurotrophicfactorsbytheskeletalmuscle
	might sustain neuronal survival and enhance muscle reinnervation. Such an example
	wasprovidedbythestudyofLiandcollaborators[146]showingthatmuscleproduction
	of GDNF, but not astrocyte derived-GDNF delayed disease onset and slowed down
	diseaseprogressionofmSOD1mice.
	SMA mice, treatment with follistatin, an inhibitor of myostatin [135] that increases Inthesameline,retrogradetransportofatherapeuticgenethroughmuscleinjectionsof
	musclemass,wasreportedtolessendiseaseseverityinSMAmice[136]butnotinALS aviruscouldprovideprotectiontomotorneurons.Twodifferentexamplesprovidethe
	mice[116].InSMAmice,butnotinALSmice,follistatin-treated miceperformedbetter proof of concept for such a strategy. First, delivery of IGF1 through AAV vectors in
	thantheirvehicle-treatedlittermates.Themostwidelydocumentedfactorthatcouldbe skeletal muscles leads to protection of motor neurons and delayed disease onset. This
	beneficial in LMN degeneration through a muscle action is IGF1. In 2002, Antonio protective effect might be due to retrograde transport of viral particles in the axon,
	Musaroandcolleaguesgeneratedatransgenicmouselineoverexpressinganisoformof leading to IGF1 production in motor neurons and autocrine protection of these cells.
	IGF1 (termed mIGF1) that is retained locally in skeletal muscle and does not Alternatively, and as suggested by A. Musaro and colleagues, IGF1 has profound local
	systematically diffuse [137]. Crossing these mice with either mSOD1 mice [138] or effects on skeletal muscle that might account for its potential for therapeutics in ALS
	SBMAmice[139]potentlyincreasedthelifespanofbothmodels.InmSOD1mice,mIGF1 [138]. A second example of a therapeutic strategy aiming at delivering a neurotrophic
	expressiondelayedthedisease,enhancedsurvival,stabilizedNMJsandhadalsodistant factor though skeletal muscle is VEGF. M. Azzouz and collaborators used a lentiviral
	protective effects by decreasing astrocytosis[138]. In SBMA mice, mIGF1 increased AR vectortoprovideVEGFdirectlytomotorneuronsthroughretrogradetransport.They
	phosphorylation, promoted the degradation of aggregated AR, rescued the muscle observed that a single injection of a VEGF-expressing lentiviral vector into various
	phenotype,increasedmotorneuroncountsandpotentlyincreasedthelifespanofSBMA muscles delayed onset and slowed progression of in mSOD1 mice[147]. Interestingly,
	mice[139].Thesedatathussuggestthatapharmacologicalinterventionsolelytargeted eitherviraldeliveryofVEGForIGF1sloweddiseaseprogressionevenwhentreatment
	at muscles is able to provide global protection to motor neurons. Indeed, it should be wasinitiatedattheonsetofdisease,suggestingthatthesestrategiesmightberelevant
	noted that the protection mediated by exercise [140-142], high fat feeding[123, 127], inALSpatients.
	creatine[143]orcarnitine[144]inanimalmodelsofLMNdegenerationmightwellbe Viral delivery might prove useful not only for providing a neuroprotective factor, but
	duetoanactionofthesetreatmentsonskeletalmuscleratherthanonmotorneurons. also to restore the causative deficient gene. Indeed, multiple muscular injections of a
	Suchanindirecteffectissuggestedbytheprofoundeffectsofexerciseongenesinvolved lentiviral vector expressing SMN restored SMN expression in motor neurons and
	inNMJmaintenance[145]. delayed the pathology of severe SMA mice [148]. Conversely, similar viral strategies
	might be used to silence the toxic gene when gain of function of the mutant protein is
	showntoleadtothepathogeniceffects.Inthisline,targetingofSOD1mutationsthrough
	siRNA has been achieved by Ralph and collaborators in mSOD1 mice [149] through
	Dupuis,L&Echaniz-Laguna,A Dupuis,L&Echaniz-Laguna,A	18/18 19/19

  Lastly, it should be kept in mind that while skeletal muscle is a much more important actor in LMN degeneration than previously anticipated, these affections target motor neurons and involve other cell types, i.e. astrocytes, schwann cells and microglia[75,[150][151][152][153][154][155][156][157].Anefficienttherapyshouldtakeallthesecellularactorsintoaccount.

	To our
	knowledge,notreatmenthasbeenspecificallydesignedtotargetNMJsinmotorneuron
	diseases until now. It may worth to consider that a drug or treatment targeting the
	commonfinalpathwayofdiseaseswithLMNdegenerationi.e.theNMJ,wouldbeequally
	beneficialforALS,SMAandSBMApatients.

Dupuis,L&Echaniz-Laguna,A 20/20

Dupuis,L&Echaniz-Laguna,A