domain: spi phys math info

text:
Marc Boyer

Pierre Roux

Hugo Daigmorte

Checking validity of the min-plus operations involved in the analysis of a real-time embedded network

Checking validity of the min-plus operations involved in

the analysis of a real-time embedded network

Introduction

Network calculus is a theory widely used in industry to check that a real-time network (like AFDX or TSN) provides guaranteed latency bounds to the real-time data flow [START_REF] Boyer | PEGASE, a robust and efficient tool for worst case network traversal time[END_REF][START_REF] Boyer | Experimental assessment of timing verification techniques for AFDX[END_REF][START_REF] Maile | Network calculus results for tsn: An introduction[END_REF]. When these networks are embedded in a critical system, where faults can lead to severe damages or injuries, a very high level of confidence on these bounds must be provided. Since such bounds are commonly computed by a dedicated tool [START_REF] Zhou | A survey on network calculus tools for network infrastructure in real-time systems[END_REF], the correctness of the bounds depends both on the correctness of the algorithms and the correctness of their implementation.

The correctness of the algorithms is commonly ensured by open publication and peer-reviewing while the correctness of the implementation is mainly ensured by code review and tests. More confidence in the implementation can be insured by developing several pieces of software and comparing on the fly that all programs give the same result. Nevertheless, such approach can not detect an error in the algorithm itself [START_REF] Davis | Controller area network (CAN) schedulability analysis: Refuted, revisited and revised[END_REF]. Using proof assistants, such as Coq or Isabelle/HOL, is a way to increase the confidence in a software: one may prove the correctness of the algorithms and derive an implementation from the proof [START_REF] Letouzey | Extraction in coq: An overview[END_REF]. One may also use a skeptical approach, where the proof assistant is not able to check an algorithm or to compute a result, but still able to check that a result is correct. Indeed, checking a solution is commonly much easier that solving a problem (for example, finding vs checking the roots of a polynomial, the decomposition into prime factors, matrix inversion,...). Of course, this approach can be used only for software used at design: if there is a mistake in the algorithm or a bug in the implementation, it will only be detected at runtime, while a completely proved approach will ensure that the software is conform to its specification. Nevertheless, the skeptical approach often requires significantly less effort.

Network calculus is based on the min-plus dioid theory [START_REF] Bouillard | Deterministic Network Calculus -From theory to practical implementation[END_REF], and analyzing a network involves a lot of operations in this theory (like physics involves a lot of matrix manipulations). In a recent work [START_REF] Rakotomalala | Verifying min-plus computations with coq[END_REF], this skeptical approach has been applied to the min-plus dioid of real functions. This paper shows how this approach can be used in an industrial context.

Network calculus

Network calculus is a theory designed to compute upper bounds on delay an memory usage in networks. Data transiting through the network are called flows. A flow is modeled by cumulative curves at each point in the considered network, A : R + → R + where A(t) represents the cumulative amount of data observed in the flow up to time t at a given point of the network. Possible cumulative curves are specified by envelopes called arrival functions. A flow A satisfies an arrival function α when: ∀t, d ≥ 0 :

A(t + d) -A(t) ≤ α(d).
For instance, a periodic flow sending frames of size L every T time unit admits as arrival curve ν L,T : d → L d T , where • : R + → N is the ceiling function. All network elements are modeled by servers. A nserver S transforms n input flows (A 1 , . . . , A n ) into n output flows (D 1 , . . . , D n ), where all A i and D i are cumulative curves. The performance of these servers is specified by service curves. A n-server S admits a strict service curve β when, for all busy interval (t, t + d], the aggregate output is at least β(d), i.e.,

n i=1 D i (t + d) -D i (t) ≥ β(d).
Among others, a result of network calculus states that, if a server S uses a FIFO policy, if it admits a strict service curve β and each of its incoming flow A i admits as arrival curve a function α i , then the delay experienced by each flow in the server is upper bounded by

hDev n i=1 α i , β (1) with hDev(f, g) = sup t≥0 {inf {d f (t) ≤ g(t + d)}} . (2)
Network calculus also uses other operators, like the the min-plus convolution * and deconvolution , defined by: ∀f, g : R

+ → R + , ∀t ∈ R + , (f * g)(t) = inf 0≤s≤t {f (t -s) + g(s)} , (3)
(f g)(t) = sup s≥0 {f (t + s) -g(s)} . (4)

Related work

To perform actual min-plus computations, one has to settle on a given class of real functions. Two main classes of functions are used in network calculus: the set of concave or convex piecewise linear functions, C[x]PL [START_REF] Sariowan | SCED: A generalized scheduling policy for guaranteeing quality-of-service[END_REF], and the, strictly larger, set of ultimately pseudo-periodic piecewise linear functions, commonly known as UPP [START_REF] Bouillard | An Algorithmic Toolbox for Network Calculus[END_REF]. The data structure and algorithms for the CPL class are so simple that they, to our knowledge, have never been published. Nevertheless, they cannot accurately model packetized traffic, whereas the UPP class gives more precise results at the expense of higher computation times [START_REF] Boyer | PEGASE, a robust and efficient tool for worst case network traversal time[END_REF]. The algorithms of the operators on the UPP class are given in [START_REF] Bouillard | An Algorithmic Toolbox for Network Calculus[END_REF].

