Tomasz Toczek
email: tomasz.toczek@gipsa-lab.inpg.fr

Dominique Houzet
email: dominique.houzet@inpg.fr

Stéphane Mancini
email: stephane.mancini@grenoble-inp.fr

Efficient Stackless Ray Traversal for Bounding Sphere Hierarchies with CUDA

 We improve on the current stackless traversal methods by increasing memory access locality and accelerating both the primary and secondary ray shooting through specific optimizations achieved at the cost of additional precomputations. Those supplementary steps can be performed on the host and have their results transferred asynchronously on the GPU while the rendering kernel is running, hence being completely hidden.

Introduction

Ray tracing as a rendering method is well known for the quality of the produced output and its adequacy for solving difficult problems such as light transport. This is done by casting numerous rays, the more the better for most rendering algorithms. That is why acceleration structures (AS) are systematically used to speed up the ray traversal itself. Since the time spent building the AS is typically far lesser that the one gained by shooting rays through it, this approach makes sense. For increased scalability, the AS tend to be hierarchical space indexing means build using divide and conquer strategies [START_REF] Vlastimil Havran | Heuristic Ray Shooting Algorithms[END_REF]. Therefore, the most straightforward ways to traverse such AS involve using non-tail recursion, and hence a stack. This hinders their adaptability to GPGPUs, which permit to allocate only very limited per-thread amounts of fast on-chip memories. What is more, nVidia architectures' register memory is not addressable, implying the stack a thread would need has to be located in the scarce shared memory. This is a significant problem to overcome in order to make the oftentimes otherwise embarrassingly parallel ray tracing algorithms GPU friendly.

Several approaches have been proposed so far. Of course, one way to avoid stack problems is to use a flat AS instead of a hierarchical one [START_REF] Purcell | Ray tracing on programmable graphics hardware[END_REF][START_REF] Ralovich | Implementing and analyzing a GPU ray tracer[END_REF]. Such methods suffer however from the well-known [START_REF] Vlastimil Havran | Heuristic Ray Shooting Algorithms[END_REF] drawbacks of non-hierarchical AS, the main one being their inadequacy for handling scenes with spatially variable detail level. When it comes to hierarchical AS traversal on the GPU, essentially two families of methods can be found: those using kd-trees [START_REF] Foley | Kd-tree acceleration structures for a GPU raytracer[END_REF][START_REF] Popov | Stackless kd-tree traversal for high performance GPU ray tracing[END_REF], that is a hierarchical subdivision of space by splitting planes, and those using bounding volume hierarchies (BVH) [START_REF] Carr | Fast GPU ray tracing of dynamic meshes using geometry images[END_REF][START_REF] Günther | Realtime ray tracing on GPU with BVH-based packet traversal[END_REF][START_REF] Thrane | A comparison of acceleration structures for GPU assisted ray tracing[END_REF]. In order to perform the traversal without a stack, one can restart from the root of the tree at each iteration [START_REF] Foley | Kd-tree acceleration structures for a GPU raytracer[END_REF], which is costly in redundant computation, or to some extend try to store additional cues within the nodes to compensate for the missing information [START_REF] Popov | Stackless kd-tree traversal for high performance GPU ray tracing[END_REF], which is costly in memory space and, even worse, bandwidth used during rendering.

Our approach in inspired from [START_REF] Thrane | A comparison of acceleration structures for GPU assisted ray tracing[END_REF] and improves on it on several accounts. We propose to perform supplementary precomputations on the host and transfer their results on the GPU while it is busy ray tracing. While the amount of computations on the host side and the size of the AS are higher, the ray traversal is faster and the kernel memory reference locality is kept reasonably high. This allows to make better use of the texture cache. The sections 2 and 3 contain a detailed description of our method. Ray shooting performance measurements are given in section 4. Finally, practical issues linked to the AS updating and transfer between the host and the device are discussed in section 5. The basic principle of traversal is much the same as exposed by Thrane and Simonsen [START_REF] Thrane | A comparison of acceleration structures for GPU assisted ray tracing[END_REF], and we will use from now on the terminology coined by them. We build a BVH tree (using spherical nodes instead of boxes in our very case), and produce from it a series of lists which will be iterated upon during traversal. How such a list is obtained from the BVH is represented on the figure 1; the list is stored as an array obeying the following rules:

Overall principle

• each element of the list corresponds to a node of the BVH

• for each element corresponding to an internal node: the next element in the array corresponds to its first child

• for each element corresponding to a leaf: the next element corresponds to its immediate sibling in the tree, or, if it has none, to the one of its first ancestor having one (let us call it a super-sibling)

In other words, the elements are in the order given by a depth-first traversal of the BVH tree. In order to be able to skip whole nodes should a ray not intersect them, a relative escape index is stored for each element, pointing to the element's super-sibling (that is, where the depth-first traversal would continue should the current node have no children).

Clearly, this index is 1 if and only if the corresponding node is a leaf, hence enabling us to differentiate bounding spheres from primitives from its value alone. Two special values of the relative escape index, 0 and -1, identify respectively the last primitive, and an internal node with no super-sibling. When such a special escape link is followed, traversal ends (intersection may or may not have been found). In practice, to represent a node, we use an "escape pointer" of 32 bits and a word of 128 bits representing either a bounding sphere geometry or a list of triangle vertex indices. The vertex positions themselves are stored in a separate array shared by all the traversal lists, making each of them comparatively smaller.

The resulting traversal algorithm is quasi-identical to the one given in [START_REF] Thrane | A comparison of acceleration structures for GPU assisted ray tracing[END_REF]:

node <-t r a v e r s a l L i s t H e a d ( d i r ) param <-i n f i n i t y i n t e r s e c t e d T r i a n g l e <-none do r e l a t i v e N e x t = node . r e l a t i v e N e x t i f node . i s T r i a n g l e then i f ( node . i s I n t e r s e c t e d B y T h e R a y && i n t e r s e c t i o n P a r a m e t e r < param ) then param <-i n t e r s e c t i o n P a r a m e t e r i n t e r s e c t e d T r i a n g l e <-node e l s e i f ( node . i s I n t e r s e c t e d B y T h e R a y && i n t e r s e c t i o n P a r a m e t e r < param ) then r e l a t i v e N e x t <-1 node <-node + r e l a t i v e N e x t w h i l e ( r e l a t i v e N e x t > 0 ) r e t u r n ( param , i n t e r s e c t e d T r i a n g l e )

Thrane et al. chose to generate only one such list, and regret the ray traversal is costly in the worst cases. We attempt to work around this by making several lists, by ordering the nodes of the BVH tree along different spatial axes. For each ray, we determine before traversal which list to use by picking the one which matches its direction the best.

There are several ways to pick the node sorting directions, which are illustrated by the figure 2. This gives the following options:

• A single list is constructed (figure 2(a)), the nodes being ordered along an arbitrary direction. This case has been studied by [START_REF] Thrane | A comparison of acceleration structures for GPU assisted ray tracing[END_REF].

• Two lists are constructed (figure 2(b)), the nodes in one being stored in the reverse order of those of the other. The framerate is less dependant on the point of view than on the previous case. We did not study this case because it does not show some of the interesting properties of the following ones. • Six lists (figure 2(c)) constructed by ordering the nodes along the three main axes, in both ways. The overhead due to the redundant geometry storage is becoming rather high, but it can be noticed that this configuration allows for geometry culling. Indeed, assuming the scene geometry is given as a set of one-sided triangles, if a ray direction belongs to a given sextant, it is impossible for it to hit a triangle whose normal belongs to the opposite sextant. Therefore, node redundancy is more like 5 than 6; for each sextant list, approximately 16.67% of the geometry is culled. It is the case we have studied, as a good trade off.

• Eight lists (figure 2(d)). Geometry culling is still possible, but only to an average of 12.25% of primitives par octant list. On the other hand, the optimizations presented in the section 3.1 work better for this division method than for the previous.

The ray shooting process tends to benefit from the fact that the nodes a ray may intersect are stored in compact lists with only one pointer per node, and with a part of the scene geometry already discarded. This increases the locality of the traversal process. What is more, due to the limited size of the texture memory caches on current GPUs, expecting a given geometry node to remain in the texture cache between two consecutive ray launches is rather unrealistic. That is why creating multiple traversal lists is expected to increase memory reference locality despite also increasing significantly the overall memory consumption.

Bounding Sphere Hierarchy construction

For our test we used a top-down BVH generation algorithm very similar to sparse octree generation [START_REF] Glassner | Space subdivision for fast ray tracing[END_REF]. In order to build a node from a set of triangles:

• we determine the tightest axis-aligned bounding box containing all the triangles; let C = (C x , C y , C z ), the barycenter of the bounding box

• the shape of the bounding volume is that of the smallest sphere containing all the triangles and having C as its center

• each triangle big enough compared to the node becomes one of its children

(1) (2) (3) (4)
(5)

secondary ray (a) Per-polygon head computation; in this example, traversal should start from (4) or, even better, ( 5)