An open source implementation of the operators on the C[x]PL class can be found in the DISCO network calculus tool [START_REF] Bondorf | The DiscoDNC v2 -A Comprehensive Tool for Deterministic Network Calculus[END_REF]. An open source implementation of the UPP class has been developed [START_REF] Bouillard | COINC library: a toolbox for the network calculus[END_REF] but is no longer maintained to our knowledge. The Real-Time Calculus toolbox (RTC) does performance analysis of distributed real-time systems [START_REF] Wandeler | Modular performance analysis and interface based design for embedded real time systems[END_REF][START_REF] Wandeler | Real-Time Calculus (RTC) Toolbox[END_REF]. Its kernel implements Variability Characterization Curves (VCC's), a class very close to UPP. None of these implementations has been formally proved correct.

The first work on the formal verification of network calculus computation were presented in [START_REF] Mabille | Towards certifying network calculus[END_REF]. The aim was to verify that a tool was correctly using the network calculus theory. An Isabelle/HOL library was developed, providing the main objects of network calculus and the statement of the main theorems, but not their proofs. They were assumed to be correct, since they have been established in the literature for long. Then, the tool was extended to provide not only a result, but also a proof on how network calculus has been used to produce this result. Then, Isabelle/HOL was in charge of checking the correctness of this proof. The result was taking the form of an algebraic min-plus expression, yet to be computed.

Another piece of work, presented in [START_REF] Rakotomalala | Formal Verification of Real-time Networks[END_REF], consists in proving, in Coq, the network calculus results themselves: building the min-plus dioid of functions, the main objects of network calculus and the main theorems (statements and proofs).

The tool CertiCAN [START_REF] Fradet | Certican: A tool for the coq certification of CAN analysis results[END_REF] is able to produce Coq proofs for some real-time analyses of the CAN protocol. These analyses are not based on the network calculus theory.

The PROSA library also provides proofs of correctness for the response time of real-time systems, but focuses on scheduling tasks for processors [START_REF] Cerqueira | PROSA: A case for readable mechanized schedulability analysis[END_REF].

Existing tools

4.1. RTaW-Pegase. RTaW-Pegase is a proprietary tool written in Java and developed by the company RealTime-at-Work that can provide network analyses and optimization. It can support many technology types and networks such as: automotive, aerospace and industrial Ethernet TSN, CAN (FD,XL), LIN, Arinc as well as wireless networks for off-board communication.

Its first functionality is to model a network, visualize it and set configuration parameters: priorities, offsets, routing, shapers, transmission schedule, preemption,... The graphical interface allows to manipulate the configurations as shown in Figure 1. In this example, the network is made of 5 switches (in blue) and 14 end systems (in orange) and one of the flows is shown, between "CAM1" and "ECU1".

In addition to timing-accurate simulation, RTaW-Pegase can compute guaranteed upper bounds on message delays using a state-of-the-art analysis in network calculus.

RTaW-Pegase can also generate complete traces of its analyses. These traces contain all the computations performed during the analysis in a format both readable by a human and that can be interpreted by an additional RTaW tool, the Network calculus interpreter. Figure 2 shows a simplified example of such a trace. This trace gives the calculations for two periodic flows (Flow1, Flow2) crossing the first link of a network, arbitrated with FIFO policy. The assert expression at last line checks that the computed value is not greater than the value 156/5 computed by RTaW-Pegase.

Thereby, a network calculus expert can read this trace and check that the mathematical operations performed correspond to the result of the network calculus theory. Using the calculation capability of the interpreter, it can perform other computations,

1# ################################ 2# Time u n i t : microsecond 3# Frame s i z e u n i t : b i t 4# ################################ 5# I n p u t f l o w s 6# ################################ 7#
Flow1 e n t e r i n g a t Node1>p o r t -P1 8 Flow1 := s t a i r ( 0 , 1 0 0 0 0 , 1 3 6 0 ) 9 10# Flow2 e n t e r i n g a t Node1>p o r t -P1 11 Flow2 := s t a i r ( 0 , 5 0 0 0 , 1 7 6 0 ) and prove this property. Such a proof is given in Figure 3.

12 13# ################################ 14# EndSystem : Node1>p o r t -P1 15# ################################ 16#
First, one loads our tool Minerve [START_REF] Rakotomalala | Verifying min-plus computations with coq[END_REF] (for MINplus ExpRession VErification) providing a formalization of the UPP class of functions and an automatic proof tactic to check min-plus computations on those functions. The next line simply instructs Coq to interpret all subsequent numeric constants as arbitrary precision rationals.

Then one needs to define the considered UPP functions. The first function Flow1 is, as seen on line 8 of Figure 2, a stair function that is incremented by 1360 every 10000, starting from 0. The second function Flow2 is also a stair function, as seen on line 11 of Figure 2, whereas the third function S Node1 is, still according to Figure 2 (line 26), a linear function of slope 100. These functions are encoded by their period sequpp_d, increment sequpp_c and an initial segment sequpp_T (to allow a specific initial behavior before the regular periodic one) and a list of linear segments following the pattern (x, (y, (ρ, σ))) where (x, y) are the coordinates of the leftmost point of the segment, ρ is its slope and σ its limit on the right of x (discontinuities are allowed on the right of x, as seen for instance on Flow1 where the function is y = 0 at x = 0 and immediately jumps to σ = 1360 just after 0). Not all combinations of parameters are valid. For instance the period must be positive. Such validity of the parameters is checked by the F_of_sequpp function.

Finally, the property to prove is expressed after the Goal keyword and automatically proved by our nccoq tactic [START_REF] Rakotomalala | Verifying min-plus computations with coq[END_REF]. This tactic is a reflexive tactic, which means it makes use of Coq efficient computation capabilities to perform proofs. This is key in getting a very pervasive tactic being entirely developed in Coq. Of course, the proofs automatically performed by the tactic offer the same strong correctness guarantees as any other handmade Coq proof.

It is worth noting the application of the skeptical approach here, the horizontal deviation 156 5 is computed by RTaW-Pegase but only checked with Coq.

Reading the Coq Specification.

To fully trust a Coq proof, one must inspect its statement in order to agree that the proof is indeed proving what the user is expecting. Indeed, whereas Coq can automatically check proofs, it cannot read the user mind to ensure the formal statement match its understanding by the user. in particular, one can see that + was a notation for F plus. One can for instance inspect the latter by asking Coq to print its definition

1 Print F_plus.
and Coq answers

1 F_plus = fun f g : F ⇒ f \+ g
By deactivating printing of notations again, one could see that \+ is the pointwise addition of functions.

Proceeding with such investigations, one can check that hDev_bounded indeed states that the horizontal deviation is bounded and that the definitions of functions introduced with F_of_sequpp perfectly match what one is expecting.

Digging further, one could even look at the definition of the field of real numbers R given by the library we are using.

Checking RTaW-Pegase traces with Minerve

The RTaW-Pegase tool allows to compute upper bounds on the delays on the flows crossing a network. As presented in Section 4.1, the engineer enters into the tool the network description, the flow characteristics, and the tool can apply network calculus to check that the system satisfies its latency requirements. The correctness of these bounds depends on a chain of responsibilities. The first link of the chain is the correctness of the network calculus theorems (for example, the result presented in (1)). In case of mistake in the proof, the confidence in the result collapses. Such issue have been addressed in [START_REF] Rakotomalala | Formal Verification of Real-time Networks[END_REF]. A second link is the correct application of network calculus results by the tool: if the tool applies a result whose hypotheses are not satisfied by the system, the confidence also collapses. The trace generated by the tool, illustrated in Figure 2, has been designed to allow proofreading by a human expert. A formal proof can also be generated [START_REF] Mabille | Towards certifying network calculus[END_REF]. The last link is the exactness of the computation: the basic operations (sum, convolution, deconvolution, hDev...) are too complex to be checked by humans. This is the aim of Minerve, presented in Section 4.2.

The approach presented in the current work boils down to checking that all computations done in a given RTaW-Pegase trace have provided a sound result, i.e., verifying that the transformations of expressions into values have been performed correctly.

But the traces generated by RTaW-Pegase have been designed to be read by a network calculus expert, to increase confidence in the operations, whereas Minerve has been designed for proof simplicity.

To make both tools run together, we had to solve a few issues:

(1) Function syntax: Both tools do not have the same syntax to represent functions. In particular, the domain of the non-periodic part (the initial prefix) of a function in Minerve is always a right open interval [0, T ), whereas it can be open [0, T ) or closed [0, T ] in the syntax of RTaW-Pegase. (2) Single assignment: The RTaW-Pegase trace is a script in an imperative programming language, in which identifiers are variables, whose value can be updated along the script lines. On the opposite, Coq is designed to state mathematical definitions, where a given identifier represents the same value all along the proof. There are several ways to solve this problem, and we have basically chosen to resort on a single static assignment transformation.

(3) Performance tricks: While going from handmade examples, with dozens of operations, to realistic examples with thousands of operations, we faced some performance problems, not related to the core of the algorithms but related to some details in implementations.

5.1. Function syntax. One problems is that, although both tools represent functions as sequences of segments and spots, RTaW-Pegase's input language accepts segments that can be open or closed on both ends, whereas NCCoq always considers a sequence of spots and open segments.

Consider a function f : R + → R + , defined by ( 5)

f (t) = 1 if t ≤ 2, t if t > 2.
In RTaW-Pegase, such a function can be represented as a sequence of two segments, the first one going from point (0,0) to (2,0) with slope 0 (printed as [(0,0)0(2,0)]) and a second one going from (2,2), excluded, up to infinity with slope 1 (then printed as ](2,2)1(+Inf,+Inf)[). In Minerve input, such a function is represented as a sequence of two pairs (spot, open segment), the first one having a spot (0,0) and a segment with origin 0 and slope 0, and the second one having a spot (2,0) and a segment with origin 0 and slope 1. Then, the translation from RTaW-Pegase to Minerve has to split the closed segment into a spot and an open segment, and push the right extremity as a spot of the second segment. Eventually, the translation can be done on a per-segment basis, pushing spots from one segment to another.

A second problem was that RTaW-Pegase may have no periodic part when the function ends with an infinite segment. The transformation into Minerve has to chose an arbitrary period value (we chose 1).

The third problem was that RTaW-Pegase accepts two expressions of the periodicity, whereas Minerve admits only one. In RTaW-Pegase, one may either state that a function is pseudo-periodic when it exists T, d, c such that:

∀t > T, f (t + d) = f (t) + c or: ∀t ≥ T, f (t + d) = f (t) + c,
whereas Minerve only knows about the latter definition. Both conditions are equally expressive, but one has to increase the value of T in order to cast a definition from the former format into the latter one.

Consider, for instance, the function

g : t → max t + 1, t 2
plotted in Figure 4. In RTaW-Pegase, it can be represented by a the closed first segment [(0, 2) -1/2(2, 0)] followed by the left-open segment ](2, 1)0(4, 0)] repeated with periodicity 2 and increment 1, as shown in the upper part of Figure 4. In Minerve, such a representation is impossible, and one has to extend the non-periodic prefix, as illustrated in the lower part of Figure 4.

Static Single assignment.

Looking at the trace presented in Figure 2, the correctness of the trace relies on a correct computation of the variable cumA Node. But since this variable is assigned three times in the trace, there is no single value to check. We may consider the line number of the expression as a tie-breaker, but it is somehow fragile. Then, RTaW-Pegase can generate an enhanced trace, augmented with comments giving an number identifier to each expression to check. This enhanced trace also contains as assertions the expected values of the operands and results for each operation. For instance, the line 20 in the listing of Figure 2 is replaced by the set of lines presented in Figure 5.2.

Performance tricks.

Going from simple hand-made examples, with dozens of operations, to realistic examples with thousands of operations, we encountered some performance issues, not related to the core of the algorithms but related to some details in implementations. We sum them up here.

In a first version of the files we used Let instead of Definition. While this was apparently inocuous with only a few occurrences, this became a major issue with hundreds or thousands of occurences as this means the terms computed by Coq for the last check was embedding all previous definitions, dramatically slowing down computations. Replacing the keyword Let by Definition was enough to fix the issue. As a first step, our automatic tactic nccoq maps each min-plus operation, like + or * introduced in Section 2, on arbitrary functions to effective operators on UPP functions, our tactic uses the typeclass resolution mechanism of Coq. This mechanism can perform exponential searches and is known to easily lead to serious slow downs. After doing some profiling, we discovered that more time was spent in this resolution than actually performing the computation of the reflexive tactic. Putting the definitions of the sequences sequpp_js in a separate definition (they were originally inlined) solved the issue by enabling the type class search procedure of Coq to find the expected solution much earlier.

Finally, the largest computations first appeared much slower than expected. Inspecting the intermediate values computed, we discovered rational numbers such as 17498164897827×10 5000 38753975857×10 5000 . Further investigation revealed that we were using non normalizing operations on arbitrary precision rational numbers. Replacing them with the normalizing operations solved the issue.

In Minerve, all functions are periodic with a given period (c.f. d in Figure 4). For affine functions, this means that an arbitrary period must be chosen. A bad choice can be an issue when computing an operator whose operands have wildly diferent periods. To avoid such issues, a preprocessing was added to change the (fake) period of affine functions in accordance to the period of the other operand before any binary operation.

When performing a proof with Coq, the proof is first elaborated with tactics (everything between Proof and Qed) then rechecked by the kernel of Coq at Qed time. This means any expensive computation performed by the tactics will be performed a second time by the Qed. To avoid such duplications, a trick using the abstract tactic of Coq is used 1 .

Benchmarks

We evaluated our approach on three midsize to large case studies representative of actual industrial use cases.

The first case study, is a medium size network made of 8 end systems and 2 switches. It is crossed by 57 flows, each having 1 to 5 receivers. The links data rate is set to 100Mb/s except for the link between the two switches which is at 1000Mb/s. For the service policy used, all the flows are distributed between 5 priority levels, at the same level of priority flows respect the FIFO rule. The analysis of such a network with RTaW-Pegase as well as the writing of the trace takes about 1 second.

In the second and third case studies, the considered network is much larger. Comprising 104 end systems and 8 switches, it is crossed by a thousand flows. The links data rate is set to 100Mb/s. For the second case study, all the flows have the same level of priority and are processed in a single FIFO queue. For the third case study, the flows are now distributed in different priority levels and are processed by 5 FIFO 1 This tactic basically seals a computation into an auxiliary lemma (with its own Qed), then the final Qed just checks the auxiliary lemma statement rather than completely rechecking it.

queues. RTaW-Pegase analyzes these configurations in about 4 and 8 seconds.