(1) (2) (3) (4)
(5) • the other triangles are split in eight groups, depending on the sign of G i -C i , for each i ∈ {x, y, z}, G being the barycenter of a given triangle; the process is then applied recursively on each of the non-empty groups, which are then added as children to the current node Implemented correctly, this algorithm can be quite fast and suited for dynamic scenes with a reasonable poly count. Of course, any other algorithm could have been used for the initial BVH generation.

Partially precomputed traversal

It is interesting to notice that rays sharing some common geometric features may not need to start from the first element of the traversal list for their direction. For instance, primary rays of some part of the screen may all miss all of the primitives. Similarly, secondary rays originating at a given triangle may also systematically miss a given number of consecutive intersection tests, because of the very geometry of the triangle. In this section, we comment on how to handle such cases.

The figure 3 provides 2D illustrations of the methods exposed below, considering a list of 5 primitives roughly ordered along the x axis, numbered from (1) to (5).

Secondary rays

When aiming for interesting shading effects, most of the rays traced are secondary rays. It is therefore important to speed them up to the maximum extent. Sadly, secondary rays are much more tricky to accelerate than primary rays using our approach. However, it is to some degree feasible.

To do so, the heads of the traversal lists can be specifically computed on a per-triangle basis. When a ray bounces on a triangle, those heads are read with the rest of the material information. The algorithm to compute the skipped elements is very similar to ray shooting and hence can be performed on the GPU if necessary. It is demonstrated on a 2D example on the figure 3(a).

The basic idea is to skip all the list elements which are behind the polygon from which a ray is re-emitted (dark gray area on the figure 3(a)). Additionally, for slightly improved efficiency, should also be excluded all the nodes which cannot be hit because of the position of the polygon and the overall direction of the ray (light gray area on the figure 3(a)). How this can be done depends essentially on what direction space partition is used in order to obtain the traversal lists. In all the examples of partitions of the figure 2, skipping the nodes behind a few more planes, depending on which overall direction the ray is going in, does the job. The 2D case is illustrated on figure 3(a), where 2 such additional planes can be seen. In 3D, the number of additional planes is 4 in our case, since we have divided the direction space into sextants (see figure 2(c)).

Theoretically, we should check that any rejected node does not intersect the intersection of all the half-spaces delimited by the planes described in the previous paragraph and oriented towards where re-emitted rays can exist (for a given polygon and a given overall direction). In practice, this is costly and not really necessary. A mostly efficient and inexpensive test is to simply check whether there exists a half-space among the aforementioned ones which a node does not intersect at all. If there is one, the node can safely be skipped.

Primary rays

A similar technique can be applied to primary rays, and works significantly better. That being said, advanced rendering algorithms cast only so much primary rays, and hybrid ray tracing is another way to get a significant speed up in most cases (see for instance [START_REF] Philippe | Hybrid ray tracing -ray tracing using GPU-accelerated image-space methods[END_REF]). However, casting primary rays can be a good way to produce depth of field and fish eye effects.

The basic idea is to divide the screen into a grid, and to compute the heads of the traversal lists for the primary rays of each cell. When using a pinhole camera, a satisfying result can be obtained by using for each cell a set of separating planes as illustrated on the figure 3(b). The resulting effect is superficially similar to frustum culling. Of course, due to the nature of traversal lists, a node which should be culled will not be if it is behind one which cannot. However, this tends to work much better than what is done for secondary rays because the "beam" which is tested for intersections is much narrower.

Ray shooting performances

We measured the ray shooting performances on the 5 scenes of the figure 4. The benchmarking results are summarized on the table 2. The performances given are those obtained with all of the aforementioned optimization enabled. Alternatively, the table 1 shows how performances vary depending on which optimizations have been turned on. The scene used to perform those measurements is the Stanford bunny. Here is a summary of the meaning of the columns:

• Node ordering: the node ordering policy for the traversal lists. Since spheres and triangles are convex objects, their projections onto the sorting axis are segments.

Let us assume the sorting axis is parametrized, and the projection of the nodes is given by the parameter ranges ([x

(i) min , x (i) max ]) i∈[1..n] .
The policy earliest first puts the nodes in ascending x min order, whereas latest last uses the ascending x max order Ray tracing performance summary for different scenes. As polygon count increases, the locality of memory references of the rays of a block is progressively lost, leading to a lesser node traversal rate.

• Back-face culling: enables geometry culling at list construction

• Per-polygon heads computation: computes a set of heads of the traversal lists for each polygon, as described in the section 3.1. It is either disabled, simple (effectively rejecting intersection tests with the primitives located under the surface on which the ray bounces) and regular (further rejection using the additional separating planes)

• Frustum culling: divides the screen space into a grid and computes a different head of traversal list for the primary rays of each cell, as described in section 3.2

Since we used a very simple example rendering algorithm (direct illumination with lambertian shading of triangles), all our test cases' performances are memory bound. Indeed, ray shooting performance is supposed to be approximately a logarithmic function of the triangle count. We used 1D texture caches to store the triangles and vertices, therefore memory reference locality concerns impact the framerate the most. This can be seen on the table 2, where small scenes fitting entirely or almost entirely in the cache offer 10 times higher framerates that their bigger counterparts. It is not unrealistic to think that a cleverer memory organisation scheme, or the use of more complex primitives or shading models -such as those used by real-world ray tracing based renderers -could bring the bottleneck back to the computations. Uncached coalesced references have also been shown as a possible remedy [START_REF] Aila | Understanding the Efficiency of Ray Traversal on GPUs[END_REF]. Such considerations are beyond the scope of this article, however.

The table 1 shows the impact of the optimisations described above, presented on the Stanford bunny scene, with the ground removed to maximize their impact. Since we are still memory bound, the framerate stays virtually the same. It can be seen that they have a heavy incidence on the average traversed nodes per ray count, impacting to as much as 19.8%. In fact, the effects of some parameters, such as the node ordering, are somewhat difficult to assess and call for further investigation in relation with the BVH construction method.

A fair comparison with other methodologies is not straight-forward, since we focused on the traversal itself, not implementing several important rendering related optimizations such as ray shooting by packets [START_REF] Popov | Stackless kd-tree traversal for high performance GPU ray tracing[END_REF] or efficient load balancing [START_REF] Aila | Understanding the Efficiency of Ray Traversal on GPUs[END_REF]. Future prospects include those aspects. We have, however, compared our Comparison between memory transfers and computation times the simpler 1-traversal-list case [START_REF] Thrane | A comparison of acceleration structures for GPU assisted ray tracing[END_REF], improved with each of the optimizations mentionned earlier still working in that context. The gains of our approach range from 5% to 15% on our test scenes, the more complex a scene the higher the gain.

Acceleration structure handling improvements

One of the reasons for the efficiency of the described methodology is the fact the traversal lists are stored as ordered arrays. In this aspect, the traversal lists are similar to AS with implicit pointers. As a consequence, they suffer from the weak points of such structures, i.e. mainly their lack of updatability. However, as can be seen on figure 3, for reasonably sized scenes, transferring the geometry information takes less time than rendering. Since recent NVidia GPU allow for it, those transfers can be done in a nonblocking fashion for the host as well as for the device. Wisely used, the host to device bandwidth permits to modify parts of the traversal lists with little overhead.

It is also worth noting that mechanisms allowing to traverse several lists in a row may be efficiently used. Once a traversal list ends, the head of the next one becomes the current node. Since the parameter of the best intersection is not reseted, the traversal of subsequent lists is in principle faster than that of the original one. Several "layers" can be created in this way; for instance, a static mid-poly one and a dynamic low-poly layer recomputed at each frame. Also, the classical argument according to which vertices of the primitives within a BVH can be updated without recomputing the whole structure still holds for traversal lists, as long as to host keeps enough information to locate the list elements corresponding to a given BVH tree node.

All in all, traversal lists are less rigid than they might first seem.

Conclusion

In this paper, we have shown a series of measures significantly accelerating ray shooting on the GPU at the cost of additional precomputations on the host, compared to classical stack-based algorithms. Raw ray shooting performances have been analysed and commented, and are to our knowledge among the best published so far at equal scene complexity. We did not provide accurate performance measurements for the parts precomputed on the host, mainly because our benches involved various static models bearing little resemblance with polygon distributions of typical dynamic scenes. We did, however, give several ideas to reduce the host computations to the strict necessary. In particular, if a scene can be divided into a static and a dynamic part (as often found in, for instance, video games), the AS for the static part can be precomputed once and for all. Also, we have shown how well-designed DMA usage can reduce both the CPU and GPU loads.

Future work will include studying the compatibility of currently available ray tracing rendering algorithms' optimisations with our ray shooting method, and studying the engine design required to easily and efficiently handle real-time rendering of dynamic scenes with such algorithms.

Figure 1 .

 1 Figure 1. Building a traversal list from a BVH is essentially equivalent to recording the steps of a depth first traversal. On the fig. 1(b), dotted lines represent escape links. They are not shown for the primitives (the leafs), since they always lead to the next element (already pointed by the array). Following escape links leading to nothing ends the traversal.

Figure 2 .

 2 Figure 2. Several interesting partitions of the directions of space

Figure 3 .

 3 Figure 3. Partially computed traversal

Figure 4 .

 4 Figure 4. Our not-so-original test scenes. On a GTX 280 card, at a resolution of 1024 × 1024 and with a single point light, we got on average 31.36 fps for the cubes, 22.87 fps for Suzanne, 6.01 fps for the bunny, 3.03 fps for the Buddha, 3.20 fps for the dragon.

Table 1 Efficiency

 1

	Node order	Back-face culling	Per-polygon head	Frustum culling	FPS	# rays per sec	# traversed nodes per sec.
	latest last	disabled	disabled	enabled 6.81 8.43 M	15.02 G
	latest last	disabled	disabled	disabled 6.81 8.43 M	14.54 G
	latest last	disabled	regular	enabled 6.78 8.40 M	13.99 G
	latest last	disabled	regular	disabled 6.78 8.40 M	16.41 G
	latest last	enabled	disabled	enabled 6.81 8.43 M	13.05 G
	latest last	enabled	disabled	disabled 6.78 8.40 M	14.85 G
	latest last	enabled	regular	enabled 6.82 8.44 M	15.01 G
	latest last	enabled	regular	disabled 6.81 8.43 M	13.92 G
	earliest first	disabled	disabled	enabled 6.78 8.40 M	16.29 G
	earliest first	disabled	disabled	disabled 6.81 8.43 M	13.52 G
	earliest first	disabled	regular	enabled 6.79 8.41 M	15.32 G
	earliest first	disabled	regular	disabled 6.81 8.43 M	14.87 G
	earliest first	enabled	disabled	enabled 6.79 8.40 M	13.75 G
	earliest first	enabled	disabled	disabled 6.78 8.40 M	16.17 G
	earliest first	enabled	regular	enabled 6.81 8.43 M	13.39 G
	earliest first	enabled	regular	disabled 6.81 8.43 M	14.65 G

of several optimization methods on the bunny (without the ground). As most of the proposed optimisations happen at the cost of memory access locality, framerate gains are offset by lesser memory efficiency. Our optimisations permit to reduce the average number of nodes traversed per ray, however.

Table 2

 2

Table 3

 3 6-traversal-list based implementation with

	Scene	Scene copy Frame rendering Ratio
	Cubes	12.6 ms	31.8 ms	39.5 %
	Suzanne	12.7 ms	43.7 ms	29.1 %
	Bunny	18.2 ms	167.0 ms	10.9 %
	Happy Buddha	38.2 ms	329.0 ms	11.6 %
	Dragon	88.5 ms	311.7 ms	28.3 %


Coq Modulo Theory

Pierre-Yves Strub INRIA -Tsinghua University pierre-yves@strub.nu Qian Wang Tsinghua University q-w04@mails.tsinghua.edu.cn Theorem provers like COQ [START_REF]The Coq Proof Assistant Reference Manual -Version 8[END_REF] based on the Curry-Howard isomorphism enjoy a mechanism which incorporates computations within deductions. This allows replacing the proof of a proposition by the proof of an equivalent proposition obtained from the former thanks to possibly complex computations. Adding more power to this mechanism leads to a calculus which is more expressive (more terms are typable), which provides more automation (more deduction steps are hidden in computations) and, most importantly, eases the use of dependent data types in proof development.

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

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

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

Further steps in the direction of integrating first-order theories into the Calculus of Constructions are Stehr's Open Calculus of Constructions (OCC) [START_REF] Stehr | The Open Calculus of Constructions: An equational type theory with dependent types for programming, specification, and interactive theorem proving (part I and II)[END_REF] and Oury's Exten-sional Calculus of Constructions (ECC) [START_REF] Oury | Extensionality in the calculus of constructions[END_REF]. OCC allows the use of an arbitrary equational theory in conversion. ECC can be seen as a particular case of OCC in which all provable equalities can be used in conversion. Unfortunately, strong normalization and decidability of type checking are lost in ECC and OCC.

In [START_REF] Strub | Type Theory and Decision Procedures[END_REF], we defined the Calculus of Inductive Congruence Constructions (CCIC), which was our first answer to the problem of incorporating validity entailment of an equational first-order theory T in the computation mechanism of the Calculus of Inductive Constructions. This calculus partially solved the problem but contained too many ad-hoc restrictions to be implementable in practice. Besides, the procedure could not be invoked to solve goals occurring below eliminators.

Achievements

Our objective is to incorporate in the Calculus of Inductive Constructions, a general mechanism invoking a decision procedure for equality in some first-order theory T , for solving conversion-goals of the form Γ ⇒ U = V . This mechanism should be simple enough to be implementable in practice.

Our theoretical contribution is the definition of a new version of the Calculus of Congruent Inductive Constructions, called COQMT. COQMT integrates in its computational part the entailment relation -via decision proceduresof a first order theory T over equalities. A major technical innovation of COQMT lies in the computational mechanism: goals are sent to the decision procedure together with a set of user hypotheses available from the current context Γ of the proof -a mechanism we call equations extraction.

Not only is the new formulation much simpler, but is is also more general: in particular, we succeeded to remove the ad-hoc restrictions of CCIC [START_REF] Strub | Type Theory and Decision Procedures[END_REF]. In particular, conversion now contains the entire equational theory T , allowing its use below eliminators.

In CCIC, meta-theoretical results were obtained via a complex sequence of definitions and lemmas. By drastically simplifying the definition of CCIC, we were able to carry out the meta-theoretical study of COQMT in a much simpler way than in [START_REF] Strub | Type Theory and Decision Procedures[END_REF]: subject reduction, strong normalization of reduction, logical consistency and decidability of type-checking are all satisfied.

Further, we have formalized CoqMT (without the equations extraction mechanism) in COQ, and already carried out part of its formal meta-theoretical study.

We have implemented COQMT, a new version of COQ based on our work. As of today, this implementation allows the use of decision procedures in the conversion rule. The equations extraction mechanism will be released very soon.