Checking each of these benchmarks involved verifying thousands of operations in each case. We ran the benchmarks on an average few years old laptop with 4 GiB of RAM. The total run time where kept within a couple of hours thanks to checking time per operation well below the second in most cases, with only a handful of operations requiring a few dozen of seconds to be proved correct by Coq. All timings are summarized in Table 1. Note that the last benchmark had to be divided in eight separate Coq files to avoid Coq running out of memory on a huge file.

Although much slower than the initial runs of RTaW-Pegase, we consider these runtimes for verification to be perfectly acceptable considering that they would constitute the last part of the development or certification process of an embedded network. The fat RTaW-Pegase can still be used without extra verification for dimensioning or development purposes.

Last but not least, no bug was found in RTaW-Pegase during the experiments.

The benchmarks, as well as detailed instructions to reproduce those results, are available at https: //doi.org/10.5281/zenodo.5849594.

Conclusion

The skeptical approach (that formally proves the correctness of a result given by a program), is an efficient way to get a high level of confidence in the results of a program. It has been applied in the context of the real-time performances of embedded networks: the correctness of the min-plus operations involved in the computation of real-time bounds can now be checked using the Coq proof assistant. The theoretical part have been presented in [START_REF] Rakotomalala | Verifying min-plus computations with coq[END_REF]. This paper presents how it can be used in an industrial context.

This research experiment can be seen as a success both in terms of development effort and scalability of the verification. Developing a min-plus toolbox requires about one man-year of development [START_REF] Bouillard | An algorithmic toolbox for network calculus[END_REF][START_REF] Boyer | The PEGASE project: precise and scalable temporal analysis for aerospace communication systems with network calculus[END_REF], developing our min-plus checker required one PhD year of development [START_REF] Rakotomalala | Verifying min-plus computations with coq[END_REF] and plugging the min-plus checker and RTaW-Pegase required about 1 month of development. On run-time, analyzing a network with the RTaW-Pegase requires typically a few minutes using a common laptop whereas checking the results requires a few hours on the same hardware. For software with such a confidence level, the overhead in development time and running time is fully acceptable.

As a future work, one could consider unifying the previous works in [START_REF] Rakotomalala | Formal Verification of Real-time Networks[END_REF], [START_REF] Mabille | Towards certifying network calculus[END_REF] 1. Benchmarks: "#op" is the number of operations, "Time" the total time for Coq to check all operations (hours:minutes:seconds), "time / op" the average time per operations (in seconds), "max time" the maximum time to check a single operation (in seconds). a single Coq proof. This would greatly reduce the trusted code base and avoid having a Network Calculus expert check the output trace of RTaW-Pegase and its mapping to the verified Coq file.

Figure 1 .

 1 Figure 1. Example of visualization in RTaW-Pegase.

19 #

 19 Computations a t p r i o r i t y l e v e l 0 17 cumA Node1 := z e r o 18 Flow1 i n Node1 -> P1 20 cumA Node1 := cumA Node1 + Flow1 21 22# Flow2 i n Node1 -> P1 23 cumA Node1 := cumA Node1 + Flow2 24 25# Common s e r v i c e a t l e v e l 0 26 S Node1 := a f f i n e ( 1 0 0 , 0 ) 27 28# Common d e l a y 29 d Node1 := hDev ( cumA Node1 , S Node1 ) 30 31 a s s e r t ( d Node1 <= 1 5 6 / 5 )

Figure 2 .

 2 Figure 2. Example of a trace that can be produced by RTaW-Pegase

3 4

 3 Definition Flow1_js : @seqjs bigQ := [:: 5 (0, (0%:E, (0, 1360%:E))); 6 (5000, (1360%:E, (0, 1360%:E))); 7 (10000, (1360%:E, (0, 2720%:E)))]. 8 Definition Flow1 := F_of_sequpp {| 9 sequpp_T := 5000; 10 sequpp_d := 10000; 11 sequpp_c := 1360; 12 sequpp_js := Flow1_js 13 |}.

14 15

 14 Definition Flow2_js : @seqjs bigQ := [:: 16 (0, (0%:E, (0, 1760%:E))); 17 (2500, (1760%:E, (0, 1760%:E))); 18 (5000, (1760%:E, (0, 3520%:E)))]. 19 Definition Flow2 := F_of_sequpp {| 20 sequpp_T := 2500; 21 sequpp_d := 5000; 22 sequpp_c := 1760; 23 sequpp_js := Flow2_js 24 |}. 25 26 Definition S_Node1_js : @seqjs bigQ := [:: 27 (0, (0%:E, (100, 0%:E)))]. 28 Definition S_Node1 := F_of_sequpp {| 29 sequpp_T := 0;

3435

  Goal hDev_bounded (Flow1 + Flow2) S_Node1 (156/5). 36 Proof. nccoq. Qed.

Figure 3 .

 3 Figure 3. Example of Coq proof

1 Unset Printing Notations. 2 3 Set 2 Flow2) 3 ( 4 (

 123234 So lets inspect our freshly proved theorem. If one typesCheck hDev_bounded (Flow1 + Flow2) S_Node1 (156/5). Printing Notations.Coq reprints the statement with all notations expanded 1 UPP_PA_refinement.hDev_bounded (F_plus Flow1 S_Node1 (bigQ2rat (BigQ.div (BigQ.Qz BigZ.Pos (BigN.N0 156))) (BigQ.Qz BigZ.Pos (BigN.N0 5)))))

Figure 4 .Figure 5 .

 45 Figure 4. Prefix extention due to translation from RTaW-Pegase to NCCoq

(

  * Proof for Check 1*) (* Conversion of upp([(0,0)0(1,0)[, period ([(1,0)0(2,0)[), 0, 1) *) Definition lop_1_js : @seqjs bigQ := [:: (0, ( (0)%:E, (0, (0)%:E))); (1, ( (0)%:E, (0, (0)%:E)))] %bigQ. Definition lop_1 := F_of_sequpp {| sequpp_T := 1; sequpp_d := 1; sequpp_c := 0; sequpp_js := lop_1_js |}%bigQ. (* Conversion of upp([(0,0)0(0,0)], period (](0,1360)0(10000,1360)]), 1360, 10000) *) Definition rop_1_js : @seqjs bigQ := [:: (0, ( (0)%:E, (0, (1360)%:E))); (5000, ( (1360)%:E, (0, (1360)%:E))); (10000, ( (1360)%:E, (0, (2720)%:E)))] %bigQ. Definition rop_1 := F_of_sequpp {| sequpp_T := 5000; sequpp_d := 10000; sequpp_c := 1360; sequpp_js := rop_1_js |}%bigQ. (* Conversion of upp([(0,0)0(0,0)], period (](0,1360)0(10000,1360)]), 1360, 10000) *) Definition res_1_js : @seqjs bigQ := [:: (0, ( (0)%:E, (0, (1360)%:E))); (5000, ( (1360)%:E, (0, (1360)%:E))); (10000, ( (1360)%:E, (0, (2720)%:E)))] %bigQ. Definition res_1 := F_of_sequpp {| sequpp_T := 5000; sequpp_d := 10000; sequpp_c := 1360; sequpp_js := res_1_js |}%bigQ. Goal res_1 = (lop_1 + rop_1). Proof. idtac "Check 1". Time nccoq. Qed.

Figure 6 .

 6 Figure 6. Coq proof generated from listing in Figure 5.2

1

  Require Import minerve.tactic.

[START_REF] Bondorf | The DiscoDNC v2 -A Comprehensive Tool for Deterministic Network Calculus[END_REF]

Local Open Scope bigQ.

  and the current work in

	benchmark	#op	time time / op max time
	MEDIUM SP 1923	4:44	0.15	15.23
	BIG FIFO	34121	47:35	0.08	7.61
	BIG SP	81333 4:19:38	0.19	20.28
	Table


The Institut des politiques publiques (IPP) has been created by PSE and is developed through a

Introduction

Legally, in France, an "informal caregiver" to an elderly person is someone who provides regular assistance to a dependent elderly person in a non-professional capacity.

"The following are considered as 'close' caregivers of an elderly person: a spouse, a partner with whom the person has entered into a civil union pact, a cohabitant, a relative or a friend, defined as family caregivers, or a person living with the person or having a close and stable relationship with the person, who provides regular and frequent non-professional assistance to accomplish all or part of the acts or activities of daily life."1 Care within a couple may seem natural because it is rarely the result of a decision-making process between the two members of the couple but rather a gradual arrangement over time. In the case of married couples, the French Civil Code indicates, in article 212, that married partners "owe each other mutual respect, fidelity, help, assistance". Moreover, while an elderly person with a loss of autonomy can use their Personal Autonomy Allowance2 to pay for the help of a relative or friend, they cannot do so for the help provided by their partner. When people in a couple were interviewed before a possible loss of autonomy, half of them indicated that they would prefer their partner's help to professional help if they needed two hours of assistance per day [START_REF] Mahieu | Comment les Français envisagent-ils le risque dépendance ? Une analyse à partir des données de l'enquête Pat€r 2020[END_REF]).

Yet partners are the category of caregivers who report the most difficulties related to helping. Three-quarters of female caregiving partners and half of male caregiving partners report at least one negative health consequence of caregiving, compared with about one-third of other caregivers [START_REF] Besnard | Les proches aidants des seniors et leur ressenti sur l'aide apportée. Résultats des en-quêtes « CARE » auprès des aidants (2015-2016[END_REF].

Within couples in which one partner loses some autonomy, we are interested in the differences between the help provided by women and that provided by men. The definition of help within a couple depends on the preexisting division of labor, before the loss of autonomy of one of the partners changes the situation. Understanding the role of gender in caregiving within a couple requires going into the details of the tasks performed. We demonstrate the effect of gender on the probability of providing help, for different activities. We also show how age differences between partners influence our results.

How to assess help from others

Data

We use the CARE survey, presented in Box 1, which provides information on the assistance needs of people over 60, their marital status, and the help they receive. These data have the advantages of accurately describing the assistance provided and including information on the partner of the respondents (in particular, their gender and age), whether they are caregivers or not. The information on the level of autonomy concerns only one member of the couple: the one interviewed in the CARE survey. We can find information on the level of autonomy of the partner of the person interviewed in CARE only for certain partners who are present in the VQS survey (see Box 1).

Measuring the need for help

Loss of autonomy can be defined using two concepts: functional limitations and restrictions of activity (see Box 2). Functional limitations refer to the deterioration of body functions. Examples are difficulties in lifting an arm ("physical" functional limitation) or in concentrating ("cognitive" functional limitation). They are similar to a measure of health status. Activity restrictions measure the ability of the elderly to compensate for these functional limitations and to perform activities of daily life. A list of activities is usually proposed. For example, washing and cleaning are listed. The list of activities used to identify restrictions is similar to the one used to identify the assistance received.

To estimate a person's potential need for assistance in the analysis on page 5, we choose to use functional limitations. Activity restrictions could be influenced by what each person is used to doing or not doing in the household, and are therefore more likely to be endogenous. They are only used to select our sample of dependent individuals.

Measuring the assistance received

What does helping a dependent partner involve?

In the CARE survey, respondents are asked about their relatives who provide financial support, moral support, or help with daily life. We are interested in the latter type of assistance.

After identifying the restrictions that the respondents face regarding their daily activities, two questions allow us to identify their reliance on a caregiver from their family and friends:

-For which activities do you regularly receive

The Capacités, Aides et REssources des seniors (CARE) surveys, carried out by the Direction de la recherche, des études, de l'évaluation et des statistiques (DREES) with the support of the Caisse Nationale de Solidarité pour l'Autonomie (CNSA), aim to gain a better understanding of the living conditions of senior citizens, their relationships with their families and friends, their difficulties in carrying out certain activities of daily life, and the financial and social assistance they receive to overcome these difficulties.

The study has two parts: one focused on the institution; the other, CARE-M, on the home. We are interested in the home part, for which the question of the division of tasks within the couple makes sense. From May to October 2015, the CARE-M survey interviewed 15,000 people born before 02/05/1955 and living in ordinary accommodation in mainland France who had responded to the 2014 Vie Quotidienne et Santé (VQS) survey (one person per household). More than 10,000 people responded. Family and friends who provide assistance are also surveyed.

The CARE survey oversamples dependent people, so that specific analyses can be performed on this population. The sample weights, which we use in this study, make it possible to produce representative estimates of people aged over 60 living in mainland France in 2015.

Box 1 : The CARE surveys Box 1 : The CARE surveys

Functional limitations There are three types of functional limitations:

Sensory limitations: Having difficulty reading characters, seeing a face, hearing a person in a silent room, hearing what is said in a conversation with several people. If the person uses glasses, contact lenses or a hearing aid, we are interested in the person's abilities once they are fitted.

Physical limitations:

Having difficulty biting and chewing hard foods, walking 500 meters on level ground, walking up and down stairs, lifting an arm, using hands, kneeling, carrying a five-kilogram bag.

Cognitive limitations: Having difficulty remembering the time of day, concentrating for 10 minutes, solving everyday problems, understanding and being understood, relating to others, putting oneself in danger, having memory lapses, being aggressive.

Activity restrictions