We developed in COQMT the theory of dependent lists as a paradigmatic example. In COQMT, dependent lists definitions are just those of non-dependent lists which can be found in Coq. Likewise, proofs of all basic properties of dependent lists in CoqMT follow from the ones of non-dependent lists in Coq. The full (commented) development can be found in the source release of COQMT (/testsuite/dp/*).

All these developments are available at on the first author website 2 . An extended abstract of the first author results can be found in [START_REF] Strub | Coq modulo theories[END_REF].

Work in progress

When formalizing abstract mathematical structures and properties (abstract algebras, lattices, categories, ...), it is often necessary to use constructions which are not compatible with impredicativity. This problem can be addressed by introducing a cumulative hierarchy of predicative universes, and then define the needed constructions in this hierarchy. Indeed, the current version of COQ has such a type hierarchy, which is similar to the one of [START_REF] Martin-Löf | Intuitionistic Type Theory[END_REF], except for the impredicative universe of propositions situated at the bottom of the hierarchy.

Although the current implementation of COQMT-as an extension of COQ -makes use of this type hierarchy, we did not study the meta-theory of such a calculus. We have strong reasons to believe that the introduction of decision procedures, as done in COQMT, is compatible with the introduction of a type hierarchy. We have recently started this study as a part of the PhD work of the second author, which aims at studying the metatheory of the Coq and CoqMT implementations.

Perpectives

The extraction mechanism under implementation in CO-QMT will allow much more than described in Sections 1 and 2: using extracted equations below eliminators and within the reduction mechanism will be possible.

2 http://strub.nu/research/coqmt/ In the theoretical model, however, reduction modulo T cannot use extracted equations, since otherwise potential user's inconsistencies could propagate and compromise the logical consistency of the calculus. A work-around would be to only use, during reduction, a subset of extracted equations consistent by construction. Although the idea is quite straightforward, the many dependencies between conversion, reduction modulo and consistency of extracted equations make it difficult to get a definition which meets our requirement of simplicity.

Further, we plan to extend the extraction mechanism (currently restricted to equations) to arbitrary first-order propositions, possibly using other predicates (like the ordering on natural numbers) or universal quantification.

Finally, we plan to define a more general calculus where decision procedures are seen as heuristics tagging the terms of the calculus with non-intrusive conversion markers. Such a calculus would capture COQMT, allow the use of incomplete decision procedures, and lead to a more elegant implementation of COQMT.

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

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


Patrick Chames
email: patrick.chames@inserm.fr

Brigitte Kerfelec

Daniel Baty

Therapeutic antibodies for the treatment of pancreatic cancer

Keywords: Antibodies, therapy, pancreatic, bispecific, clinical trials

Pancreatic cancer is a devastating disease with the worst mortality rate and an overall 5-year survival rate lower than 5%. In the United States, this disease is the fourth leading cause of death and represents 6% of all cancer related deaths. Gemcitabine, the current standard firstline treatment offers marginal benefits to patients in terms of symptom control and prolongation of life. Since 1996, about 20 randomized phase III trials have been performed to improve the efficacy of gemcitabine with little success regarding a significant improvement in survival outcomes. The need for novel therapeutic strategies such as target therapy is obvious.

Monoclonal antibodies have finally come of age as therapeutics and several molecules are now approved for cancer therapies. This review aims at giving a general view on the clinical results obtained so far by antibodies for the treatment of pancreatic cancer and describes the most promising avenues toward a significant improvement in the treatment of this frustrating disease.

Introduction

Pancreatic cancer

Pancreatic cancer is a devastating disease with the worst mortality rate and an overall 5-year survival rate lower than 5%. Although accounting for only 3% of all cancers, this disease is the fourth leading cause of death and represents 6% of all cancer related deaths. In the United States, the overall incidence is about 8-10 cases per 100,000 persons/year and rises slowly over the years [START_REF] Jemal | Cancer statistics[END_REF]. Pancreatic cancer remains one of the most difficult to treat due to late initial diagnosis and to intrinsic resistance to conventional treatments. About 50% of patients have distant disease at the time of diagnosis (locally advanced stage) and in 40% the tumor has spread (metastatic stage). Risk factors have been identified [START_REF] Klapman | Early detection of pancreatic cancer: why, who, and how to screen[END_REF], molecular pathogenesis has been elucidated, but advances in early detection and efficient treatments remain rather disappointing despite tremendous efforts. The majority of pancreatic tumors (95%) is adenocarcinoma and mainly develops from exocrine cells. They are characterized by an aggressive behavior with a fast progression rate that makes them highly metastatic, by a dense fibrotic stroma surrounding a minor population of cancerous cells and by an early and vascular invasive growth. This reactive stroma is composed of extracellular matrix proteins (collagen, fibronectin), myofibroblastic pancreatic stellate cells, immune cells, cytokines, growth factors, proteases and vessels.

Current treatments

There is consensus on the fact that surgical removal of the tumor represents the best option for pancreatic cancer treatment; to be resectable, tumors need to be small and strictly localized to pancreas without invasion into surrounding organs and evidence of metastasis. However, only 15-20% of all patients are candidates for potentially curative surgery. Depending on the tumor localization, pancreaticoduodenectomy, distal or total pancreatectomy can be performed.

However, even with an optimal curative surgery, metastases often occur. Median survival time without evidence of recurrent disease is 21.2 months after resection [START_REF] Helm | Outcomes following resection of pancreatic adenocarcinoma: 20-year experience at a single institution[END_REF].

For locally advanced or metastatic disease, treatment is still palliative rather than curative, and chemotherapy remains the only option. Since its approval in 1997, gemcitabine is the current standard first-line treatment. It was shown by Burris and colleagues (4) to improve median disease-free survival and overall survival (OS) rate at 5 years. Since 1996, about 20 randomized phase III trials have been performed to improve the efficacy of gemcitabine with little success regarding a significant improvement in survival outcomes (for review see [START_REF] Cartwright | Cancer of the pancreas: are we making progress? A review of studies in the US Oncology Research Network[END_REF][START_REF] Nieto | Metastatic pancreatic cancer 2008: is the glass less empty?[END_REF][START_REF] Heinemann | Accomplishments in 2008 in the treatment of metastatic pancreatic cancer[END_REF]).

A small clinical benefit is evidenced for the erlotinib/gemcitabine and platinum/gemcitabine combinations but it must be balanced by increased toxicity. Up to now, the only combination approved by FDA is the gemcitabine/erlotinib combination (Tarceva®) which increased the median overall survival from 6 to 6.4 months [START_REF] Moore | Erlotinib plus gemcitabine compared with gemcitabine alone in patients with advanced pancreatic cancer: a phase III trial of the National Cancer Institute of Canada Clinical Trials Group[END_REF][START_REF] Senderowicz | Erlotinib/gemcitabine for first-line treatment of locally advanced or metastatic adenocarcinoma of the pancreas[END_REF].

New potential targets

Advances in the understanding of pancreatic cancer biology and of the mechanisms by which it eludes conventional cytotoxic therapies should lead to the identification of new potential targets. Cancer stem cells (CSC) might be one of them. Tumors are constituted by differentiated cells that have limited proliferative potential and by a small subset of cancer cells responsible for tumor initiation and propagation [START_REF] Reya | Stem cells, cancer, and cancer stem cells[END_REF][START_REF] Visvader | Cancer stem cells in solid tumours: accumulating evidence and unresolved questions[END_REF]. In pancreatic cancer, CSC represent 0.2 to 0.8% of all cancer cells and they are characterized by cell surface markers CD44, CD24, ESA (epithelial specific antigen) [START_REF] Li | Identification of pancreatic cancer stem cells[END_REF]. CSC have been shown to be resistant to conventional chemotherapy and radiation [START_REF] Simeone | Pancreatic cancer stem cells: implications for the treatment of pancreatic cancer[END_REF], which might explain the poor therapeutic results of current therapies. The contribution of tumor/stroma interactions in pancreatic cancer progression has also been recently emphasized [START_REF] Hwang | Cancerassociated stromal fibroblasts promote pancreatic tumor progression[END_REF][START_REF] Hernandez-Munoz | Pancreatic ductal adenocarcinoma: cellular origin, signaling pathways and stroma contribution[END_REF]. Promising results in a phase II trial have been obtained by combining gemcitabine with nab-paclitaxel [START_REF] Saif | Phase II clinical trial of paclitaxel loaded polymeric micelle in patients with advanced pancreatic cancer[END_REF]. This compound which is an anti-mitotic agent increased the potency of gemcitabine by altering the stroma surrounding the tumor. Thus, the need for novel therapeutic strategies such as target therapy in pancreatic cancer patients is obvious. Recent years have seen the approval of several therapeutic antibodies for cancer therapy (Table 1), some of them leading to very significant therapeutic effects [START_REF] Chames | Therapeutic antibodies: successes, limitations and hopes for the future[END_REF].

Disappointments met with the first murine therapeutic molecules that were rapidly eliminated by the patient's immune system and that were not interacting properly with human receptors of the patient's effector cells have been replaced with significant clinical outcomes achieved by chimeric (human IgG bearing murine variable domains), humanized (human IgG bearing murine hypervariable loops) and fully human antibodies [START_REF] Chames | Therapeutic antibodies: successes, limitations and hopes for the future[END_REF]. Therapeutic antibodies have been shown to rely on various modes of action, including direct blocking of a ligand or a receptor, induction of apoptosis by receptor clustering, complement-dependent cytotoxicity, or cell-mediated cytotoxicity/phagocytosis. The last generation of therapeutic antibodies has been engineered to strongly interact with activating receptors such as FcRIIIA expressed on NK cells. Modifications have targeted some residues of the Fc fragment involved in the interaction with Fc receptors, or the nature of the Fc glycosylation shown to greatly influence the affinity of the receptors for the IgG. More recently, bispecific antibodies capable of simultaneously binding to a tumor antigen and to CD3 on T cells and thereby redirecting polyclonal T cells to tumor cells have led to exciting clinical results [START_REF] Chames | Bispecific antibodies for cancer therapy[END_REF][START_REF] Chames | Bispecific antibodies for cancer therapy: the light at the end of the tunnel?[END_REF].

The aim of this paper is to review the most recent studies involving the use of antibodies for the treatment of pancreatic cancer.

Clinical trials involving antibodies

Angiogenesis

Vascular endothelial growth factor (VEGF)

Angiogenesis provides the required substrates for tumor growth and dissemination. Targeting angiogenesis is attractive because in theory it can reduce cancer progression. VEGF-A (or VEGF) is the predominant member of the VEGF family. VEGF receptor is similar to EGFR because after binding to its ligand, VEGF receptor forms a dimer, and the tyrosine kinase becomes autophosphorylated and amplifies the initial signal by activating the intracellular pathways, such as MAPK and PI3K [START_REF] Xie | Transcriptional anti-angiogenesis therapy of human pancreatic cancer[END_REF]. VEGF exerts most of its neoangiogenic effects through VEGF-R2 [START_REF] Tabernero | The role of VEGF and EGFR inhibition: implications for combining anti-VEGF and anti-EGFR agents[END_REF]. VEGF is expressed in 88% to 93% of the patients with pancreatic adenocarcinoma [START_REF] Niedergethmann | High expression of vascular endothelial growth factor predicts early recurrence and poor prognosis after curative resection for ductal adenocarcinoma of the pancreas[END_REF]. Moreover, VEGF presence in tumor samples correlates with tumor size, and is also a predictor of early recurrence after surgery, development of liver metastasis, poor prognosis, and cancer-related death [START_REF] Holloway | Selective blockade of vascular endothelial growth factor receptor 2 with an antibody against tumor-derived vascular endothelial growth factor controls the growth of human pancreatic adenocarcinoma xenografts[END_REF].

Bevacizumab is a recombinant humanized anti-VEGF-A monoclonal antibody that prevents binding to both VEGFR (Table 1). This antibody has proven clinical benefit in metastatic colon, breast, and non-small cell lung cancer. Bevacizumab decreases lymphangiogenesis and neovascularization in vivo and is expected to increase the delivery of chemotherapy to the tumor in pancreatic cancer. Kindler and colleagues reported the results of a phase II trial of bevacizumab plus gemcitabine in 52 patients with metastatic pancreatic cancer. Partial responses were observed in 21% of patients, the median survival time was 8.8 months, and the 1-year survival rate was 29% [START_REF] Kindler | Phase II trial of bevacizumab plus gemcitabine in patients with advanced pancreatic cancer[END_REF]. The major side effect with bevacizumab therapy in pancreatic cancer is bleeding and perforation. Therefore, it was not recommended in patients with tumors invading the duodenum or other organs. These data prompted the CALGB to conduct a double-blind, placebo-controlled randomized phase III trial (CALGB 80303) of gemcitabine plus bevacizumab versus gemcitabine plus placebo in 602 advanced pancreatic cancer patients. Gemcitabine was given in the standard fashion and bevacizumab was given at a dose of 10 mg/kg on days 1 and 15 of each 28-day cycle. Unexpectedly, the median OS times were 5.7 months and 6.0 months for gemcitabine plus bevacizumab and gemcitabine plus placebo, respectively [START_REF] Kindler | A double-blind, placebo-controlled, randomized phase III trial of gemcitabine (G) plus bevacizumab (B) versus gemcitabine plus placebo (P) in patients (pts) with advanced pancreatic cancer (PC): A preliminary analysis of Cancer and Leukemia Group B (CALGB)[END_REF]. Finally a phase III Trial of bevacizumab in combination with gemcitabine and erlotinib involving 607 patients with metastatic pancreatic cancer demonstrated that the addition of bevacizumab to gemcitabine-erlotinib does not lead to a statistically significant improvement in OS in patients, although progression free survival was significantly longer in the bevacizumab group compared with placebo [START_REF] Van Cutsem | Phase III trial of bevacizumab in combination with gemcitabine and erlotinib in patients with metastatic pancreatic cancer[END_REF].

Unfortunately, it appears that bevacizumab does not lead to clinical benefits for pancreatic cancer treatment, probably because other pro-angiogenic factors including insulin-like growth factor-I, hepatocyte growth factor, fibroblast growth factor, platelet-derived growth factor, and TGF- are often overexpressed by pancreatic cancer cells.

Integrin 5β1

Integrins form a superfamily of widely expressed transmembrane glycoprotein receptors for extracellular matrix ligands, such as fibronectin, vitronectin, laminin, collagens, and other plasma membrane proteins, and are involved in the regulation of a broad variety of cellular processes, including embryogenesis, inflammation, bone metabolism, apoptosis, cell proliferation, angiogenesis, and tumor metastasis. Integrin alpha5beta1, the principal fibronectin receptor, is an important survival factor, playing a key role in angiogenesis.

Endothelial cell expression of the 51 integrin and its ligand fibronectin are both upregulated during tumor angiogenesis [START_REF] Ricart | Volociximab, a chimeric monoclonal antibody that specifically binds alpha5beta1 integrin: a phase I, pharmacokinetic, and biological correlative study[END_REF]. Volociximab, a high-affinity IgG4 chimeric monoclonal antibody, has lead to a very efficient apoptosis of vascular endothelial cells, angiogenesis and tumor growth inhibition in preclinical studies, independently of the VEGF pathway [START_REF] Ramakrishnan | Preclinical evaluation of an anti-alpha5beta1 integrin antibody as a novel anti-angiogenic agent[END_REF]. Volociximab is currently being tested in a phase II study in combination with gemcitabine in 40 patients with metastatic pancreatic cancer. Preliminary results (ASCO 2008 Gastrointestinal Cancers Symposium, abstract 142) indicate 3 partial remissions and 17 stable diseases. The treatment was well tolerated and these results are thus encouraging.

Tumor targeting

Epidermal growth factor receptor (EGFR)

The EGFR, also known as ErbB1 or HER1, is a 170 kDa protein belonging to the fourmember ErbB1-4 family of transmembrane tyrosine kinase growth factor receptors. Upon binding to a number of ligands conformational alterations occur in the single chain receptor, allowing dimerization or oligomerization with other EGFR molecules or other members of the ErbB family, leading to autophosphorylation and signal transduction. EGFR is expressed in 30% to 89% of pancreatic cancers assayed by immunohistochemistry techniques [START_REF] Fjallskog | Expression of molecular targets for tyrosine kinase receptor antagonists in malignant endocrine pancreatic tumors[END_REF][START_REF] Tobita | Epidermal growth factor receptor expression in human pancreatic cancer: Significance for liver metastasis[END_REF].

Cetuximab is an anti EGFR therapeutic antibody already approved for the treatment of colorectal cancer (Table 1). This antibody has also been investigated in pancreatic cancer, in combination with the standard gemcitabine agent. In a phase II study with chemotherapy naïve patients with advanced disease, 41 patients with EGFR immunostain-positive tumors (6 locally advanced, 34 metastatic) were treated with cetuximab (initial dose 400 mg/m2, followed by 250 mg/m2 weekly) and gemcitabine. Five patients (12.5%) achieved a partial response and 26 patients (63.4%) had stable disease. The median time to progression was 3.8 months, and the median OS duration was 7.1 months. The 1-year survival rate of 31.7% compared favorably to 18% with gemcitabine alone in historical series. The combination was well tolerated with the most commonly reported toxicities of all grades as follows: rash (87.8%), nausea (61.0%), weight loss (58.5%), and diarrhea (53.7%) [START_REF] Xiong | Cetuximab, a monoclonal antibody targeting the epidermal growth factor receptor, in combination with gemcitabine for advanced pancreatic cancer: a multicenter phase II Trial[END_REF]. This small but significant improvement warranted further studies and two trials were launched. The SWOG S0205 study was a randomized phase III trial of gemcitabine with or without cetuximab in 766 patients with locally advanced or metastatic pancreatic adenocarcinoma. The data, presented in 2007, did not evidence a statistically significant difference in progression free survival (PFS) (3 vs 3.5 months, p = 0.14), and OS duration (6 vs 6.5 months, p = 0.058), in the gemcitabine alone vs gemcitabine and cetuximab groups, respectively [START_REF] Philips | Phase III study of gemcitabine [G] plus cetuximab [C] versus gemcitabine in patients [pts] with locally advanced or metastatic pancreatic adenocarcinoma [PC]: SWOG S0205 study[END_REF]. The second study (ECOG) was a randomized phase II trial, in which 87 eligible patients with metastatic pancreatic cancer were randomized to the Murren regimen of docetaxel and irinotecan with or without cetuximab. Unexpectedly, the patients treated with cetuximab had shorter median survival duration (5.3 months) compared to the placebo group (6.5 months). A very short post-progression survival was observed in the cetuximab arm, not well explained by the data.

The toxicity of this regimen was high, even without cetuximab. Grade 3 or 4 diarrhea was observed in 47% of patients in the three drug arm and the rate of treatment-related death was 4% [START_REF] Burtness | Phase II ECOG trial of irinotecan/docetaxel with or without cetuximab in metastatic pancreatic cancer: Updated survival and CA19-9 results[END_REF]. Thus, unfortunately, no significant improvements could be demonstrated using cetuximab. Of note, another anti-EGFR antibody, matuzumab, has demonstrated some activity in clinical trials. A phase I study assessed the safety and potential benefit of combined treatment with matuzumab and standard-dose gemcitabine [START_REF] Graeven | Phase I study of the humanised anti-EGFR monoclonal antibody matuzumab (EMD 72000) combined with gemcitabine in advanced pancreatic cancer[END_REF]. Seventeen chemotherapynaive advanced pancreatic adenocarcinoma patients received escalating doses of matuzumab (400 mg weekly, 800 mg biweekly, or 800 mg weekly) and gemcitabine. Severe treatmentrelated toxicities were limited to grade 3 neutropenia, leucopenia, and decreased white blood cell count. Common study drug-related adverse events were skin toxicities and fever.

Matuzumab inhibited phosphorylated EGFR and affected receptor-dependent signaling and transduction; effects were seen even in the lowest-dose group. Partial response (PR) or stable disease occurred in eight of 12 evaluated patients (66.7%), with three PRs among six evaluated patients in the group receiving 800 mg weekly. Matuzumab was thus well tolerated and the combination may have enhanced activity. Panitumumab is a fully human anti-EGFR that prevents EGF and TGF- from binding to the receptor (Table 1). This antibody has yielded exciting preclinical data, including the complete eradication of established human tumors (derived from the human vulvar epidermoid carcinoma cell line A431) as large as 1.2 cm 3 [START_REF] Yang | Eradication of established tumors by a fully human monoclonal antibody to the epidermal growth factor receptor without concomitant chemotherapy[END_REF]. A phase II clinical trial comparing gemcitabine plus erlotinib with or without panitumumab is currently ongoing in the USA (NCT00550836).

Human Epidermal growth factor Receptor 2 (HER2)

HER2 (or ErbB2) is another member of the EGFR family. HER2 is involved in signal transduction pathways leading to cell growth and differentiation, and is overexpressed in a number of cancers, including breast and pancreatic cancer. Up to 26% of pancreatic tumor specimens express HER2 as shown by immunohistochemistry [START_REF] Safran | Overexpression of the HER-2/neu oncogene in pancreatic adenocarcinoma[END_REF]. Trastuzumab is a neutralizing humanized antibody directed against the extracellular domain of the HER2 receptor (Table 1). The therapeutic effect of trastuzumab is well documented in breast cancer and has been ascribed to cell cycle arrest and induction of apoptosis as well as induction of antibody-dependent cellular cytotoxicity (ADCC) against HER2-overexpressing tumor cells [START_REF] Garnock-Jones | Trastuzumab: A review of its use as adjuvant treatment in human epidermal growth factor receptor 2 (HER2)-positive early breast cancer[END_REF]. Based on this rational and on several encouraging pre-clinical results, a phase I clinical trial enrolling 34 patients with metastasized HER2 overexpressing (grade 2-3) pancreatic cancer was launched. A combination of trastuzumab and gemcitabine resulted in partial response rates of 6%, and 41% of patients showed a >50% reduction of the tumor marker CA19-9 [START_REF] Safran | Herceptin and gemcitabine for metastatic pancreatic cancers that overexpress HER-2/neu[END_REF]. A modest improvement of the median survival in patients with metastatic pancreatic cancer suggested there may be a modest benefit of trastuzumab treatment for some patients. A larger phase II trial combining trastuzumab and capecitabine should start soon [START_REF] Mihaljevic | A prospective, nonrandomized phase II trial of Trastuzumab and Capecitabine in patients with HER2 expressing metastasized pancreatic cancer[END_REF].

Interestingly, a combination of anti-HER1 and anti-HER2 antibodies was tested in preclinical studies and demonstrated a significant improvement of survival and tumor regression in mice treated with trastuzumab plus cetuximab in first and second-line treatments, compared with gemcitabine. These results warrant further clinical trials [START_REF] Larbouret | Combined cetuximab and trastuzumab are superior to gemcitabine in the treatment of human pancreatic carcinoma xenografts[END_REF].

Mesothelin

Mesothelin is a differentiation antigen whose expression in normal human tissues is limited to mesothelial cells lining the pleura, pericardium and peritoneum [START_REF] Chang | Molecular cloning of mesothelin, a differentiation antigen present on mesothelium, mesotheliomas, and ovarian cancers[END_REF]. The mesothelin gene encodes a precursor protein of 71 kDa that is processed to a 31 kDa shed protein called megakaryocyte potentiating factor (MPF) and a 40 kDa fragment, mesothelin, that is attached to the cell membrane by a glycosyl-phosphatidylinositol (GPI) anchor. Mesothelin binds the mucine MUC-16, also called CA-125 [START_REF] Hassan | Mesothelin targeted cancer immunotherapy[END_REF], but little is known about its function. It has been shown that mesothelin is highly expressed in several human cancers, including virtually all mesotheliomas and pancreatic adenocarcinomas, and approximately 70% of ovarian cancers and 50% of lung adenocarcinomas. Argani and colleagues were the first to show mesothelin expression in pancreatic ductal adenocarcinoma but not in normal pancreas [START_REF] Argani | Mesothelin is overexpressed in the vast majority of ductal adenocarcinomas of the pancreas: identification of a new pancreatic cancer marker by serial analysis of gene expression (SAGE)[END_REF]. In addition, mesothelin mRNA expression was present in 4 of 4 resected primary pancreatic cancers and all 60 resected primary adenocarcinomas were mesothelin positive as shown by immunohistochemistry. These results were confirmed by Hassan and colleagues who showed that mesothelin was expressed in all 18 cases of pancreatic adenocarcinomas examined but absent in normal pancreas and in chronic pancreatitis [START_REF] Hassan | Mesothelin is overexpressed in pancreaticobiliary adenocarcinomas but not in normal pancreas and chronic pancreatitis[END_REF]. Mesothelin is also highly expressed in other adenocarcinomas of the biliary tree such as gallbladder cancer and tumours of the common bile duct [START_REF] Swierczynski | Analysis of novel tumor markers in pancreatic and biliary carcinomas using tissue microarrays[END_REF]. This tumor marker is being evaluated for targeted therapy. SS1P is a recombinant immunotoxin consisting of a mouse anti-mesothelin disuldidestabilized Fv linked to a truncated Pseudomonas exotoxin (dsFv-PE38) that mediates cell killing upon internalization. Pre-clinical studies have shown that SS1P is cytotoxic to cell lines expressing mesothelin and causes complete regression of mesothelin expressing tumour xenografts in nude mice [START_REF] Hassan | Mesothelin: a new target for immunotherapy[END_REF]. This construct was further tested in phase I clinical trial. Out of the 34 patients treated (20 mesothelioma, 12 ovarian cancer and 2 pancreatic cancer) 4 had minor response and 19 had stable disease including complete resolution of ascites in two patients [START_REF] Hassan | Phase I study of SS1P, a recombinant anti-mesothelin immunotoxin given as a bolus I.V. infusion to patients with mesothelin-expressing mesothelioma, ovarian, and pancreatic cancers[END_REF]. The immunotoxin was well tolerated and led to some clinical resulted, warranting further clinical trials.

MORAb-009 is a high-affinity chimeric (mouse/human) IgG1 with high affinity and specificity for mesothelin. The heavy and light chain variable regions of mouse antimesothelin scFv (obtained by panning on mesothelin-positive cells a phage display library made from an immunized mouse) were grafted with human IgG1 and  constant regions.

MORAb-009 was shown to prevent adhesion of mesothelin-bearing tumor cells to MUC16

positive cells and to elicit cell-mediated cytotoxicity on mesothelin-bearing tumor cells.

Treatment that included MORAb-009 in combination with chemotherapy led to a marked reduction in tumor growth in nude mice compared to chemotherapy or MORAb-009 treatment alone [START_REF] Hassan | Preclinical evaluation of MORAb-009, a chimeric antibody targeting tumor-associated mesothelin[END_REF]. This antibody is now being evaluated in clinical trials. A phase I study of MORab-009 on 24 mesothelioma, pancreatic and ovarian cancer patients gave encouraging results.

MORAb-009 was well tolerated and 6 subjects demonstrated stable disease warranting additional therapy [START_REF] Laheru | A phase I study of MORab-009, a monoclonal antibody against mesothelin, in mesothelioma, pancreatic and ovarian cancer[END_REF]. Given the favorable safety profile and possibility of clinical benefit, a phase II study of the efficacy of MORAb-009 with gemcitabine in unresectable pancreatic cancer is underway.

Carcinoembryonic antigen (CEA, CEACAM5)

Carcinoembryonic antigen (CEA), a glycoprotein, is a tumor-associated antigen and elevated levels are detected in the cell membrane of tumors derived from epithelium. CEA is overexpressed in over 90% of pancreatic cancers [START_REF] Yamaguchi | Pancreatoduodenal carcinoma: a clinicopathologic study of 304 patients and immunohistochemical observation for CEA and CA19-9[END_REF]. Binding of antibodies to CEA has been shown to inhibit cell migration, cell invasion, cell adhesion and to have anti metastatic effect in vivo [START_REF] Blumenthal | Inhibition of adhesion, invasion, and metastasis by antibodies targeting CEACAM6 (NCA-90) and CEACAM5 (Carcinoembryonic Antigen)[END_REF]. In a phase I/II clinical trial, Sultana and colleagues have enrolled 25 patients to assess the safety and efficacy of I 131 -labelled anti-CEA chimeric (sheep/human) antibody KAb201 in patients with unresectable pancreatic adenocarcinoma [START_REF] Sultana | Randomised Phase I/II trial assessing the safety and efficacy of radiolabelled anti-carcinoembryonic antigen I(131) KAb201 antibodies given intra-arterially or intravenously in patients with unresectable pancreatic adenocarcinoma[END_REF]. In this approach based on the use of a monoclonal antibodies conjugated with radionuclides, the radiation component has a bystander effect, i.e. killing of adjacent unbound cells, while lessening toxicity to normal tissues. The results demonstrated tumor targeting, with hematological toxicity of varying degrees. Survival and efficacy data was comparable to the median survival and efficacy seen with single agent gemcitabine. An antigenic responses directed to the chimeric antibody was observed and might constitute a limitation for repeated dosing.

Insulin-like Growth Factor 1 Receptor (IGF-1R)

Cixutumumab (IMC-A12) is a fully human monoclonal antibody (IgG1) against type 1 insulin like growth factor receptor (IGF-1R). The IGF-1R and its ligands IGF-1 and IGF-2 have been implicated as playing key roles in the development, maintenance, and progression of cancer [START_REF] Rowinsky | IMC-A12, a human IgG1 monoclonal antibody to the insulin-like growth factor I receptor[END_REF]. IGF-1R signaling is known to activate both the PI3K/Akt and the MAP kinase pathways leading to increased tumor cell survival and proliferation, respectively. By blocking this signaling, cixutumumab has demonstrated encouraging results in preclinical studies, with significant growth inhibition of breast, renal, and pancreatic tumors, and a marked increase in apoptotic tumor cells in antibody-treated animals [START_REF] Burtrum | A fully human monoclonal antibody to the insulin-like growth factor I receptor blocks ligand-dependent signaling and inhibits human tumor growth in vivo[END_REF]. A phase I/II clinical trial is currently comparing the efficiency of gemcitabine and erlotinib with or without cixutumumab for the treatment of patients with metastatic pancreatic cancer (NCT00617708).

AMG 479 is also a fully human monoclonal IgG1 antibody that binds IGF-1R without crossreacting with the closely related insulin receptor. AMG 479 has been shown to inhibit binding of IGF-1 and IGF-2 to the receptor [START_REF] Beltran | AMG 479, a fully human anti-insulin-like growth factor receptor type I monoclonal antibody, inhibits the growth and survival of pancreatic carcinoma cells[END_REF]. As a single agent, AMG 479 strongly inhibited the growth of pancreatic carcinoma xenografts, and long-term treatment was associated with reduced IGF-IR signaling activity and expression. The combination of AMG 479 with gemcitabine resulted in additive inhibitory activity both in vitro and in vivo. A phase II study of AMG 479 as single therapy in advanced carcinoid and pancreatic neuroendocrine tumors is currently on going (NCT01024387).

Pre-clinical studies

Several other tumor targets have been explored as marker for antibody therapy of pancreatic cancer.

Nonspecific cross-reacting antigen (NCA, CEACAM6)

CEACAM6 ( CD66c) is an integral member of the CEA family. It is a cell surface glycoprotein composed of an extracellular region containing three immunoglobulin-like domains (344 residues) and linked to the plasma membrane via a glycophosphoinositolanchor. CEACAM6 is capable of homophilic and/or heterophilic adhesion to other CEACAM family members [START_REF] Oikawa | Extracellular N-domain alone can mediate specific heterophilic adhesion between members of the carcinoembryonic antigen family, CEACAM6 and CEACAM8[END_REF]. CEACAM6 is expressed on normal human epithelial and myeloid cells but the level of expression is 1 to 2 log lower compared with expression in malignant tissue [START_REF] Scholzel | Carcinoembryonic antigen family members CEACAM6 and CEACAM7 are differentially expressed in normal tissues and oppositely deregulated in hyperplastic colorectal polyps and early adenomas[END_REF]. Several gene expression profiling studies on pancreatic ductal adenocarcinoma (PDA) cell lines [START_REF] Han | Identification of differentially expressed genes in pancreatic cancer cells using cDNA microarray[END_REF][START_REF] Ryu | Relationships and differentially expressed genes among pancreatic cancers examined by large-scale serial analysis of gene expression[END_REF]) and human PDA biopsy samples [START_REF] Iacobuzio-Donahue | Highly expressed genes in pancreatic ductal adenocarcinomas: a comprehensive characterization and comparison of the transcription profiles obtained from three major technologies[END_REF][START_REF] Iacobuzio-Donahue | Exploration of global gene expression patterns in pancreatic adenocarcinoma using cDNA microarrays[END_REF] have shown a 20-to 25-fold overexpression of CEACAM6 compared with normal pancreatic ductal epithelial cells [START_REF] Han | Identification of differentially expressed genes in pancreatic cancer cells using cDNA microarray[END_REF][START_REF] Iacobuzio-Donahue | Exploration of global gene expression patterns in pancreatic adenocarcinoma using cDNA microarrays[END_REF]. CEACAM6 is also overexpressed in several other epithelial carcinomas (colon, breast, ovarian and non-small cell lung cancers) [START_REF] Scholzel | Carcinoembryonic antigen family members CEACAM6 and CEACAM7 are differentially expressed in normal tissues and oppositely deregulated in hyperplastic colorectal polyps and early adenomas[END_REF]. Based on these data, CEACAM6 appears as an attractive pancreatic tumor marker. However, expression of CEACAM6 protein has been noted in a variety of normal human tissues, including granulocytes and antigen-dependent toxicity cannot be easily tested in preclinical model since rodents do not express CEACAM6.

A recent interesting preclinical study has evaluated the potential of an immunoconjugate between a chimeric (mouse/human) anti-CEACAM6 IgG and an anti-mitotic agent, maytansinoid (DM1), in Cynomolgus macaques [START_REF] Strickland | Preclinical evaluation of carcinoembryonic cell adhesion molecule (CEACAM) 6 as potential therapy target for pancreatic adenocarcinoma[END_REF]. The authors first confirmed the expression of CEACAM6 in > 90% of invasive pancreatic adenocarcinomas as well as in intraepithelial neoplastic lesions by tissue macroarrays and obtained a marked tumor growth inhibition in xenografted mice. As expected, the treatment induced neutropenia in macaques, as a result of antigen-dependent toxicity. However this phenomenon was fully reversible and the authors observed a repopulation from the pool of CEACAM6-negative, lineage-committed progenitors in a time span shorter than typically seen after bone marrow ablation in the course of conventional, non-targeted cytotoxic chemotherapy. Beside this rapid but reversible neutrophils depletion, no adverse effects were seen, which encourages further studies of this immunoconjugate.

CEACAM6 has also been targeted in another preclinical study for the treatment of pancreatic ductal adenocarcinoma. The authors have produced a humanized anti-CEACAM6 scFv fragment and PEGylated the fragment through the introduction of a cysteine in the linker to increase serum half life [START_REF] Riley | Design and activity of a murine and humanized anti-CEACAM6 single-chain variable fragment in the treatment of pancreatic cancer[END_REF]. In vivo, the fragment inhibits tumor growth in a murine xenograft model, through inhibition of angiogenesis and proliferation. It was shown to specifically induce targeted tumor cell apoptosis without dependence on antibody-dependent cellular cytotoxicity, complement dependent cytotoxicity, or conjugation with a cytotoxic agent. The proposed mode of action was high affinity binding to CEACAM6, which enhances the disruption of domain 1 homophilic dimer with consequent functional inhibition of CEACAM6, known to play an important role in apoptosis resistance in conditions where cells lose contact with the extra cellular matrix [START_REF] Ordonez | Human carcinoembryonic antigen functions as a general inhibitor of anoikis[END_REF]. These promising results justify clinical trials.

Epithelial cell adhesion molecule (EpCAM)

EpCAM is a glycosylated, 30-to 40-kDa type I membrane protein, which is expressed in a variety of human epithelial tissues, cancers, and progenitor and stem cells. EpCAM is comprised of an extracellular domain with epidermal growth factor (EGF)-and thyroglobulin repeat-like domains, a single transmembrane domain, and a short 26-amino acid intracellular domain. EpCAM in normal cells is predominantly located in intercellular spaces where epithelial cells form very tight junctions. It has, therefore, been speculated that EpCAM on normal epithelia is sequestered and, therefore, much less accessible to antibodies than EpCAM in cancer tissue, where it is homogeneously distributed on the cancer cell surface.

Moreover, EpCAM is expressed on essentially all human adenocarcinoma, on certain squamous cell carcinoma, on retinoblastoma, and on hepatocellular carcinoma [START_REF] Baeuerle | EpCAM (CD326) finding its role in cancer[END_REF].

Importantly, EpCAM is part of the signature of cancer-propagating cells in numerous solid tumors and of normal progenitor and stem cells [START_REF] Visvader | Cancer stem cells in solid tumours: accumulating evidence and unresolved questions[END_REF][START_REF] Gires | On the abundance of EpCAM on cancer stem cells[END_REF]. Moreover, EpCAM is apparently needed to maintain distinct cancer cell attributes (67) and, potentially, cancer stem cell phenotype as well.

Recently, several studies using various formats of bispecific antibodies (bsAbs) to retarget T cells to tumor cells have yielded outstanding results in cancer therapy studies [START_REF] Chames | Bispecific antibodies for cancer therapy[END_REF][START_REF] Chames | Bispecific antibodies for cancer therapy: the light at the end of the tunnel?[END_REF].

Interestingly, several of these molecules target EpCAM. Catumaxomab, a EpCAM x CD3 bsAb represents the first success of this new class of therapeutic antibodies as it was recently approved for the intraperitoneal treatment of patients with EpCAM positive malignant ascites [START_REF] Linke | Catumaxomab: Clinical development and future directions[END_REF]. In clinical trials, this molecule could lead to very clear clinical results, including a reduction of EpCAM-positive malignant cells in ascites by up to 5 logs [START_REF] Burges | Effective relief of malignant ascites in patients with advanced ovarian cancer by a trifunctional anti-EpCAM x anti-CD3 antibody: a phase I/II study[END_REF] and the induction of a long term anti cancer immunity [START_REF] Strohlein | Induction of anti-tumor immunity by trifunctional antibodies in patients with peritoneal carcinomatosis[END_REF]. The efficiency of this new molecule for pancreatic cancer should soon be assessed.

MT-110 is another EpCAM x CD3 bsAb that can induce potent redirected lysis of target antigen-expressing cells at pico to femtomolar concentrations, which is accompanied by highly conditional T cell activation. Redirected lysis involves formation of a cytolytic synapse, possibility of serial lysis at very low effector-to-target (E:T) ratios, and is no longer depends on MHC class I expression or co-stimulatory molecules [START_REF] Haas | Mode of cytotoxic action of T cell-engaging BiTE antibody MT110[END_REF][START_REF] Brischwein | MT110: a novel bispecific single-chain antibody construct with high efficacy in eradicating established tumors[END_REF]. This molecule is also expected to be tested soon for pancreatic cancer treatment.

Finally, a third EpCAM x CD3 bsAb is yielding promising results for pancreatic cancer treatment. HEA125 x OKT3, a hybrid-hybridoma-derived murine bispecific antibody, has recently been investigated in preclinical studies using BxPC-3 pancreatic carcinoma xenografts in NOD SCID mice [START_REF] Salnikov | Targeting of cancer stem cell marker EpCAM by bispecific antibody EpCAMxCD3 inhibits pancreatic carcinoma[END_REF]. The bsAb could significantly retard growth of xenografts in vivo, and was shown to increase duration of the contact between migrating lymphocytes and tumor cells, and to stimulate secretion of effector cytokines from non-stimulated PBMCs in the presence of EpCAM-bearing tumour cells in vitro.

Mucin 1 (MUC-1)

MUC-1 is a mucin expressed by >85% of invasive pancreatic adenocarcinomas, including early stage I disease and the precursor lesions, pancreatic intraepithelial neoplasia and intraductal papillary mucinous neoplasia [START_REF] Gold | PAM4-reactive MUC1 is a biomarker for early pancreatic adenocarcinoma[END_REF]. PAM-4, a murine anti-MUC-1 IgG, targets an epitope of MUC-1 which is absent from normal and inflamed pancreatic tissues, as well as from most other malignant tissues [START_REF] Gold | Targeting of xenografted pancreatic cancer with a new monoclonal antibody, PAM4[END_REF]. Preclinical studies demonstrated that PAM-4 was able to target pancreatic cancer with high specificity, achieving high concentrations at the tumor site using xenografted athymic nude mice. More recently, TF10, an anti-MUC-1 x HSG bsAb was derived from this mAb. This bsAb can be used in pretargeted approaches, in which the bsAb is first injected and is allowed to accumulate in the tumor before injecting, in a second step, a radiolabeled hapten ( 111 In-HSG) that is captured by the bsAb at the tumor site. This method can lead to very high tumor to normal tissues contrasts. When compared with its parental mAb in studies conducted in nude mice bearing CaPan1 human pancreatic cancer xenografts, TF10 led to much greater tumor/blood ratios of 111 In-HSG (1,000:1 at 3 hours) compared to 111 In-PAM4-IgG (5:1 at 24 hours) [START_REF] Gold | A novel bispecific, trivalent antibody construct for targeting pancreatic carcinoma[END_REF]. The high therapeutic potential of this approach should thus soon be tested in the clinic.

Death Receptor 5 (TRAIL-R2)

Tumor necrosis factor-related apoptosis-inducing ligand (TRAIL) binds to death receptors 4 and 5 (DR4, DR5) to transduce apoptotic signals. TRAIL receptors are increased in the membrane of cancer cells. More than 50% of cancer cell lines tested in vitro are TRAILsusceptible. Brain, lung, pancreatic, liver, ovary, rectum, cervix, testes, thyroid, stomach, and laryngopharynx cancers frequently overexpress DR4 and DR5 [START_REF] Ichikawa | Tumoricidal activity of a novel antihuman DR5 monoclonal antibody without hepatocyte cytotoxicity[END_REF]. However, the ability of soluble human TRAIL to induce apoptosis of normal human hepatocytes in vitro has raised questions regarding the potential usefulness of this agent in cancer therapy. TRA-8, an antihuman DR5 monoclonal antibody induces apoptosis of most (TRAIL)-sensitive tumor cells both in vitro and in vivo. However, unlike TRAIL, it does not induce apoptosis in normal hepatocytes [START_REF] Ichikawa | Tumoricidal activity of a novel antihuman DR5 monoclonal antibody without hepatocyte cytotoxicity[END_REF]. In animal models, TRA-8 produced synergistic cytotoxicity in combination with gemcitabine or irinotecan through enhanced caspase activation [START_REF] Derosier | Treatment with gemcitabine and TRA-8 anti-death receptor-5 mAb reduces pancreatic adenocarcinoma cell viability in vitro and growth in vivo[END_REF][START_REF] Derosier | Combination treatment with TRA-8 anti death receptor 5 antibody and CPT-11 induces tumor regression in an orthotopic model of pancreatic cancer[END_REF][START_REF] Derosier | TRA-8 anti-DR5 monoclonal antibody and gemcitabine induce apoptosis and inhibit radiologically validated orthotopic pancreatic tumor growth[END_REF]. These findings, with substantial inhibition of tumor growth in a mouse pancreatic cancer xenograft model receiving combination therapy, are encouraging for anti-death receptor therapy in the treatment of pancreatic cancer. Tigatuzumab, the humanized IgG1 monoclonal antibody derived from TRA-8 is ongoing phase-I clinical trials at the moment [START_REF] Forero-Torres | Phase I Trial of Weekly Tigatuzumab, an Agonistic Humanized Monoclonal Antibody Targeting Death Receptor 5 (DR5)[END_REF].

Conatumumab (AMG 655) is a fully human monoclonal agonist antibody (IgG1) to human DR5. This mAb can also induce apoptosis via caspase activation and could inhibit tumor growth in colon (Colo205 and HCT-15), lung (H2122) and pancreatic (MiaPaCa2/T2) xenograft models [START_REF] Kaplan-Lefko | Conatumumab, a fully human agonist antibody to death receptor 5, induces apoptosis via caspase activation in multiple tumor types[END_REF]. These results suggest that conatumumab is a potential therapeutic agent for treating patients with multiple tumor types, including pancreatic tumors. Clinical trials are expected for soon.

Other targets of interest

Human Claudin-4 (CLDN4) is a tetraspanin transmembrane protein consisting of 209 amino acids (aa) belonging to the CLDN family which play an important role in tight junction formation and function.. The protein structure consists of cytoplasmic N-and C-termini, four transmembrane domains and two extracellular loops. Immunohistochemical analysis and differential expression studies between normal and cancerous tissues indicate that CLDN4 expression is highly detectable in a variety of carcinomas, including pancreatic cancers.

However, CLDN4 protein is detectable in normal breast, prostate, bladder, and gastrointestinal mucosa, although its expression is substantially less intense than that seen in cancer tissue samples [START_REF] Nichols | Claudin 4 protein expression in primary and metastatic pancreatic cancer: support for use as a therapeutic target[END_REF]. Recently a chimeric (mouse/human) anti-CLDN4 has been evaluated in preclinical studies [START_REF] Suzuki | Therapeutic antitumor efficacy of monoclonal antibody against Claudin-4 for pancreatic and ovarian cancers[END_REF]. mAb KM3934 induced dose-dependent antibodydependent cellular cytotoxicity and complement-dependent cytotoxicity in vitro, and significantly inhibited tumor growth in CFPAC-1 xenografted SCID mice indicating that CDLN4 might be a valuable pancreatic tumor target.

Feto-acinar pancreatic protein (FAPP) is present at the cell surface of human pancreatic tumoral tissues. A murine antibody, mAb16D10, recognizing the O-glycosylated COOHterminal domain of FAPP, has been developed. In a recent study [START_REF] Benkoel | Monoclonal antibody 16D10 to the COOH-terminal domain of the feto-acinar pancreatic protein targets pancreatic neoplastic tissues[END_REF], this mAb stained 22 tumoral tissues over the 22 tested, independently of the tissue pretreatment (frozen sections or formalin-fixed, paraffin-embedded sections) and presented a unique specificity for membranes of neoplastic cells. Furthermore, the mAb16D10 did not react with all non pancreatic tumoral and normal tissues tested. Moreover, i.p. injections of mAb16D10 in mice xenotransplanted with human pancreatic tumoral SOJ-6 cells decreased the growth rate of the established tumor [START_REF] Panicot-Dubois | Monoclonal antibody 16D10 to the C-terminal domain of the feto-acinar pancreatic protein binds to membrane of human pancreatic tumoral SOJ-6 cells and inhibits the growth of tumor xenografts[END_REF], indicating that this target might be of interest for antibody based pancreatic cancer therapy.

Conclusion

There is an obvious need for new therapies in pancreatic cancers. Therapeutic antibodies have been successful in a number of malignancies, but results obtained on pancreatic cancer treatments have so far been extremely frustrating, with all phase III clinical trials leading to failure. However, recent years have seen the emergence of new antibody formats such as bispecific antibodies and the discovery of highly specific tumor markers. These advances should yield major improvements in a near future and should ultimately greatly impact the treatment of this devastating disease.

Gemtuzumab "ozogamicine" is coupled to calicheamicin, an antitumoral antibiotic.

3

Alemtuzumab is commercialized under the trade name Campath in USA.

4

Ibritomomab "tiuxetan" and Tositumomab are coupled to radioisotopes.