Activity restrictions measure the level of autonomy by looking at the difficulties that people have in carrying out tasks of daily life. A distinction is made between Activities of Daily Life (ADL) (bathing, dressing or undressing, cutting food or serving drinks, eating and drinking, using the toilet, getting up or going to bed, sitting down or getting up from a chair) and Instrumental Activities of Daily Life (IADL) (performing household chores: shopping, preparing meals, cleaning, or administrative tasks, using the telephone, taking medication, using a means of transportation on one's own, moving between rooms on the same floor, getting out of one's home, taking public transportation, and finding one's way. The IADLs include tasks that some people do not perform, not necessarily because of a health problem, disability or age, but because someone else does them. The questionnaire specifies that it is only concerned with difficulties related to a health problem, disability or age. This wording distinguishes the usual division of labor within the couple and takes into account cases where the partner was already performing the task in question ("does more than before").

Elderly couples

The elderly and the couple

Because women live longer on average than men and are also younger on average than their partners, elderly men are more often in couples than women of the same age. They are also less likely to be widowed. When they are dependent, they are therefore more likely to have a partner. They are also more likely to have a partner who needs help.

"Elderly men are more likely to be in a couple than women of the same age."

Of the individuals over age 60 surveyed in the "household" component of the CARE survey, 64% are in a relationship. Barely half of the women (52%) have a partner, compared to 79% of the men. Of those who are dependent, 49% are in a couple. The difference between women and men in the probability of being in a couple is more pronounced among elderly dependents because many female dependents are widowed. Thus, female dependents are almost half as likely to be in a relationship as male dependents (38% versus 70%).

Loss of autonomy in the couple

Among people in couples, women and men are equally likely to have a dependent partner. The fact that men are generally older than their partners is offset by an earlier loss of autonomy, and over a longer period of time, among women.

"Among partners who are potential caregivers, there are as many men as women."

Selected sample

We include in our sample all people in cohabiting heterosexual couples, 3 married or not, with a CARE respondent who has at least mild difficulty in performing one of the basic or instrumental activities of daily life. On average, they report difficulties with two instrumental activities of daily life, and 0.5 basic activities of daily life. Our sample consists of 2,872 potential caregiving partners. We exclude those in a couple with someone with no difficulties, who are not likely to provide care.

Care generally provided within the couple

On average, 37% of the women in our sample help their dependent partner, compared to 41% of the men.

Figure 1 shows the proportions of men and women who help their dependent partner with different tasks. At the 3 Same-sex couples are not included because there are too few of them in our data. top right of this graph are the tasks most commonly performed by spousal caregivers are shopping, cleaning, and helping with medical care (making medical appointments and accompanying visits to the doctor, buying and helping with medications). Each of these three tasks is performed by more than 15% of partners of an elderly person with at least mild difficulty. These tasks are also identified as the most common by previous research [START_REF] Soullier | L'aide humaine auprès des adultes à domicile : l'implication des proches et des professionnels[END_REF]. Dependent older adults clearly identify when such tasks are performed by their partners due to their age or loss of independence, and do not consider their partners doing the shopping or cleaning to be part of the usual division of labor within the couple. Some tasks are more rare. For example, less than 10% of partners help their partner with eating, moving around, orientation, going to the bathroom, or making phone calls.

Above the first bisector of this graph, we find help with activities that are mostly performed by women: This is the case for help with washing or dressing (17% of women and 11% of men), help with using the telephone (7% of women and 3% of men). The tasks for which help is mostly provided by men are located below the first bisector. These include help with cleaning (18% of women and 21% of men), getting out of the house (11% of women and 15% of men), taking transportation (12% of women and 19% of men) and especially shopping (21% of women and 31% of men). All these differences are statistically significant.

To move around the home, go to the bathroom, or find one's way, help is provided equally by men and women. The involvement of men helping their partners with tasks outside the home (in blue in the graph) confirms the results of qualitative studies, which identify this phenomenon in couples with a traditional division of labor [START_REF] Renaut | Vieillir à deux, aides et entraide dans le couple[END_REF].

Results

Given equal needs, what tasks are performed by female and male caregivers?

An analysis controlling for the age and functional limitations of the partner who is potentially being helped allows us to identify whether the differences presented in Figure 2 presents the results grouped into three categories: tasks performed outside the home, housework performed in the home,4 and bodily care. Our measures identify whether the partner performs at least one task in each category, for example, at least one task outside the home. We also present the probability of providing at least one form of assistance, regardless of the activity.

Given the same needs and age, women and men in a couple with a person who has lost autonomy are equally likely to help, considering all tasks together. Men are more likely to help outside the home, the difference being between 2 and 11 percentage points (pp). This result is mostly due to shopping and helping with transportation. For some activities performed inside the home (DIY, meal preparation, using the telephone), women help their partners more than men, given equal needs. There is no difference related to the gender of the caregiver for administrative activities, cleaning, or medical care. Conversely, women are more likely to help their partner with bodily care (between +7 and +13 pp), especially dressing or washing and eating or drinking.

"Men help their partners more with tasks outside the home, and women help more with bodily care."

The choice of the measure of loss of autonomy does not impact our results. Indeed, the findings presented here do not change when we include the details of activity restrictions instead of functional limitations.

In perspective

While previous studies have highlighted the greater involvement of female partners [START_REF] Bonnet | La dépendance : quelles différences entre les hommes et les femmes ?[END_REF], our results show a more egalitarian evolution within couples in the probability of being a caregiver, all types of assistance combined. However, if we look in detail at which activities are performed by partners, we identify systematic differences by gender. The effect of gender on the type of activity performed by partners is similar to that observed for children who are caregivers: Petite and Weber (2006) show that sons help more with activities performed outside and [START_REF] Dutheil | Les aides et les aidants des personnes âgées[END_REF] shows that daughters help more with bodily care activities. Our study shows that in the case of partners, these differences are not related to differences in needs.

There is a clear social norm for considering that an independent person can perform certain activities, includ-ing bodily care, on their own. Conversely, some people may consider themselves independent even though they are unable to perform certain activities such as preparing a meal or doing DIY. These individuals will find it more difficult to identify their partner as a caregiver [START_REF] Roy | Qu'est-ce qu'un "proche aidant[END_REF]. One might have imagined that male caregivers would often report performing traditionally female tasks: if a woman loses her autonomy, her partner would report helping with meals, whereas if a man loses his autonomy, his partner who was already preparing meals would not report being a caregiver. However, our results do not attest to such a role reversal, as male caregivers do not more often report traditionally female tasks such as meals or cleaning. The only evidence of a reversal of the traditional division of labor is the higher proportion of women who report helping with DIY.

The role of the age of partners

Can our results be explained by the fact that women are often younger than their partners?

Younger or more independent partners might be more likely to help, which could explain why women, who are often younger, help their partners more with bodily care.

Given the same age difference between members of the couple, men help their partners more (between +0.2 and +12 pp). This effect is no longer significant if we also take into account the level of autonomy of the potential caregiver, because women who are younger than their partner are not necessarily in better health. The other results are almost identical. Regardless of whether the age or level of autonomy of the partner is taken into account, men help more outside the home, women help more with bodily care, and there are no systematic differences for housework performed within the home.

Results vary depending on whether the woman or man in the couple is older

Social norms related to gender may interact with age differences between partners. Does the help given to a partner depend on the age structure of the couple: traditional (older man) or otherwise?

In couples in which the man is at least three years older, the woman is more likely to provide care, across all types of help considered (Figure 3). This is in line with the results of [START_REF] Renaut | Vieillir à deux, aides et entraide dans le couple[END_REF], who identified a high level of involvement of partners in certain couples in which the man is the oldest. Conversely, if the partners are the same age or if the woman is the oldest, we find our previous results: Men perform more tasks outside the home and women help more with bodily care. In total, men are more likely to provide help than women when they are the same age or younger than their partner. In all situations, women more often provide help with bodily care.

"In couples in which the man is older, the woman is more likely to help her partner, given equal needs, regardless of the activity considered."

Conclusion and implications for public policy

Using detailed data on elderly couples, we examine the impact of gender on the probability of helping a dependent partner.

Women and men are equally likely to have a dependent partner, and equally likely to provide at least some assistance to their partner, considering all tasks together. Thus, while caregiver support policies are more relevant to women if we include all non-professional caregivers, this is not the case if we only consider partners.

Women and men who care for their partners do not perform the same activities to help, even if their partners have the same needs. Men do more chores outside the home, and women help more with bodily care. This gendered distribution is observed in couples of the same age and in those in which the woman is older. When the man is older, he is less involved than the woman in all activities.

A policy of assistance to caregivers must take into account the role of gender in the type of support provided.

The problems of the isolation of caregivers seem to be of greater concern for women, who provide more help within the home, while the help provided by men brings them into greater contact with the outside world. Female caregivers are also more vulnerable because they perform more bodily care, which involves a significant physical and emotional investment.

Providing support to couples, and female caregivers in particular, by offering and encouraging them to accept professional help for the tasks they perform for their partner, sometimes to the detriment of their health, must be an objective of policies that seek to help the elderly and their caregivers.

Figure 1 :

 1 Figure 1: Care provided by women and men in couples Sample: 2,872 people in couples with someone over 60 who has at least a mild difficulty with an activity of daily life. Definitions : Activities outside the home: Finding one's way around, getting out of the home, taking transportation, shopping. Activities in the home: Using the telephone, DIY, preparing meals, administrative tasks, helping with medical care, cleaning. Physical care: Helping to move around the home, dress and wash, go to the bathroom, eat or drink. Interpretation: 31% of men and 21% of women help their partner with shopping. Source: CARE-Ménages survey, DREES, 2015.

  Figure 1 persist with equivalent needs.

Figure 2 :

 2 Figure 2: Effect of gender on the care provided to a dependent partner Sample: 2,872 individuals in a couple with a person over age 60 who has at least a mild difficulty with a daily life activity. Definitions: Activities outside the home: Finding one's way, leaving the home, taking transportation, shopping. Activities in the home: Using the telephone, DIY, preparing meals, administrative tasks, helping with medical care, cleaning. Bodily care: Helping with moving around the home, dressing and washing, going to the bathroom, eating or drinking. Controls: Details of the age and functional limitations of the potential care recipient. Interpretation: Being male increases the likelihood of assisting one's dependent partner with outdoor tasks by 6 percentage points, given the same age and needs. Source: CARE-Ménages survey, DREES, 2015.

Figure 3 :

 3 Figure 3: Effect of gender on helping a dependent partner, by relative age of partners Sample: 1,441 couples in which the man is at least three years older and 1,431 couples in which the man is younger, or the same age (+/-3 years), and in all of which a person over 60 has at least a mild difficulty in a daily life activity. Definitions: Activities outside the home: Finding one's way, getting out of the home, taking transportation, shopping. Activities in the home: Using the telephone, DIY, preparing meals, administrative tasks, helping with medication, cleaning. Bodily care: Helping with moving around the home, dressing and washing, going to the bathroom, eating or drinking. Controls: Details of the age and functional limitations of the potential care recipient. Interpretation: In couples in which the man is older, being a man decreases the likelihood that he will help his dependent partner with bodily care by 15 percentage points. Source: CARE-Ménages survey, DREES, 2015.

Box 2 : Measuring loss of autonomy Box 2 : Measuring loss of autonomy

	help from one or more people around you (part-
	ner, family, friend...)? [List of declared activity
	restrictions]
	-For each activity restriction reported: Among
	your family or friends, who helps you with [this
	activity]?
	The CARE survey specifically identifies help from cohab-
	iting caregivers with the following question:
	Because of your health problems or age, does
	[caregiver's first name] do more than before or
	regularly help you with any of the following ac-
	tivities? [List unreported activity restrictions]

Article L113-1-3 of the Code de l'action sociale et des familles.

The Allocation personnalisée d'autonomie (APA) is used to pay, in whole or in part, the expenses related to the loss of autonomy of elderly people, at home or in an institution.

Two tasks can be done indoors or outdoors: helping with treatment, and DIY/gardening. We include them in the most varied category, housework performed in the home.

Acknowledgments

This study received financial support from the Caisse nationale de solidarité pour l'autonomie (CNSA). It was carried out within the framework of an IPPCNSA research contract entitled "Trajectoires des personnes âgées en perte d'autonomie et disparités départementales de prise en charge".

scientific partnership between the Paris School of Economics (PSE) and the Groupe

Authors

Léa Toulemon is an economist at IPP.


Amélie Carrère

Mapping loss of autonomy among the elderly

The Institut des politiques publiques (IPP) has been created by PSE and is developed through a scientific partnership between the Paris School of Economics (PSE) and the Groupe des écoles nationales d'économie et de statistique (GENES). The aim of the IPP is to promote quantitative analysis and evaluation of public policy using cutting-edge research methods in economics.

Mapping loss of autonomy among the elderly Understanding the differences in loss of autonomy between French departments is essential since they are the leading providers of social services to the elderly. For the first time, thanks to the combination of several data sources, it is possible to obtain a snapshot of the care needs of the elderly in each French department. This study sheds light on the differences in care that can be observed between departments from the perspective of the needs of their citizens, and can help to orient local policies to meet these needs. Unlike previous studies on the subject, it is not restricted to the population receiving benefits related to loss of autonomy [START_REF] Abassi | L'aide et l'action sociales en France -Perte d'autonomie, handicap, protection de l'enfance et insertion[END_REF], it includes both the at-home and institutionalized populations [START_REF] Brunel | Les personnes âgées dépendantes vivant à domicile en 2015. Premiers résultats de l'enquête CARE "ménages[END_REF], and it compares several measures of disability [START_REF] Larbi | 4 millions de seniors seraient en perte d'autonomie en 2050[END_REF]. Moreover, it allows us to question the implications of departmental policy via two channels: (1) the way departments mobilize the criteria for assessing loss of autonomy; and (2) the supply of institutional places and the residential mobilities that may induce.

The analysis of several measures of loss of autonomy highlights differences between French departments in terms of prevalence, type of disability, and its appearance at an early age.

Pas-de-Calais is particularly affected by physical disabilities (24% of people aged 60 or more), Guadeloupe by cognitive disorders (17%), and Lozère by difficulties in washing (13%). Northern France and Seine-Saint-Denis stand out for early onset of difficulties (before 75 years of age).

These differences in needs are not entirely consistent with the loss of autonomy assessed by the departmental councils.

Departmental differences in needs change little when considering the department of residence before entering a nursing home, with the exception of a few departments. Paris is the department for which the prevalence of loss of autonomy decreases the most due to an "institutional" exodus.

What are the differences depending on who assesses disability?

In France, to measure loss of autonomy among the elderly, it is possible to:

• use survey data that question the elderly about their difficulties;

• or mobilize administrative data.1

Administrative sources regarding the Allocation personnalisée d'autonomie (APA) are derived from an evaluation by departmental councils, whose criteria can be reconstructed using survey data. To open the discussion on equity of access to the financing of disability, this study first presents the differences between the evaluations made by departments and the declarations of elderly people in the surveys.

Assessment of disability by departmental councils

Departmental councils are responsible for assessing the needs of elderly people applying for APA. They assign them an iso-resource group (GIR) which classifies people according to their degree of loss of autonomy.2 This administrative measure of loss of autonomy can be converted into a weighted average GIR (GIR moyen pondéré, or GMP), Box 1. A GMP of 100 is equivalent to an average need for 10 full-time jobs for 100 elderly people living in that department. 3 The GMP "assigned" by department provides information on the care needs of the elderly from the point of view of the allocation of social assistance. The assigned GMP is 113 points in the French population aged 60 or more. It varies from 92 points in Guyana to 139 points in Haute-Corse (Figure 1-A).

"The loss of autonomy assessed by departments is highest in Haute-Corse, lowest in Guyana." GMP: weighted average GIR. GIR: iso-resource group (disability score). A score of 70 is applied equally to all GIRs (estimated or assigned) 5-6. Note: The relative gap corresponds to the difference between the GMP estimated with surveys (in the department before entering nursing home) and the GMP assigned by the department divided by the GIR assigned by the department. Interpretation: Aude department has an assigned GMP of 109 points (average need of 10.9 employees per 100 elderly people) and an estimated GMP of 189 points (average need of 18.9 employees per 100 elderly people). Sources : DREES, 2014 VQS, 2015 EHPA and 2015 Aide Sociale surveys. Coverage: French departments (excluding Mayotte).

Assessment of disability using survey data

We use the same methodology as [START_REF] Larbi | 4 millions de seniors seraient en perte d'autonomie en 2050[END_REF] For all departments, the GMP estimated by survey is higher than the GMP assigned by the departments. The relative dif-ference is greatest in Guadeloupe (Figure 1-B).

The differences between the needs attributed by the departmental councils and the needs estimated by surveys may be due to individual effects such as non-use of APA,4 but also to differences in the implementation of departments' gerontological policy. The latter has an impact on:

• APA applications: Applications are made by elderly individuals or their entourage but the degree to which they are facilitated by the departments may vary (complexity of the files, access to information about APA, etc.);

• Eligibility for APA: People whose GIR is between 1 and 4 can benefit from the department's coverage of part of their dependency expenses. Departments may therefore be encouraged to assess people at the limit of their eligibility for APA as GIR 5 rather than 4;

• GIR evaluation: The amounts proposed for APA depend on the GIR assigned.

The department's dual role as assessor and funder of loss of autonomy, allocating APA under a constrained budget, may encourage it to minimize the needs measured in an attempt to limit expenditure.

"Differences between the loss of autonomy measured by surveys and by departments calls into question the ability of departments to identify the real needs of the elderly."

Type of loss of autonomy and age: Differences within differences

The GMP is a synthetic measure of loss of autonomy. It shows both the prevalence and the severity of loss of autonomy, but masks its multidimensional nature (Box 1). Depending on the measure of loss of autonomy considered or the source used, there are between 1.3 and 3.9 million people aged 60 or over with loss of autonomy in France [START_REF] Abassi | L'aide et l'action sociales en France -Perte d'autonomie, handicap, protection de l'enfance et insertion[END_REF]. Our analysis also questions the capacity of the AGGIR assessment grid to capture several dimensions of loss of autonomy.

Progress in the management of loss of autonomy varies from one department to another

The different types of functional limitations, as well as difficulties in washing oneself, are not identically distributed across the country. A principal component analysis (PCA) of the different measures of loss of autonomy (Box 2) takes into account territorial specificities. Figure 4-A

Differences in age at onset of disability

The differences identified above partly hide differences in the age of exposure to the risk of loss of autonomy according to departments. We have therefore carried out the same type of analysis by splitting the loss of autonomy indicators: prevalences among people aged 60 to 74 and among people aged 75 or more are introduced separately (part "B. 60-74 years and 75 or more" of Figure 4). The x-axis still identifies the prevalence of loss of autonomy regardless of age, and Loss of autonomy is measured, on the one hand, using administrative data from the 2014 DREES Aide Sociale survey. Three measures are calculated at the departmental level: the weighted average iso-resource group (GIR moyen pondéré, or GMP) assigned by the departmental councils (assigned GMP: GMP_reel); a the proportion of people assigned to GIR 1 to 4 (GIR14_reel); the proportion of people assigned to GIR 1 or 2 (GIR12_reel).

On the other hand, it is also estimated by combining data from the 2014 Vie Quotidienne et Santé (VQS) survey, which questioned 166,800 people aged 60 or over, and the 2015 Établissement d'Hébergement pour Personnes Agées (EHPA) survey (299,264 nursing-home residents). Estimates are given for the proportion of people with at least one functional limitation (LF) related to physical mobility (LFphys); b the proportion of people with at least one cognitive LF (LFcog); c the proportion of individuals with both physical and cognitive LFs (deuxLF); the proportion of individuals with LFs but no restriction of activity (RA) (LFseul); d the proportion of people with (physical or cognitive) LFs combined with RAs (LFRA); the estimated GMP e (GMP_est); the proportion of people in estimated GIR 1 to 4 (GIR14); and the proportion of people in estimated GIR 1 or 2 (GIR12).

The analyses are carried out on the population aged 60 years or more residing in France, in "ordinary" accommodation or in a care home for dependent elderly (Etablissement d'Hébergement pour Personnes Agées dépendantes, or EHPAD), a non-EHPAD EHPA, or a long-term care unit (unité de soins longue durée, or USLD).

a The (assigned or estimated) GMP corresponds to the average level of dependency in a given population. A person in GIR 1 has a weight of 1000, respectively 840 for a person in GIR 2, 660 for a person in GIR 3, 420 for a person in GIR 4, 250 for a person in GIR 5, and 70 for a person in GIR 6. The (assigned or estimated) GMP of a department is the sum of the weights of each person aged 60 or more compared to the total population aged 60 or more of the department.

b They are measured in VQS using the question "Does the person have difficulty climbing a flight of stairs or walking 500 meters?" (grouping the options "No and "Yes, a little" vs. "Yes, a lot" and "Can't at all") and the "Moving around the home" axis of the AGGIR grid (No=A vs. yes=B, C) in EHPA.

c Cognitive LFs are measured using the questions "Does the person have difficulty with... Understanding others or being understood by others; Concentrating for more than 10 minutes; Remembering important things; Solving everyday problems (such as finding their way around or counting money)" in VQS (grouping the options "No" and "Yes, a little" vs. "Yes, a lot" and "Can't at all") and using the "Orientation in time", "Orientation in space", " Behavioral coherence", and "Orientation in communication" dimensions of the AGGIR grid used in EHPA (No=A vs. yes=B, C).

d The RA are measured using the question "Does the person have difficulty washing themselves?" in VQS ("No"; "Yes, a little" vs. "Yes, a lot"; "Can't at all") and using the "Washing" section of the AGGIR grid in EHPA (No=A vs. yes=B, C).

e In the VQS survey, the GIR is imputed via a model using the common variables between the VQS and CAREMénages surveys (DREES, 2015). For EHPA, it is the assigned GIR.

Box 1 : Loss of autonomy: Definitions, measures and data Box 1 : Loss of autonomy: Definitions, measures and data

We use principal component analyses (PCA). These allow us to classify statistical individuals, in this case departments, into dimensions, which we call "principal components", constructed from variables, in this case measures of loss of autonomy, at several ages (60 years or more; 60-74 years; and 75 years or more). The advantage of this method is that each dimension removes redundancy from correlated variables. For each component, a variable is created: the "coordinate" of the component. It summarizes the variables that are most important for this component and allows the department to be positioned on a plane (when considering the first two dimensions, for example). Groups of departments with similar characteristics (or clusters) are constructed using the kmeans method. We choose to construct five distinct clusters. a The kmeans method is based on minimizing the sum of the squared Euclidean distances between each department and the centroid (center point) of its cluster.

a "Elbow", "silhouette" and "gap statistic" methods are used to determine the optimal number of clusters to build.

Box 2 : Methodology: Principal component analysis Box 2 : Methodology: Principal component analysis contributes 45% of the total variance. Departments to the right have higher prevalences. The y-axis identifies the earliness of the loss of autonomy. This dimension contributes 21% of the total variance. The departments at the top have high prevalences before age 75. Those at the bottom have high prevalences after age 75.

"The departments most affected by cognitive disorders have high prevalences, especially after age 75. The departments most affected by physical disabilities have high prevalences, especially before age 75."

Northern and eastern France have high prevalences of loss of autonomy at all ages (departments in purple in Figure 2). Central France, Brittany, and the Rhone Valley have high prevalences, especially after age 75 (departments in pink). Departments on the Le Havre-Troyes line (to the north and east of Ile-de-France) and the Loire Valley departments (to the south of Ile-de-France) have high prevalences, especially before the age of 75 (departments in yellow). Loss of autonomy remains low in the coastal departments. The Paris region (except for Seine-Saint-Denis) still has the lowest prevalence, especially among people over 75.

Do we really measure departmental differences in loss of autonomy?

The differences in prevalence identified can be questioned from the perspective of residential mobility to- wards old people's homes [START_REF] Ramos-Gorand | Accessibilité de l'offre en établissements d'hébergement pour personnes âgées : enjeux territoriaux[END_REF]. The estimates presented above do not make it possible to know whether there are departments in which it would be good to grow old, or whether the apparently "advantaged" departments are so because dependent elderly people have left their territory due to the lack of care.

The surveys used provide information on the department of residence before entering an institution. We therefore estimate the prevalence of loss of autonomy in the department of residence before moving to an institution, in order to compare it with the prevalence estimated previously, which used the department of residence at the time of the survey. In the majority of departments, the prevalence changes little. For some, however, the gain or loss due to institutional mobility is significant (Figure 3). Prevalence decreases the most due to migration to another department for the departments in dark red. 5 These areas are close to areas that appear to receive dependent elderly people (dark blue). Paris and the Rhone Valley "benefit" the most from the exodus of elderly people (in the sense that they see their rate of prevalence of loss of autonomy improve). Conversely, Lozère, Yonne, Ain and Territoire-de-Belfort "suffer" the most from the migration of elderly people to their territory.

5 These are the 25% with the highest value (strong improvement).

Conclusion

The loss of autonomy estimated by the surveys does not match the loss of autonomy evaluated by the departmental councils in the context of the allocation of APA, which raises the question of access to aid to help the elderly pay for part of the cost of their loss of autonomy.

The results, in terms of type of loss of autonomy and age of onset, support the hypothesis that the type of underlying pathologies may explain the mismatch between life expectancy and disability-free life expectancy (Crouzet et al., 2020). We can see here that the departments with the most physical limitations witness these disabilities before the age of 75. These are the same departments that have a double disadvantage in terms of life expectancy and disability-free life expectancy. These departments are characterized by a historically high level of industrial activity, which may explain the appearance of early disabilities and lower longevity. On the other hand, the departments in which the elderly suffer mainly from complex disorders are those which combine high longevity with a high proportion of years of life with disability. These are rather rural departments where agricultural activity is important.

The departmental differences observed should also be seen in the light of the mobility induced by a lack of facilities in certain territories. [START_REF] Laborde | Contextual factors underpinning geographical inequalities in disability-free life expectancy in 100 French départements[END_REF] identify that a high density of institutions reduces both life expectancy and disability-free life expectancy. Our analyses suggest that the lack of supply, or its high cost, effectively induces residential mobility that modifies territorial inequalities in loss of autonomy. Thanks to the principle of "domicile de secours", the financial burden of this mobility is not passed on to the departments where the elderly are placed in nursing homes. However, these interdepartmental mobilities, which are not always chosen, call into question the adequacy of the supply to the needs [START_REF] Carrère | Un nouvel indicateur pour mesurer l'accessibilité géographique aux structures médicosociales destinées aux personnes âgées[END_REF].

  Figure 1: Comparison of an administrative measure of disability by source (administrative or surveys)

Figure 2 :

 2 Figure 2: Map of departmental differences in loss of autonomy according to age of individuals Department: Department of residence at the time of the survey. Note: This is the cartographic representation of the principal component analysis of Figure 4-B. Interpretation: Corsica, in yellow, is characterized by a rather high disability level, especially before age 75. Coverage: Departments in metropolitan France. Sources: DREES, 2014 VQS and 2015 EHPA surveys.

Figure 3 :Figure 4 :

 34 Figure 3: Map of the indicator of rise/fall in prevalence before and after institutional mobility Note: The thresholds used correspond to the quartiles of the indicator of rise/fall in prevalence. The latter is constructed using a PCA on all the indicators of relative difference in prevalence before and after mobility to a nursing home (coordinate of the first dimension of the PCA). Interpretation: The prevalence of disability in the department before entering a nursing home is lower than the one in the department after admission to a nursing home for Territoire-de-Belfort (in dark blue). Sources: DREES, 2014 VQS and 2015 EHPA surveys. Coverage: Departments of metropolitan France.

  corresponds to the projection in a plane of the different indicators of loss of autonomy based on the population aged 60 or more by department of residence at the time of the survey. They are represented by the arrows and indicated by the name of the measure. The x-axis identifies the prevalence of loss of autonomy in the department, in the sense of the proportion of people affected by loss of autonomy. Departments with the highest prevalence rates are located on the right. This dimension contributes 75% of the total variance. The y-axis identifies the severity of the loss of autonomy. Departments with complex disabil-

ities (cognitive disorders or situations of cumulative functional limitations or activity restrictions) are at the bottom of the graph. Axis 2 contributes to 14% of the total variance. Departments in central France and Occitanie (in pink) are more affected by complex disabilities. The high prevalences seen in northern France (purple) are mainly related to physical difficulties or simpler disabilities. Conversely, Île-de-France, Haute-Savoie, Normandy and Morbihan (in apple green) are less affected by loss of autonomy. Between these categories, there is a gradient in the need for care, with a slight advantage for the departments of Brittany, the mountainous regions (Alps, Pyrenees, Vosges) and the coastal regions (in mint green) and a slight disadvantage for the eastern and rural regions (in yellow).

"Departments in central France and Occitanie are more affected by cognitive problems; northern France is more impacted by physical difficulties. Île-de-France, Haute-Savoie, Normandy and Morbihan are less affected by loss of autonomy."

Evaluation of loss of autonomy requested by elderly people is carried out by departmental councils. This assessment then allows them to be allocated an amount of aid to cover all or part of their disability expenses.

 2 The GIR has a value from 1 to 6. People in GIR 1 are the most dependent; those in GIR 5 or 6 are

autonomous.3 The 2007-2012 Solidarité Grand Âge plan recommends a ratio of one employee per 1,000 GIR points in institutions.

For example, lack of knowledge of APA, underestimation of their need, and low rates of coverage were cited as possible reasons for nonuse of APA.

Acknowledgments

This study received financial support from the Caisse nationale de solidarité pour l'autonomie (CNSA). It was carried out within the framework of an IPPCNSA research contract entitled "Trajectoires des personnes âgées en perte d'autonomie et disparités départementales de prise en charge".

Author


Thomas Le Barbanchon

Julien Sauvagnat

The Institut des politiques publiques (IPP) has been created by PSE and is developed through a scientific partnership between the Paris School of Economics (PSE) and the Groupe des écoles nationales d'économie et de statistique (GENES). The aim of the IPP is to promote quantitative analysis and evaluation of public policy using cutting edge research methods in economics.

Electoral Competition, Voter Bias, and

Women in Politics

Only a quarter of the members of the world's national parliaments are women. Despite significant progress in recent years, women remain largely under-represented among elected politicians. This study provides some explanations for the underrepresentation of women in politics using data from the past seven French legislative elections. On the one hand, the analyses suggest that there is a preference bias among voters towards male candidates. In addition, political parties contribute to reproducing the under-representation of women in elected office by running fewer female candidates in constituencies where voter bias is high. To promote women's access to political office, the 2000 law to promote equal access of women and men to electoral mandates and elective offices, also known as the parity law, requires French political parties to nominate women as 50% of their candidates or face financial penalties.

As expected, the application of this law has led to an increase in the proportion of women candidates. However, this proportion is relatively lower in electoral districts where the vote is close compared to those where a majority is more easily obtained.

In these competitive districts, paying a fine for not complying with the parity rule is more advantageous than the risk of losing the election by running a woman rather than a man. This suggests that parties still prefer to put forward male rather than female candidates to increase their chances of winning.

An increase of e200 in the gross monthly gender pay gap, in favor of men, increases the vote gap between male and female candidates in legislative elections by 1 percentage point in favor of men.

A 10 percentage-point increase in the proportion of people reporting that men are better political leaders than women is associated with a 10% decrease in the number of women running for office.

A 10% increase in the number of districts where the electoral race is close significantly reduces the effectiveness of the parity law: the share of women parliamentarians drops from 28% to 23%.

Introduction

Despite significant progress in recent years, there is still some way to go to achieve gender parity in elected office. Only a quarter of the world's national parliamentarians are women.

There is no consensus on the mechanisms contributing to this under-representation. Some work explores the role of political parties in promoting male candidates [START_REF] Norris | Political Recruitment. Gender, Race and Class in the British Parliament[END_REF], but the findings of recent studies are mixed [START_REF] Casas-Arce | Women and Power: Unpopular, Unwilling, or Held Back?[END_REF][START_REF] Bagues | Can Gender Quotas in Candidate Lists Empower Women? Evidence from a Discontinuity Design[END_REF].

The possibility that women's access to political office is limited by voter preferences is also widely debated. One reason is the difficulty in empirically identifying voter preference bias for male candidates. This bias corresponds to a situation in which a voter is more likely to vote for a male politician than for a female politician, even though both candidates have the same ideology and expertise. 1This study measures voter bias against women in politics and the strategic bias of political parties, which reinforce the under-representation of women in politics by incorporating voter bias into their choice of candidates. The analyses use electoral results from the past seven French legislative elections, from 1988 to 2017 (see Box 1).

Voter preference bias in favor of male candidates

According to [START_REF] Bertrand | New Perspectives on Gender[END_REF], the gender pay gap that is not explained by the skill level of employees or the nature of their jobs reflects negative ideas about women's place in society. The bias of voters in favor of men is thus approximated by the gap in gross monthly earnings between women and men at the municipal level (see Box 1).

Voters' preference bias in favor of male candidates is approximated in each municipality by the gender pay gap.

These are compared with the vote gaps between male and female candidates in legislative elections. The same electoral district includes several municipalities, which makes it possible to compare the electoral results and the gender pay gap in municipalities with the same candidates (because they are from the same district).

A large pay gap between women and men, to the disadvantage of women, is associated with a significantly higher preference of voters for male candidates. Figure 1 presents the coefficients of several econometric analyses. In all analyses, there is a negative and statistically significant relationship between the pay gap and the vote gap: residents of municipalities with high pay disparities in favor of men give more votes to male candidates than to female candidates. Interpretation: According to the third specification, a 10 percentage-point increase in the gender pay gap, in favor of men, results in a 0.7 percentage-point loss of vote share for female candidates.

In the most comprehensive analysis, an increase of e200 in the gross monthly gender pay gap, in favor of men, decreases the vote share received by female candidates (relative to male candidates) by 1 percentage point. For comparison, in the analysis sample, about 12% of runoff results in the legislative elections have vote gaps between the two candidates of less than 1%. These situations could have resulted in a different outcome in the absence of voter preference bias. This confirms that voter bias in favor of male candidates has a significant impact on electoral outcomes in terms of gender parity.

Even when controlling for other characteristics of the municipality -such as its proportion of female voters, size, or employment rate -voter bias in favor of male candidates remains significant.

The presence of voter bias in favor of male candidates re-lated to the gender pay gap raises questions about the integration of this bias into the strategies of political parties. To measure the strategies of political parties, and in particular to identify whether they are incorporating potential voter preference bias in favor of male candidates by running fewer female candidates in more biased districts, we analyze the relationship between voter preference bias and the share of female candidates running for office in each electoral district.

Integration of voter preference bias by political parties

Voter preference bias in favor of male candidates is approximated by the gender pay gap (as before) and also by the share of people who agree with the statement "Men are better political leaders than women", calculated at the county level using the Generations and Gender Survey (GGS) (see Box 1).

Districts with a strong voter preference bias in favor of male candidates are more likely to have male candidates than female candidates.

Figure 2 presents the statistical relationship between the likelihood that a woman will be a candidate and the share of people who agree with the statement "Men are better political leaders than women", controlling for candidate characteristics (age, education, occupation), political party, election year, past political experience, and party's score in the previous presidential election. A 10 percentage-point increase in the share of those who say that "Men are better political leaders than women" is associated with a 2.3 percentage-point decrease in the likelihood that a woman will be a candidate in the election. Figure 3 replicates the analysis using the gender pay gap at the district level instead. A 10 percentage-point increase in the gender pay gap is associated with a 5 percentage-point decrease in the likelihood that a female candidate will run for office in that district.

These results suggest that political parties or candidates themselves internalize the voter preference bias in favor of men. The creation of the parity law (see Box 2) requires parties to field 50% women candidates. This reform may have led to changes in party strategies for running candidates in elections.

We analyze the elections of deputies to the National Assembly in 1988Assembly in , 1993Assembly in , 1997Assembly in , 2002Assembly in , 2007Assembly in , 2012Assembly in and 2017. The National Assembly is composed of 577 deputies. The voting system is a two-round majority system. Three data sources are mobilized: (i) administrative and online data on candidates and their electoral results; (ii) survey data on attitudes towards men and women; (iii) administrative and census data on earnings and socio-demographic characteristics aggregated by municipality or electoral district. The Ministry of the Interior publishes the votes obtained by each candidate in the legislative elections since 1988 in the different municipalities of each electoral district (550 districts for 36,000 municipalities), as well as their gender and political party. Their date of birth and socioeconomic category are only available from 2012. We complement the Ministry of the Interior's data on candidates with online and academic sources (Le [START_REF] Barbanchon | Electoral Competition, Voter Bias, and Women in Politics[END_REF]. The study sample is restricted to candidates with a reasonable chance of being elected, i.e., candidates from the two major coalitions on the right and left that account for 80% of elected deputies. a To directly measure gender bias, we use two indicators. The first is the proportion of people who agree with the statement "Men are better political leaders than women", calculated at the departmental level using the 2006 Generations and Gender Survey (GGS) of the Generations and Gender Program, which surveyed nearly 10,000 households and was coordinated in France by INED (Institut national d'études démographiques). The second is the gender pay gap. This is calculated for each French municipality and each electoral district in the year preceding legislative elections using DADS (Déclarations annuelles de données sociales) data from INSEE (Institut national de la statistique et des études économiques). Each privatesector employer declares the annual salaries paid to each of its employees. These pay gaps are estimated for identical worker characteristics (age, occupation, and sector of activity) and for the employee's municipality of residence. We also use INSEE census data to characterize the localities.

1. Voter preference bias in favor of male candidates. To study the relationship between the gender pay gap and the vote gap between female and male candidates, we estimate the following linear regression model:

VoteShare i,m,t = α i,t + νm,t + β • PayGapMF m,t × Female i + γ • PayGapMF m,t × X i,t + ϵ i,m,t (1)
where VoteShare i,m,t is the score of candidate i obtained in the first round of the legislative election t in municipality m and PayGapMF m,t is the pay gap (in logarithm) between men and women residing in municipality m measured in the year before the election (adjusted for employee characteristics). We interact the pay gap with a variable indicating female candidates Female i . The coefficient of this interaction β is the one reported in Figure 1. The first coefficient is from an analysis that includes only fixed effects for each candidate per election α i,t and fixed effects for each municipality per election νm,t. The second coefficient also introduces interaction terms of the wage gap with the socio-demographic characteristics of the candidate X i,t . The last coefficient also includes the candidate's political experience. For this analysis, only parliamentary districts with candidates of different sexes are selected. The sample is composed of more than 280,000 observations (one observation corresponds to the candidate, municipality, and year triplet).

Incorporation of voter preference bias by political parties.

To investigate the relationship between the preference bias against women and the share of women among candidates, we estimate the following linear regression model:

Female i,d,t = αp,t + β • VoterBias d,t + γ • X i,t + µ • PresidScore p,d,t + ν d + ϵ i,d,t (2)
where p denotes the political party of candidate i in election t. Female i,d,t indicates whether candidate i running in district d for election t is a woman. VoterBias d,t is either the share of respondents agreeing with "Men are better political leaders than women" in the department of district d, or the pay gap between women and men in district d in year t -1. We introduce a fixed effect specific to each political party and election, αp,t.

In some specifications, we also introduce the characteristics of the candidate X i,t , and the score obtained by the candidate's party in the previous presidential election in the same district PresidScore p,d,t . In the specification with pay gaps, we also introduce a fixed effect of the district ν d . The coefficient β is represented by the slope of the curve in Figures 2 and3.

Strategic reactions of political parties to the parity law.

We estimate the following linear regression model:

Female i,d,t = αp,t + βt • CompetitiveDistrict d,t + δt • PresidScore p,d,t + γt • X i,t + µt • PayGapMF d,t + ϵ i,d,t (3)
where p denotes the political party of candidate i in election t. All other variables are already defined above, except CompetitiveDistrict d,t indicating whether district d is competitive in election t.

a The left-wing coalition includes the Parti Socialiste (PS, 84%) and the Parti Radical de Gauche (PRG, 12%). The right-wing coalition includes Rassemblement pour la République (RPR, 79%) and Union pour la Démocratie Française (UDF, 20%) until 1997, then Union pour la Majorité Présidentielle (UMP) in 2002, 2007 and 2012, and Les Républicains (LR) in 2017. We exclude République en Marche and Mouvement Démocrate (MoDem) from our analysis. Nevertheless, the results remain unchanged if we add their candidates to the analysis.

Box 1: Data sources and statistical method Box 1: Data sources and statistical method

The law to promote equal access of women and men to electoral offices and positions, known as the parity law, was enacted on June 6, 2000. It encourages political parties to put forward as many women as men in legislative elections. When a party deviates from parity, it is subject to a financial from the first fraction of its public funding for each male candidate above the number of female candidates. The amount of the deduction was increased in 2007 and 2014. For other French elections with a multi-member voting system, the parity law requires parties to present as many women as men, and they cannot deviate.

Political parties' strategic responses to the parity law

The financial penalties for non-compliance with the parity law are charged to party budgets, not to individual candidates. This suggests that the incentive not to comply with the law affects the parties directly.

This latitude allowed to parties has led to a slow increase in the share of female candidates, but it is far from achieving parity. In our analysis sample, the share of female candidates was less than 30% in the 2002 elections, and reached only 40% in 2017. In a context marked by electoral bias against women, parties face a trade-off between the cost of losing an election by selecting a female rather than a male candidate, the electoral cost, and the cost of not complying with the parity law. In the case of a close election (competitive districts), the strategy of paying a fine may appear to be more expedient because the electoral cost of running a female candidate is potentially high. In a close election, every vote counts, and voter bias against women can significantly affect a party's chances of winning a seat. Thus, if parties internalize the bias of voters against women, they will refrain from running female candidates in competitive districts. This trade-off did not exist before the introduction of the parity law, since political parties could choose among local candidates the one most likely to win the election. In the presence of a voter preference bias in favor of men, this led to a low share of female candidates (see previous section), but it was not related to the degree of local electoral competition.

To measure the strategies of political parties, this section examines the evolution of the share of female candidates in districts with strong electoral competition versus those with weaker competition.

After the parity law, political parties are more likely to run male candidates in legislative elections in districts where the race is close.

Figure 4 shows the difference in the proportion of female candidates between competitive and non-competitive districts in different legislative elections. Districts are said to be competitive when, in the current election, the winner has a vote advantage of less than 3 percentage points. 2 Prior to 2000, we find no significant difference between districts. In 2002 and 2007, the difference is significantly negative. These results provide strong evidence for the existence of a strategic bias by political parties, manifested in the selection of male candidates over female candidates in competitive districts after the introduction of the parity law. The fact that the proportion of female candidates is not significantly lower in competitive districts before the introduction of the parity law rules out a possible aver-2 Another measure is used to define the degree of competition in the legislative election. This is the predicted results from the vote shares for parties on the right and left in the presidential election. The results are identical to those in Figure 4 with this measure. sion on the part of female candidates to campaigning in a highly competitive environment.

The lower proportion of women chosen to run for office in competitive districts could be explained by differences in female candidates' abilities to wield political office. However, the educational gap between current male and female municipal politicians, the vast majority of whom will be future candidates for legislative elections, is weakly correlated with the degree of competition in the district.

This emphasis on male candidates for legislative elections in competitive districts is not explained by local differences in skills between women and men.

Using a theoretical model calibrated on the results observed before and after the parity law, the simulation of the degree of electoral competition between the two main political parties makes it possible to estimate that a 10% increase in the share of competitive districts would reduce the increase in the proportion of women elected due to the parity law by 25%. This exercise illustrates how the effectiveness of flexible quotas in increasing women's representation in parliament is undermined by electoral competition.

Conclusion

The analyses in this policy brief confirm the existence of a voter preference bias in favor of men and a strategic bias of political parties in response to this voter bias.

Other mechanisms may explain the under-representation of women in politics, such as differences in women's and men's willingness to engage in political careers or the presence of intrinsic negative bias against women within political parties.

That said, the evidence provided in this policy brief has important implications for the design of public policies to increase women's representation in parliament. First, they highlight the relative ineffectiveness of flexible gender quotas in politics compared to strict quotas. Second, they call for the design of quota policies that take into account the competitive intensity of our electoral system.

Figure 2 :

 2 Figure 2: Relationship between the share of female candidates in the French legislative elections and voters' stated preference for men in politics Note: This figure presents the relationship between the share of female candidates and the voter preference bias estimated in the linear regression presented in Part 2 of Box 1. Sources: French Ministry of the Interior administrative data on candidates, supplemented by other sources (see Box 1) and Generations and Gender Survey (GGS). Coverage: Candidates in legislative elections between 1993 and 2017. Interpretation: The slope of the line corresponds to the β coefficient of Equation 2. A 10 percentage-point increase in stated preference for men leads to a 2.3 percentage-point decrease in the share of female candidates.

Figure 3 :

 3 Figure 3: Relationship between the proportion of female candidates at legislative elections and the gender pay gap Note: This figure presents the relationship between share of female candidates and the gender wage gap estimated in the linear regression presented in Part 2 of Box 1. Sources: Administrative data on candidates from the French Ministry of the Interior, supplemented by other sources (see Box 1) and DADS, Insee. Coverage: Candidates in legislative elections between 1993 and 2017. Interpretation: The slope of the line corresponds to the β coefficient of Equation 2. A 10 percentage-point increase in the pay gap leads to a nearly 5 percentage-point decrease in the share of female candidates.

  : This figure presents, for each legislative election, the effect of the degree of competition in the district on the gender of candidates, as estimated in the linear regressions presented in Part 3 of Box 1. Sources: Administrative data on candidates from the French Ministry of the Interior, supplemented by other sources (see Box 1) and DADS, Insee. Coverage: Candidates in legislative elections between 1993 and 2017. Interpretation: The dotted vertical line indicates the introduction of the parity law. In the 2002 elections, competitive districts have a proportion of female candidates that is 10 percentage points lower than in non-competitive districts.

			Effect of electoral competition (tight race)
			on district-level share of female candidates
		.05
	Share of female candidates	-.15 -.1 -.05 0
		-.2
		1988	1993	1997	2002	2007	2012	2017
		Figure 4: Difference in candidate share between
			competitive districts by election

Note

The origins of this bias can be multiple: voters' opinion on the role of women in society, discriminatory behaviors against women, etc.

Authors

Thomas Le Barbanchon is an Associate Professor of Economics at Bocconi University. Julien Sauvagnat is an Associate Professor of Finance at Bocconi University.