Franc ¸ois Pessaux
email: francois.pessaux@ensta.fr

For years, Integrated Development Environments have demonstrated their usefulness in order to ease the development of software. High-level security or safety systems require proofs of compliance to standards, based on analyses such as code review and, increasingly nowadays, formal proofs of conformance to specifications. This implies mixing computational and logical aspects all along the development, which naturally raises the need for a notion of Formal IDE. This paper examines the FoCaLiZe environment and explores the implementation issues raised by the decision to provide a single language to express specification properties, source code and machine-checked proofs while allowing incremental development and code reusability. Such features create strong dependencies between functions, properties and proofs, and impose an particular compilation scheme, which is described here. The compilation results are runnable OCaml code and a checkable Coq term. All these points are illustrated through a running example.

Introduction

Thanks to Wikipedia, an Integrated Development Environment is a "software application that provides comprehensive facilities to computer programmers for software development". Such environments do not provide in general all the necessary tools for critical software developments as safety, security and privacy standards require the use of formal methods all along the development cycle to achieve high levels of assurance. Every critical system must be submitted to an assessment process before commissioning. It consists in a rigorous examination of the demonstration, given by the developer, that the implementation complies with the specification requirements. Specifications, source and object codes, automated verifications and mechanically-checked (or not) proofs are scrutinized and, if needed, validation is re-done with other tools. This assessment process takes a lot of time and is expensive.

The Foc environment was created ten years ago ( [START_REF] Boulmé | On the way to certify Computer Algebra Systems[END_REF]) by T. Hardin and R. Rioboo as a laboratory language to study "how to provide comprehensive facilities" to developers of critical systems, complying to high-level rates of standards like [START_REF]Functional safety of electrical/electronic/programmable electronic safety-related systems[END_REF][START_REF]Railway Applications -Communications, Signaling and Processing Systems -Software for Railway Control and Protection Systems[END_REF][START_REF]Common Criteria for Information Technology Security Evaluation[END_REF]. At this moment, only B, Z and some tools based on algebraic data types were used in such developments. The idea was to couple the programming facilities of OCaml with the capabilities of the theorem prover Coq while avoiding the use of some complex features of these languages. The help provided to developers by object-oriented features like inheritance and late-binding, by abstraction features like modules, by parametrisation features like functors was already widely recognized in the software development world. Such features were required in the Foc specification to manage not only source code but also requirements and proofs. Their possible codings in Coq were studied [START_REF] Boulmé | Spécification d'un environnement dédié à la programmation certifiée de bibliothèques de Calcul Formel[END_REF] and some possibilities of logical inconsistencies brought by mixing these features were identified. Some of them were avoided by using a dedicated concrete syntax. The remaining ones require a dedicated static analysis to be eliminated. This was the first version of the "dependency calculus", studied by V. Prevosto [START_REF] Prevosto | Conception et Implantation du langage FoC pour le développement de logiciels certifiés[END_REF], who also designed the first compiler of the language (which name evolved in FoCaLiZe). At that time, the programming language was a pure functional strongly typed kernel, proofs were done directly in Coq. Then, a language for proofs was introduced to enable the use of the automated theorem prover Zenon[1] and automatically translate them into proof terms of Coq.

FoCaLiZe is the current version of Foc. It provides a logical language to express requirements as first-order formulas depending on identifiers present in the context, powerful data-types and patternmatching, object-oriented and modular features, a language of proofs done by Zenon, which may use unfolding of functions defined by pattern-matching. From the whole development, the compiler issues a source file written in OCaml and a proof term submitted to Coq. The two files are kept close to the FoCaLiZe source to ease traceability and the compiler guarantees that, if the FoCaLiZe source can be compiled, then its OCaml translation will be runnable and its Coq translation will be checkable. This is a way to avoid returning errors from target languages, which would be unacceptable for the user.

In this paper, we present the main features of the compiler, trying to explain why they permit to improve the adaptability of FoCaLiZe to the needs of formal developments. More returns on user experience using FoCaLiZe and help provided by this environment can been found in [START_REF] Ayrault | Development of a Generic Voter under FoCal[END_REF][START_REF] Ayrault | Development Life-cycle of Critical Software Under FoCaL[END_REF][START_REF] Prevosto | Making Proofs in a hierarchy of Mathematical Structures[END_REF].

The first specificity of FoCaLiZe is the mixing of logical and computational aspects which create a lot of dependencies between elements of a development. Definitions are considered as terms of the logical language, properties can embed names of functions being unfolded in proofs. Late-binding allows to change definitions thus altering proofs done with the old version. The second specificity of the current version of FoCaLiZe is the maximizing of sharing between computational and logical codes, at the source level, through the use of inheritance, late-binding and modularity which also adds dependencies. To keep this maximal sharing at object levels, a rather new usage of lambda-lifting relying on a static analysis of dependencies is used by the compiler and presented here.

The first section presents the paradigms FoCaLiZe is based on and introduces a running example to support further discussions. In the next section, the notion of dependency is introduced, followed by the formal description of their computation. The last section sketches the code generation model on the basis of the example.

From the FoCaLiZe Point of View

Semantical Framework

Specification requirements and implementations should be together expressible in any FIDE, the first one by logical language, the second one by a programming language. If these two languages can be related through a single semantical framework, then the demonstration of the conformance of developments to requirements can be facilitated. Choosing an imperative style related to a Hoare logical language leads to some difficulties when composing specifications and unfolding function bodies, due to the lack of referential transparency. So FoCaLiZe is built upon a pure functional language. Then, whatever is the logic, functions can be consistently unfolded in proofs and thus, can be used without restriction to express requirements (called here properties) and proofs.

Side-effects are however possible but they have to be confined into dedicated modules, separated from the rest of the development. Properties of functions making side-effects can be separately demonstrated and rendered as contracts.

Static strong typing, rich data-types and pattern-matching ease source coding and error detection. This is why the FoCaLiZe programming (sub-)language is very close to a functional kernel of the OCaml language. The logical sub-language offers first-order quantifiers and the ability to use identifiers present in the context in formulas. So formulas can contain free variables, which however are bound in the development context. These formulas are indeed formulas of a dependent type theory and are translated as such in Coq, relying on the Curry-Howard isomorphism : data types are translated onto types, properties onto types and functions on terms. Having our own logical syntax instead of the one of a dependent theory like Coq allows (not only) to restrict formation rules of terms. For example, properties can use function names but functions cannot use property names.

Incremental Specification and Development through a Running Example

To support further discussions, this section will gradually introduce a running example. It represents a "monitor" which inputs a value and outputs a validity flag indicating the position of the value with regards to two thresholds, and this value or a default one in case of problem. A fleshed-out version of this example was used to develop a generic voter used in critical software [START_REF] Ayrault | Development of a Generic Voter under FoCal[END_REF].

Object-oriented features are often offered by IDE as they have the reputation to help software development. Here, assessment also should be helped and some of these features like complex rules of visibility (tags private, friend, etc.) and possibilities of runtime late-binding can weight down this process. FoCaLiZe proposes two object-oriented features: inheritance and late-binding. We call here inheritance the ability of introducing, at any stage of the development, properties, functions and proofs (called methods in FoCaLiZe) that these new items contribute to fulfill previously stated requirements. As usual, late-binding is the possibility of introducing the name, and here the type, of a function while deferring its definition. This allows to adapt definitions along the inheritance tree and enhances reusability.

species Data = let id = "default" ; signature fromInt : int -> Self ; end ;; species OrdData = inherit Data ; signature lt : Self -> Self -> bool ; signature eq : Self -> Self -> bool ; let gt (x, y) = ˜˜(lt (x, y)) && ˜˜(eq (x, y)) ; property ltNotGt : all x y : Self, lt (x, y) -> ˜gt (x, y) ; end ;;

The component (species) Data simply says that the input is coded by an integer, converted by from int to a value of the internal representation, which is denoted by Self. The species OrdData inherits from Data, it declares two functions (lt and eq), defines a derived function gt and states a property ltNotGt using both declared and defined methods.

As function types are parts of specifications, late-binding cannot change them. But late-binding can invalidate proofs done with an "old" definition and the compiler must manage this point. Late-binding also allows stating properties and delay their proofs, while the former are already usable to write other proofs. Restricting the access to some elements is needed and handled at the component level.

A FoCaLiZe component collects not only types, declarations and definitions but also related properties and proofs. Inside a component, the manipulated data-types have a double role: a programming one used in type verification, a logical one when translated to Coq (this double view has to be managed by the compiler and it is not always straightforward as seen further). To simplify the FoCaLiZe model, all data-types introduced in a component are grouped (by the way of product and union types) into a single data-type called representation). It gives to this notion of component a flavor of Algebraic Data Type, a notion which has proven its usefulness in several IDE (e.g. [2]). The representation can be just a type variable (i.e. be not yet given an effective implementation), whose name serves in declarations. It can be instantiated by inheritance (but not redefined) to allow typing of definitions. The species TheInt defines the representation (int) and functions already declared, then proves the property by unfolding gt and using a property found in the file basics of the standard library (this proof, which could be done in OrdData, will be used later).

Functors allow parametrisation by components. Here a component may not only use functions provided by other components, but also their properties and theorems. Parametrisation by values of these parameter components is of course needed. The link between a parameterised component and its parameters will be reflected in Coq via the notion of Coq dependencies. The species IsIn has a collection parameter V and two value parameters minv and maxv from V. It mainly shows a proof decomposition into several steps (see 2.3), including a step of induction (here a simple case split) on the union type statut t.

type statut_t = | In_range | Too_low | Too_high ;; species IsIn (V is OrdData, minv in V, maxv in V) = representation = (V *
Should the definition of the representation be exposed or encapsulated by the modularity mechanism? Inheritance and late-binding require its exposure, as total encapsulation can cumbersome the development task. On the contrary parametrisation asks for its abstraction. Indeed, a component seeing the data representation of its parameters can manipulate this data without using the provided functions, hence breaking invariants and structural assumptions made by parameters and invalidating the theorems they provide. Abstract definitions of types is not sufficient as properties can still reveal the exact definition of a type (a bad point when security properties are considered). Thus FoCaLiZe has two notions of components. Species which expose their representation are only used along inheritance and late-binding during design and refinement. Collections which encapsulate the representation are used as species parameters during the integration process.

To avoid link-time errors, any call of an effective species parameter must be ensured that all functions exported by this parameter are really defined. To preserve consistency, all exported properties must have already received proofs. Thus collections can only be created by encapsulation of species, called complete species, in which all declarations have received a definition and all properties have a proof. Encapsulation builds an interface exposing only the name of the representation, declarations of (visible) functions and (visible) properties of this species. The compiler guarantees that all exposed definitions and theorems have been checked and that the interface is the only way to access collection items. The species TheInt being complete, it is submitted to encapsulation (implement) to create the collection IntC. This latter is then candidate to be effective argument of IsIn's parameter V and to apply its method fromInt to provide effective values for the minv and max parameters. Hence it can used to create other collections, In 5 10 and In 1 8.

From a developer's point of view, species serve to make an incremental development. Collections, mostly used as effective parameters of species, are used to assemble separate parts of the development.

As writing species also needs some primitive notions like booleans, integers, FoCaLiZe has a standard library which provides these low-level bricks, possibly along with proved properties but without encapsulation. The absence of encapsulation is wanted in such a case and allows manipulating basic datastructures as native constructs while however having properties. As long as the considered datatypes (i.e. type definitions here) do not have any invariant to preserve, there is no risk of inconsistency by revealing their effective structure. The standard library consists in source files that can be accessed by an opening mechanism and is not concerned by the species/collections mechanism. From the development and assessment points of view, files of the standard library are just on-the-shelf components granted by the system (or their provider).

Properties and Proofs

A proof, intended to be mechanically checked, must be decomposed into small enough steps to be checkable by the prover. Our first try (Foc) to directly use the script language of Coq, revealed several drawbacks. First, it required the user to have a deep knowledge of Coq to powerfully use it and to understand error messages. Second, the user had to be aware of the compilation of FoCaLiZe elements to Coq. Third, the proofs too deeply depended on Coq. In FoCaLiZe an intermediate step to do proofs has been introduced. It is based on natural deduction which, being reminiscent of mathematical reasoning, is accessible to a non-specialist without too much effort. It uses the automated theorem prover Zenon. A proof is a hierarchical decomposition into intermediate steps [START_REF] Lamport | How to Write a Proof[END_REF] unfolding definitions, introducing subgoals and assumptions in the context until reaching a leaf, that is, a subgoal which can be automatically handled by Zenon. When all the leaves have received proofs, the compiler translates the whole proof to Coq and builds the context needed for checking this proof. The following example shows this decomposition into a list of steps, always ended by a qed step, whose goal is the parent goal. Proofs done in a given species are shared by all species inheriting this one. As late-binding allows redefinition of functions, proofs using the "old" definition are no longer correct, must be detected as soon as the redefinition is compiled, reverted to the property status and should be done again. This link between proofs and definitions is a particular case of dependencies between elements of the user development. The section 3.1 intuitively introduces this concept while the section 3.2 formally describes the related calculus.

Specification requirements such as the safety/security ones can be split into finer ones (see [START_REF] Ayrault | Development Life-cycle of Critical Software Under FoCaL[END_REF]) and proved under the hypotheses that these finer properties hold [START_REF] Prevosto | Making Proofs in a hierarchy of Mathematical Structures[END_REF]. Thus, FoCaLiZe allows to do proofs just in time using not already proved properties and guarantees that they will be proved later in a derived complete species. This can help early detection of specification errors. Moreover, some properties can be granted by other means (contracts, verification tools, etc.). They can be considered as theorems by giving them a proof reduced to the keyword admitted. This is a needed but dangerous feature as admitted properties can lead to logical inconsistencies. The use of this keyword is recorded in the automatically done documentation file provided by the compilation process. The assessment process must ultimately check that any occurrence of this keyword is harmless.

The Compilation Process

In a nutshell, the compilation process guarantees that the whole development leads to a runnable code satisfying the requirements. Its code generation translates user code to a source code (called here simply computational code) in OCaml and to a term (called here logical code) of Coq. Data types and properties are translated to Coq types while definitions and proofs are translated as terms. Computational code only contains declarations and definitions since they are the only material contributing to an executable.

The translations of the user code are type-checked by OCaml and Coq. But these checkings arrive too late and error diagnostics may be difficult to convey to the user. Thus the compiler has its own typing mechanism, to early detect typing errors and emit comprehensive diagnostics.

First preliminary tries were done to translate inheritance and late-binding using oriented-object features of OCaml( [START_REF] Boulmé | On the way to certify Computer Algebra Systems[END_REF]). But, as Coq does not propose these features, a different way of compilation was needed to produce logical code (see [START_REF] Prevosto | Conception et Implantation du langage FoC pour le développement de logiciels certifiés[END_REF]). These two different compilation schemes jeopardize traceability as the object codes differ a lot. The current compiler uses a single method of compilation to both target languages, inspired by Prevosto's work and presented in the next section. It resolves inheritance and late-binding before code generation while controlling impacts of redefinitions onto proofs.

Zenon

The automatic theorem prover Zenon is based on a sequent calculus for first-order logic and has FoCa-LiZe-specific features such as unfolding of definitions and inductive types. Boolean values and logical propositions are strictly distinct notions in Coq but this complexity is hidden to the FoCaLiZe user: explicit conversions (done by Is true) between bool and Prop are inserted in the formula sent to Zenon. They could be axiomatized but this would blow up the search-space; instead, Zenon has inference rules dedicated to these conversions.

A proof written in FoCaLiZe is compiled into a tree of Coq sections, which translates the natural deduction style into a natural deduction proof in Coq. Each section first introduces the hypotheses of its corresponding step, then includes the sections of its substeps and ends with the proof of its goal, which is generated by Zenon from the facts of the qed step. Each leaf proof is just temporarily compiled into a "hole" later filled with a Zenon proof by invocation of ZvToV. This tool translates each leaf of the user's proof into a Zenon input file that contains the goal and assumptions and definitions listed by the user. Then Zenon outputs a Coq proof which fits right in the corresponding Coq section because every assumption it was given is available at this point in the Coq file. Once all "holes" are filled, the whole Coq source file is sent to Coq for verification.

The only acceptable errors from Zenon are simple: "out of memory", "time out", "no proof found". They mean that Zenon didn't find any proof, either because some hypotheses were missing (in this case the user may add lemmas to split the proof) or because the proposition is false. If a proof is found, Coq must raise no error when checking it otherwise there is a bug in Zenon or FoCaLiZe.

Toward Effective Code

This section begins by an informal presentation of the notion of dependencies since they strongly impact the form of the target codes generated by the FoCaLiZe compiler. Next comes the formal computation of these dependencies. Finally, the code generation model is depicted on the basis of the above example.

Dependencies in User Code

A method depending on the definition of another method m is said to have a def-dependency on m. Some def-dependencies are eliminated by a good choice of syntax. For example, function bodies cannot contain property names nor keywords for proofs, thus a function cannot def-depend on a proof. There are only two possibilities of def-dependencies. First, proofs with a by definition of m step (which unfolds the definition of m) def-depend on m. If m is redefined, these proofs must be invalidated. Second, functions and proofs can def-depend on the representation. Properties must not def-depend on the representation, as explained by the following example. The complete species Wrong may be encapsulated into a collection, whose interface contains the statement theo. This one should be well-typed in the logical code. But typing x + 1 in theo requires to identify (unify) Self with int. The encapsulation of the representation prevents it. Thus the species Wrong must be rejected by the compiler. Note that function calls do not create def-dependencies and that encapsulation of collections prevents any def-dependency on methods of collection parameters. Thus analysis of def-dependencies must ensure that proofs remain consistent despite redefinitions and that properties have no def-dependencies on the representation (in other words, interfaces of collections should not reveal encapsulated information).

Apart from the def-dependencies of proofs on definitions and of properties on representations, there are other dependencies called decl-dependencies. Roughly speaking, a method m1 decl-depends on the method m2 if m1 depends on the declaration of m2. The following example gives a first motivation for their analysis. In S, even is at once declared and defined, so its type can be inferred by the type-checker, using the type of odd. Thus even decl-depends on odd but odd does not depend on even. In T, defining odd creates a decl-dependency of odd on even and an implicit recursion between them. To keep logical consistency, such an implicit recursion must be rejected. Recursion between entities must be declared (keyword rec). The compiler has to detect any cycle in dependencies through the inheritance hierarchy.

More generally, a function m decl-depends on p if m calls p, a property m decl-depends on p if typing of m in the logical theory requires p's type, a proof decl-depends on p if it contains a step by property p or an expression whose typing needs p and, recursively, m decl-depends on any method upon which p decl-depends and so on. Def-dependencies are also decl-dependencies. These cases are not the only cases of decl-dependencies. The first version of this calculus is described in [START_REF] Prevosto | Algorithms and Proof Inheritance in the Foc language[END_REF].

Dependencies Computation

To support generation of well-formed code, the notion of dependencies must be reinforced and formally studied. The theorem ltNotGt syntactically decl-depends on gt, lt, rep and def-depends on gt. Thus, its proof is ultimately compiled to a Coq term, where gt is unfolded, making arising the identifier eq. The type of eq is needed to Coq-typecheck gt and must be provided through the λ -lift abst eq of eq. Only λ -lifting syntactic def-and decl-dependencies would lead to a generated code looking like:

Theorem ltNotGt (abst_T : Set) (abst_lt := lt) (abst_gt := OrdData.gt abst_T abst_eq abst_lt) : forall x y : abst_T, Is_true ((abst_lt x y)) -> ˜Is_true ((abst_gt x y)). apply "Large Coq term generated by Zenon".

where the := construct binds def-dependencies, and where abst eq is unbound ! Moreover, raising eq also exhibits a def-dependency on the carrier through the one of eq. Dependecies over collection parameters methods suffer from the same incompleteness. Hence, a process of "completion" of syntactically found dependencies has to be applied before λ -lifting.

It requires to compute the visible universe of a method m which is the set of methods of Self needed to analyze m. Then, the minimal (Coq) typing environment of m is built by deciding, for each method p of its visible universe if only its type must be kept (issueing λ -lift of p) or if its body is also needed (hence ":=-binding" of p). Finding the minimal set is especially important since this allows to reduce the amount of λ -liftings of method and collection generators. A last completion of the set of dependencies for parameter methods achieves the building.

In the following, we assume that inheritance has been processed, leading to a normal form of a species in which all its methods are present, in their most recent version and well-typed. Although this process is not trivial ( [START_REF] Prevosto | Algorithms and Proof Inheritance in the Foc language[END_REF][START_REF] Prevosto | Algebraic Structures and Dependent Records[END_REF]), it is out of the scope of this paper.

On Methods of Self

Let S be a species. We denote by x S (resp. x S ) the set of methods of S on which the method x decl-depends (resp. def-depends). This set is obtained by walking the Abstract Syntax Tree looking for apparition of methods names in expressions (resp. of by definition in proofs). Only dependencies on the carrier have to be checked differently, by typechecking. As proofs and properties names are syntactically forbidden inside property expressions and function bodies, typechecking of properties and functions requires only the types of the function names appearing in them (i.e. appearing in ).

Considering theorems proofs (i.e. bodies), def-dependencies can arise forcing the need to keep some definitions (not only types) to be able to typecheck. Then, one also needs to make sure that these definitions can themselves be typechecked. Moreover, proofs may involve decl-dependencies on logical methods, whose types are logical statements (i.e. expressions). Methods appearing in such types must also be typechecked. For all these reasons, the context needs to keep trace of the methods belonging to the transitive closure of the def-dependency relation, plus the methods on which these latter decl-depend. This context is called the visible universe of a method x and is noted x . In the same spirit than in [START_REF] Prevosto | Conception et Implantation du langage FoC pour le développement de logiciels certifiés[END_REF],

x is defined as follows:

y ∈ x S y ∈ x y < de f S x y ∈ x z < de f S x y ∈ z S y ∈ x z ∈ x y ∈ T S (z) S y ∈ x
where x < de f S y stands for y def-depends on x by transitivity and T S (x) stands for the type of x in the species S.

From the notion of visible universe, it is possible to define, for a method x of a species, what are the other methods needed to have x well-typed.

• Methods not present in the visible universe are not required.

• Methods present in the visible universe on which x doesn't def-depend are required but only their type is needed.

• Methods present in the visible universe on which x def-depends are required with both their type and body. Let S be a species containing the set of methods {y i ∶ τ i = e i }. Let x being one of the y i , the minimal typing environment of x is defined as follows:

∅ ⋒ x = ∅ y ∈ x {y i ∶ τ i = e i } ⋒ x = Σ {y ∶ τ = e ; y i ∶ τ i = e i } ⋒ x = Σ y ∈ x y < de f S x {y i ∶ τ i = e i } ⋒ x = Σ {y ∶ τ = e ; y i ∶ τ i = e i } ⋒ x = {y ∶ τ = e ; Σ} y ∈ x y < de f S x {y i ∶ τ i = e i } ⋒ x = Σ {y ∶ τ = e ; y i ∶ τ i = e i } ⋒ x = {y ∶ τ ; Σ}
Using the minimal typing environment it is possible to generate the method generators for nonparametrised species only since collection parameters are not taken into account. A fortiori it is not possible to generate collection generators.

On Methods from Parameters

Following the same principle than in the previous section, we note the direct dependencies of an expression e in a species S on a parameter C by DoP [EXPR] (S,C)[e] and define it by a simple search on the AST (looking for occurrences of the form C!x for any x). In the coming rule, E(S) stands for the parameters of the species S and B S (x) returns the body of the method x in the species S (i.e. an expression for a let-definition and a proof for a theorem).

The challenge is to find the minimal set of parameters methods required to typecheck a method. We now present the five first rules driving the calculus since they do not have any order of application. A last one will be exposed after.

DoP [BODY] (S,C)[x] = DoP [EXPR] (S,C)[B S (x)] DoP [TYPE] (S,C)[x] = DoP [EXPR] (S,C)[T S (x)] DoP [DEF] (S,C)[x] = DoP [EXPR] (S,C)[B S (z)] ∀z such as z < de f S x DoP [UNIV] (S,C)[x] = DoP [EXPR] (S,C)[T S (z)] ∀z ∈ x E(S) = (... ,Cp is ... ,... ,C p ′ is S ′ (... ,Cp,...)) E(S ′ ) = (... ,C ′ k is I ′ k ,...) z ∈ DoP [TYPE] (S,C p ′ )[x] ∨ z ∈ DoP [BODY] (S,C p ′ )[x] (y ∶ τy) ∈ DoP [TYPE] (S ′ ,C ′ k )[z] (y ∶ τy[C ′ k ← Cp]) ∈ DoP [PRM] (S,Cp)[x]
The rule [BODY] (resp. [TYPE]) takes into account dependencies on a method explicitly stated in the body (resp. type) of a definition.

The rules [DEF] and [UNIV] serve to collect dependencies on a parameter induced by the dependencies a method has inside its hosting species. Note that methods z introduced by the rule [DEF] are obviously included in those introduced by [UNIV]. In effect, the visible universe is wider than only transitive def-dependencies and their related decl-dependencies: if there is no def-dependencies then the relation < de f S will be empty although decl-dependencies may lead to a non-empty visible universe. The rule [DEF] allows to inspect bodies. The rule [UNIV] allows to inspect types. Hence, any z introduced by [DEF] will also has its type inspected by [UNIV].

Finally, the rule [PRM] applies to take into account dependencies of a method on a previous parameter C p used as argument to build the current parameter C p ′ . It differs from the previous rules, since the result of the calculus is not only a set of names: types are explicit. This is because the type of the methods of this set differs from the one computed during the typechecking of the species used as parameter.

If C is an entity parameter, we set: DoP [XXX] = {C}, i.e. that the identifier of the parameter is considered as it's only method.

None of these rules took into account decl-dependencies that methods of parameters have inside their own species and that are visible through types. The following example show that using P!th0 to prove th1 which only deals with P!f however needs to have P!g in the context. species A = signature f : Self -> int ; signature g : Self -> int ; property th0: all x : Self, f (x) = 0 /\ g (x) = 1 ; end ;; species B (P is A) = theorem th1 : all x : P, P!f (x) = 0 proof = by property P!th0 ; end ;; Note that because of the encapsulation process applied to collection parameters, def-dependencies are never possible and only types are visible. Hence the following rule serves to complete an initial set of dependencies D.

E(S) = (... ,Cp is Ip,...) z ∈ D(S,Cp)[x] (y ∶ τy) ∈ T Ip (z) Ip (y ∶ τy[Self ← Cp]) ∈ D + (D,S,Cp)[x]

CLOSE

Note that new dependencies brought by this rule cannot themselves require applying this rule again to make them typecheckable. In effect, only logical methods can introduce new dependencies and they only can depend on computational methods whose types are "ML-like" ones, hence cannot introduce methods names.

Code generation

Providing detailed algorithms implementing code generation is out of the scope of this paper. Instead, we illustrate their expected behaviour by showing the output obtained by compiling our above example.

Code generation starts after resolution of inheritance and late-binding, typing and dependency analyses. Note that issuing very similar target codes should ease assessment. Thus the code generation phase should be common to the two targets until concrete syntaxes are produced. Moreover a good sharing of code alleviates the assessment task and eases control of code size and reuse. Therefore we try to maximize sharing.

As inheritance and late-binding must be resolved at compile-time to ensure proof validity, it would be possible to generate code for collections only, but this prevents any sharing as shown below. Code generation of In 5 10 and In 1 8 use the last definition of methods of IsIn but they do not share their bodies. Some possible sharing of the methods of the parameter IntC are also lost. Not only code size increases but assessment takes longer since any collection should be checked in extenso. Thus, code has to be generated for all species.

Method Generators In the following example, the species IsInE redefines filter.

species IsInE (X is OrdData, low in X, high in X) = inherit IsIn (X, low, high) ; let filter = ... end ;; collection ExtIn_3_8 = implement IsInE (...) ; end ;; lowMin def-depends on filter. Its body, that is, the proof of lowMin in IsIn, can be shared by all species inheriting IsIn, if they do not redefine filter. But it cannot be shared with IsInE as the proof must be re-done. Thus, redefinitions cancel sharing of def-dependencies.

Assume that a method IsIn!m decl-depends on filter. Then all species inheriting IsIn!m and not redefining m can share its body, up to the calls of filter. Similarly the collections In 5 10, In 1 8 and ExtIn 1 8 can share the methods of IntC, up to the calls of methods on which IntC decl-depends. Thus, the body of a definition m (function or proof) of a species S can be shared along inheritance, up to the calls to methods of S and of its parameters upon which m decl-depends (thanks to the absence of cycles in decl-dependencies). The sharing is done by abstracting, in m's body, the names of these decl-dependencies, using the standard technique of λ -lifting [START_REF] Johnsson | Lambda Lifting: Transforming Programs to Recursive Equations[END_REF]. The result of this λlifting is called the method generator of m. To obtain the final code of m, this generator will have to be applied to the most recent values of its decl-dependencies, provided by the species (or its descendants) (spec-arguments) or by the effective parameters (param-arguments).

Moreover, if the logical target language (like Coq) requires explicit polymorphism, representations of Self and of parameters on which a method decl-depends are also λ -lifted (leading to parameters of type Set in Coq and named with T in the example below). As the methods and representation of a species can depend on representations and methods of collection parameters, λ -liftings of decl-dependencies upon parameters must be the outermost abstractions.

The generated codes for species are grouped into modules of the target languages, to enforce modularity and to benefit of a convenient namespace mechanism. Now either these modules contain all the inherited and non-redefined method generators of the species (but this leads to code duplication) or a method generator is created once, when a method is (re)defined and appears only in the species that defines it. We use the latter solution. Example continued. The example of section 2.2 is pursued, using a Coq-like syntax. OCaml files are just obtained by removing some types, properties and proofs and are not listed here. In method generators, any occurrence of the name of a decl-dependency m is replaced by abst_m and abstracted. If by adding a definition, this decl-dependency is turned into a def-dependency, then abst_m is bound to the definition of m by the construct abst_m := Coq term.

Generating code for species Data: The defined method id has no dependencies, hence trivially leads to a simple definition.

Module Data.

Definition id : basics.string__t := "default". End Data.

Generating code for species OrdData: The body of gt decl-depends on eq, lt and the representation as its inferred type is Self → Self → bool. Note that this body remains close to the source one. Inherited and only declared methods induce no code. Generating code for species TheInt: This species redefines id and defines eq, fromInt and lt. id has no dependencies whereas eq, from int and lt only have a def-dependency on the representation, whose value (the built-in type int) is bound (:= construct) to abst T in the corresponding method generators.

The proof of ltNotGt decl-depends on the representation. It def-depends on gt because it unfolds its definition. Note that lt and eq do not appear in this proof : unfolding of gt does not unfold them recursively. But typing ltNotGt requires typing gt and thus typing lt and eq. Hence, ltNotGt has decl-dependencies on lt and eq, coming from the def-dependency on gt. So, lt and eq must be λ -lifted in ltNotGt, to build the value of abst gt by applying the method generator gt found in the module OrdData to its three arguments. Note that only the types of lt and eq are used by ltNotGt: these methods can be redefined without impacting this theorem. As illustrated by this example, the dependency calculus cannot be reduced to a simple "grep". For any method, the analysis must compute the sets of methods of the species and of the parameters which are needed to elaborate the type and the value of its logical code (in Coq, they are called visible universe and minimal typing environment). This is the price to pay for having no errors in target codes.

Collection generators

Code generation for collections must create computational runnable code and checkable logical code. Suppose that a collection C is built by encapsulating a complete species S. The code of a method S!m is obtained by applying its method generator, say G m, to its effective arguments. The right version of this method generator G m comes from the last definition of m in the inheritance path ending on S. The effective spec-arguments of G m can be retrieved from the species having created G m and from the instantiations of formal parameters done during inheritance. These applications can be safely done as the species S is complete and as the dependency analysis provides an ordering on all methods of a species, such that the n th method depends only on the (n -1) first ones. The effective param-arguments of G m come from the application of the species S to effective collection parameters.

Thus a simple solution to generate collection code is to do it method by method, by applying method generators to their effective arguments. These applications are computed at runtime in the target languages. This solution allows us to generate only the needed applications for a given method. But a possibility of sharing is lost, when collections are issued from the same parameterized species, applied to different effective collection parameters (case of In 5 10 and In 1 8). Then the applications of the method generators to the spec-arguments can be shared between all these collections. Regarding memory use, the gain is small. But regarding assessment processes, such an intermediate step of applications represents a large gain as it avoids having to review several copies of the same code, applied to different param-arguments. We retain this solution. To ease code review, the applications to the spec-arguments are grouped into a record (we assume that target languages offer records) called collection generator while the λ -liftings of all parameters decl-dependencies are moved outside the record body. Thus the material coming from the species is found in the body while the effective parameters contribution appears in the applications of the body.

It is possible to go further by replacing the bunch of λ -liftings of parameter dependencies with a unique λ -lifting abstracting the collection parameter. Then the target modules should be first-class values of the target languages with a certain kind of subtyping as interfaces inclusion provides a simple but useful subtyping. Even if our target languages have such features, it seems better to leave the code generation model open to a wide range of potential targets.

Example ended We continue the example of 2.2 by completing the module TheInt with the collection generator and its record type. The type of each method of the species is recorded into a record field labeled rf , its value local (obtained by a future application of the collection generator to all the param-arguments) has no more λ -lift. Here, as this collection has no parameter, there is no λ -lifting on the record itself. The value of local gt for example is obtained by applying the method generator coming from OrdData to its specarguments, whose values have already been generated, thanks to the absence of cycles in dependencies. The function mk record builds the record out of these values. Generating code for species IsIn. The types of the fields are translations of the types of the methods of the collection. The dependency calculus shows that the record depends on the carrier of the parameter

Summarizing Dependencies Usage in λ -lifting

As previously introduced, dependencies are subject to be λ -lifted to define record types, method generators and collection generators. In a symmetrical fashion, they determine the effective methods to provide to these generators, which can only be achieved taking care of the instantiations of formal collection and entity parameters by effective arguments along the inheritance. The detailed mechanism of this is out of the scope of the present paper. Instead, we summarize here the material to λ -lift for each category of code generated element, in order of apparition for a species:

• Parameters carriers For record type and collection generator: all those of the parameters. For method generators: per method, only those of the used parameters. • Parameters methods -For record type: "union" of all the dependencies of all the methods got by [CLOSE] ([TYPE]).

-For method generators: the dependencies of the related method obtained by rules:

[BODY] + [TYPE] + [CLOSE] ([DEF] + [UNIV] + [PRM]

). -For collection generator: "union" of methods dependencies abstracted in each of the method generators. • Methods of Self Only needed for method generators: those belonging to the minimal typing environment that are only declared.

Note that because of relative dependencies between methods of parameters inside their own species, λ -lifts of methods must be ordered for a same parameter to ensure they only refer to previously λ -lifted elements. Moreover, parameters are processed in order of apparition in the species: this way, all the methods of a same parameter are λ -lifted in sequence.

Conclusion

Building FoCaLiZe, a lot of questions, choice points, etc. arose from the will to avoid dissociating the computational and logical aspects in a formal development while keeping the FIDE palatable. The mix of inheritance, late binding, encapsulation, inductive data types and unfolding of definitions in proofs creates complex dependencies, which have to be analyzed to ensure development correctness. This analysis gives the basis of the compilation process through the notions of method and collection generators, that we introduced to allow code sharing. The code generation model producing computable and logical target codes is outlined through an example. The formal computation of dependencies was presented with an short summary of their usage in the λ -lifting process.

Several other FIDEs mentioned in the introduction have followed other choices. It should be very interesting to compare their compilation models with ours, particularly on the method used to establish correspondence between runnable and logical code and on their semi-automation of proofs.

Zenon greatly contributes to FoCaLiZe since it brings proof automation. This point is especially crucial to keep proofs simpler. We plan to extend it to handle recursion termination, arithmetic, temporal properties and, as it targets other provers than Coq, to experiment with other target type theories.

  ; let id = "native int" ; let fromInt (x) : Self = x ; let lt (x, y) = x <0x y ; let eq (x, y) = x =0x y ; proof of ltNotGt = by definition of gt property int_ltNotGt ; end ;;

collection

  IntC = implement TheInt ; end ;; collection In_5_10 = implement IsIn (IntC, IntC!fromInt (5), IntC!fromInt (10)) ; end ;; collection In_1_8 = implement IsIn (IntC, IntC!fromInt (1), IntC!fromInt (8)) ; end ;;

  theorem t : all a b c : bool, a -> (a -> b) -> (b -> c) -> c proof = <1>1 assume a b c : bool, hypothesis h1: a, hypothesis h2: a -> b, hypothesis h3: b -> c, prove c <2>1 prove b by hypothesis h1, h2 <2>2 qed by step <2>1 hypothesis h3 <1>2 qed by step <1>1The proof has two outer steps <1>1 and <1>2. Step <1>1 introduces hypotheses h1, h2, h3 and the subgoal c. It is proved by a 2-step subproof. Step <2>1 uses h1 and h2 to prove b. Step <2>2 uses <2>1 and h3 in order to prove c. Step <1>2 ends the whole proof.

  species Wrong = representation = int ; let incr (x) : Self = x + 1 ; theorem theo : all x : Self, incr (x) = x + 1 ; end ;; collection Bad = implement Wrong ;; Bad . . . bad interface representation : self incr (x) : Self -> int theorem theo : all x : Self, incr (x) = x + 1 ;

  species S = signature odd : int -> bool ; let even (n) = if n = 0 then true else odd (n -1) ; end ;; species T = inherit S ; let odd (n) = if n = 0 then false else even (n -1) ; end ;;

  Definition gt (abst_T : Set) (abst_eq : abst_T -> abst_T -> basics.bool__t) (abst_lt : abst_T -> abst_T -> basics.bool__t) (x : abst_T) (y : abst_T) : basics.bool__t := basics.not (abst_lt x y) && basics.not (abst_eq x y) End OrdData.

  Definition id : basics.string__t := "native int". Definition eq (abst_T := basics.int__t) (x : abst_T) (y : abst_T) : basics.bool__t := (basics._equal_0x x y). Definition fromInt (abst_T := basics.int__t) (x : basics.int__t): abst_T := x. Definition lt (abst_T := basics.int__t) (x : abst_T) (y : abst_T) : basics.bool__t := (basics._lt_0x x y). Theorem ltNotGt (abst_T : Set) (abst_eq : abst_T -> abst_T -> basics.bool__t) (abst_lt : abst_T -> abst_T -> basics.bool__t) (abst_gt := OrdData.gt abst_T abst_eq abst_lt): forall x y : abst_T, Is_true ((abst_lt x y)) -> ˜Is_true ((abst_gt x y)). apply "Large Coq term generated by Zenon" ; End TheInt.

  Let effective_collection := IsIn.collection_create IntC.me_as_carrier (IntC.fromInt 5) (IntC.fromInt 10) IntC.lt IntC.gt IntC.ltNotGt. Definition filter := effective_collection.(IsIn.rf_filter _ _ _ _ ). Definition getStatus := effective_collection.(IsIn.rf_getStatus _ _ _ _). Definition getValue := effective_collection.(IsIn.rf_getValue _ _ _ _). Definition lowMin := effective_collection.(IsIn.rf_lowMin _ _ _ _). End In_5_10.

by definition of filter type statut_t hypothesis H <2>2 qed by step <2>1 property V!ltNotGt <1>2 qed by step <1>1 definition of getStatus ; end ;;

	statut_t) ;
	let getValue (x : Self) = fst (x) ;
	let getStatus (x : Self) = snd (x) ;
	let filter (x) : Self =
	if V!lt (x, minv) then (minv, Too_low)
	else
	if V!gt (x, maxv) then (maxv, Too_high)
	else (x, In_range) ;
	theorem lowMin : all x : V, getStatus (filter (x)) = Too_low -> ˜V!gt(x, minv)
	proof =
	<1>1 assume x : V,
	hypothesis H: snd (filter (x)) = Too_low,
	prove ˜V!gt (x, minv)
	<2>1 prove V!lt (x, minv)

This work is supported by the project BGLE -DEPARTS

V, on the two value parameters minv and maxv and on the method V!gt. These decl-dependencies are λ -lifted. For example, the type of rf lowMin is the translation of the property lowMin, which decl-depends on V!gt. The abstraction on V!gt needed for lowMin is also done on the other fields. Methods have no decl-dependencies on methods of IsIn, except lowMin which has a def-dependency on filter. The other decl-dependencies are on the representation of IsIn (and through it, on the one of V), on V's methods and on values minv and maxv. The def-dependency of lowMin leads to the binding (:=) of abst filter to the application of the method generator filter to all its arguments, represented by abstracted variables in the context.

The body of the collection generator IsIn!collection create are the applications of the method generators to their param-arguments (no spec-arguments here). Then these param-arguments are λ -lifted. Generating code for collection In 5 10: Here, IsIn.collection create is applied to effective arguments found in the module IntC and definitions are extracted as above. The four underscores are just arguments inferred by Coq, which denote the four parameters of the record.

A huge amount of work remains to do in order to enhance FoCaLiZe. But, with all its weaknesses, it has already proved to be efficient in non-trivial developments. While safety domains already have a large number of good tools, security domains are much less well endowed, and the recent interest in combining safety and security requirements will increase demand for such tools.


Nina Miolane
email: nina.miolane@inria.fr

Xavier Pennec

In the era of big data, one may apply generic learning algorithms for medical computer vision. But such algorithms are often "black-boxes" and as such, hard to interpret. We still need new constructive models, which could eventually feed the big data framework. Where can one find inspiration for new models in medical computer vision? The emerging field of Neurogeometry provides innovative ideas. Neurogeometry models the visual cortex through modern Differential Geometry: the neuronal architecture is represented as a sub-Riemannian manifold R 2 × S 1 . On the one hand, Neurogeometry explains visual phenomena like human perceptual completion. On the other hand, it provides efficient algorithms for computer vision. Examples of applications are image completion (in-painting) and crossing-preserving smoothing. In medical image computer vision, Neurogeometry is less known although some algorithms exist. One reason is that one often deals with 3D images, whereas Neurogeometry is essentially 2D (our retina is 2D). Moreover, the generalization of (2D)-Neurogeometry to 3D is not straight-forward from the mathematical point of view. This article presents the theoretical framework of a 3D-Neurogeometry inspired by the 2D case. We survey the mathematical structures and a standard frame for algorithms in 3D-Neurogeometry. The aim of the paper is to provide a "theoretical toolbox" and inspiration for new algorithms in 3D medical computer vision.

A survey of mathematical structures for extending 2D neurogeometry to 3D image processing Introduction Machine learning algorithms using big data are often "black-boxes". Thus, they can be hard to interpret. There is still a need of constructive models, so that the big data framework can be fed by new structures. The visual cortex offers inspiration for new methods in (medical) computer vision. From the biological model of human vision, one builds a geometric model of the visual cortex. The geometric model is in turn implemented for computer vision purposes. This is the field of (2D)-Neurogeometry.

Biological intuition behind Neurogeometry

The geometric model of the visual cortex's is built as follows. From the biological point of view, neurons of the primary visual cortex V 1 are local detectors called "point processors" [START_REF] Koenderink | Representation of local geometry in the visual system[END_REF]. They are retinotopically connected to small domains of the retina, called their "receptive field" [START_REF] Jones | An evaluation of the two-dimensional gabor filter model of simple receptive fields in cat striate cortex[END_REF]. Mathematically, this structure is an isomorphic map from the 2D retina to the 2D cortical layer. It means that each neuron is associated to a position in our retina (x, y) ∈ R 2 , or equivalently in our visual field.

Then, the neuron acts as a filter on the optical signal of the retina's photoreceptors. Its transfer function is called its "receptive profile". The so-called "simple neurons" of V 1 have a highly anisotropic profile [START_REF] Jones | An evaluation of the two-dimensional gabor filter model of simple receptive fields in cat striate cortex[END_REF]. They are sensitive to the orientation θ ∈ S 1 of the optical signal, in terms of the intensity gradient. A simple neuron is thus represented by the corresponding position (x, y) ∈ R 2 of the retina and by the preferred orientation θ ∈ S 1 of its filter [START_REF] Petitot | Neurogeometry of neural functional architectures[END_REF].

Interestingly, Hubel and Wiesel have shown that neurons detecting all orientations at the same position (x, y) form an anatomical structure, called an "orientation hypercolumn" [START_REF] Hubel | Orientation columns in macaque monkey visual cortex demonstrated by the 2-deoxyglucose autoradiographic technique[END_REF]. This discovery led to the Nobel Prize in 1981. It means that the fiber bundle R 2 × S 1 is neurally implemented in the brain.

Ultimately, one models the neuronal activity propagation in R 2 × S 2 . The horizontal cortico-cortical connections of V 1 are represented by a horizontal distribution in sub-Riemannian geometry [START_REF] Petitot | Neurogeometry of neural functional architectures[END_REF]. The propagation of the cortical activity is then a propagation along sub-Riemannian geodesics [START_REF] Citti | A cortical based model of perceptual completion in the rototranslation space[END_REF].

Implementations of Neurogeometry for computer vision

One finds implementations of 2D-Neurogeometry in computer vision. For example, a sub-Riemannian diffusion process leads to algorithms for image completion or inpainting [START_REF] Boscain | Hypoelliptic diffusion and human vision: A semidiscrete new twist[END_REF]. Fitting a sub-Riemannian geodesic enables contour completion [START_REF] Citti | A cortical based model of perceptual completion in the rototranslation space[END_REF]. Furthermore, a sub-Riemannian smoothing can smooth the image while preserving crossings [START_REF] Duits | Left-invariant parabolic evolutions on se (2) and contour enhancement via invertible orientation scorespart i: Linear left-invariant diffusion equations on se[END_REF]. But the framework lacks general applications in medical computer vision, although some exist [START_REF] Duits | Left-invariant diffusions on the space of positions and orientations and their application to crossing-preserving smoothing of hardi images[END_REF]. One reason is that Neurogeometry is essentially 2D, as the retina is 2D. And the generalization of 2D-Neurogeometry to 3D-Neurogeometry is conceptually subtle. There is a need of a theoretical survey summarizing the mathematical structures in the 3D framework. The purpose of this paper is to fill this gap.

Contribution and outline of the paper This paper aims to be a guide for understanding and generalizing 2D-Neurogeometry to 3D-Neurogeometry. It is a theoretical toolbox of 3D-Neurogeometry for: 1) conceiving new algorithms in medical computer vision; and 2) interpreting existing algorithms. In Section 1, we recall briefly some concepts of Differential Geometry. In Section 2, we describe 2D-Neurogeometry and its applications, as an introduction to the 3D case. In Section 3, we describe 3D-Neurogeometry and its possible applications.

Requirements of Differential Geometry

The following is summarized in Table 1 at the end of the section. We assume that the reader is familiar with the following concepts of Differential Geometry: manifolds, (principal) fiber bundles, (pseudo-) Riemannian manifolds [14], Lie groups, Lie algebra, bi-invariant (pseudo-)metrics [START_REF] Bourbaki | Lie Groups and Lie Algebras: Chapters 1-3. Bourbaki, Nicolas: Elements of mathematics[END_REF] [START_REF] Miolane | Computing Bi-Invariant Pseudo-Metrics on Lie Groups for Consistent Statistics[END_REF], Lie group action on a manifold, homogeneous manifolds [START_REF] Alekseevsky | The riemannian geometry of orbit spaces. the metric, geodesics, and integrable systems[END_REF], sub-Riemannian manifolds [START_REF] Bellaıche | Sub-riemannian geometry[END_REF]. Some are illustrated in Fig. 1.

Fig. 1: Left: S 2 and R 2 are manifolds. Center: tangent bundles of S 2 and R 2 . Right-top: principal bundle with base S 2 and structure group S 1 . Right-bottom: principal bundle with base R 2 and structure group R. In all cases, the fibers are drawn in blue.

The aforementioned structures are present simultaneously in the computational framework of Neurogeometry. They arise with their set of related curves, as shown in Table 1. Depending on the application for image processing, one is interested in computing one curve or another. Thus, on shall understand their differences and relations. Some curves are illustrated in Fig. 2. 2) is 1-dimensional). Riemannian geodesics on S 2 and R 2 for standard induced metric from R 3 on S 2 and the Euclidean metric on R 2 .

The example of 2D-Neurogeometry

This section serves as an introduction of the 3D case. An image processing pipeline using 2D-Neurogeometry usually follows three steps: 1. Lift (L), 2. Processing (P) and 3. Projection (P) (LPP-frame, see Fig. 3). These steps can be iterated [START_REF] Citti | A cortical based model of perceptual completion in the rototranslation space[END_REF] [START_REF] Sanguinetti | Image completion using a diffusion driven mean curvature flowing a sub-riemannian space[END_REF] or not [START_REF] Boscain | Hypoelliptic diffusion and human vision: Anthropomorphic Image Reconstruction via Hypoelliptic Diffusion[END_REF] [START_REF] Duits | Left-invariant parabolic evolutions on se (2) and contour enhancement via invertible orientation scorespart i: Linear left-invariant diffusion equations on se[END_REF]. Biologically, the lift represents the activation of the neurons in V1. The processing of the lifted image represents the propagation of the neuronal activity in V1. The projection corresponds to our visual interpretation of the information given by the visual cortex after neuronal propagation.

First, we survey the mathematical structures (subsections 2.1, 2.2). We summarize them in Table 2. Then we present the LPP-frame of standard algorithms in 2D-Neurogeometry (subsection 2.3). Application-oriented readers can start with subsection 2.3, then go to subsections 2.1, 2.2. 1: Curves related to the different structures of Differential Geometry in Neurogeometry. For spaces: M is a manifold, (P, M ) a fiber bundle of base M , (M, G) is M endowed with a G action, (P, M, G) is a principal bundle of base M and structure group G, G is a Lie group. For verticality/horizontality: V F , V O , V and V ∆ : vertical in the sense of fibers, orbits, orbits=fibers (same notion for principal bundle), ∆-distribution. Same notations using H for horizontal. For metric structures: g R is a (pseudo)-Riemannian metric, g SR is a sub-Riemannian metric. For curves: γ denotes a notion of geodesics. We have γ G , γ G e , γ R , γ SR for group geodesic, 1-parameter subgroup, Riemannian geodesics and sub-Riemannian geodesic.

On M On (P, M ) On (M, G) On (P, M, G) On G • V F -curves • V O -curves • V -curves • γ G ex: γ G -action ex: γ G -action ex: γ G e No metric • H F -curves • H O -curves • H-curves Metric • γ R • V F -γ R • V O -γ R • V -γ R IF g R bi-inv.: g R • H F -γ R • H O -γ R • H-γ R γ G = γ R SR-metric • V ∆ -curves IF ∆ ⊥ fibers: IF ∆ ⊥ orbits: IF ∆ ⊥ fibers: IF G Carnot: g SR • H ∆ -curves V ∆ = V F V ∆ = V O V ∆ = V ∃ g SR ex: γ SR H ∆ = H F H ∆ = H O H ∆ = H Table

Structures on the lifted space

SE(2) = R 2 × SO(2) = R 2 × S 1
Group actions The law of SE( 2) is, for all (t 1 , R 1 ), (t 2 , R 2 ) ∈ SE(2):

(t 1 , R 1 ) * (t 2 , R 2 ) = (R 1 .t 2 + t 1 , R 1 .R 2 )
In this law, we read the group actions on SE(2) and their general properties. SE(2) acts on itself through the left and right translations (freely and transitively). As a Lie subgroup, SO(2) acts on SE(2) on the left and right (freely but not transitively). Note that the right SO(2)-action is trivial on the R 2 part. Moreover, the right SO(2)-action makes SE(2) a principal bundle of base R 2 and structure group SO(2).

A sub-Riemannian metric and two Riemannian metrics To introduce the sub-Riemannian metric, one first defines its horizontal distribution ∆. In 2D-Neurogeometry one takes the moving frame

(X 1 , X 2 , X 3 ) on R 2 × S 1 :      X 1 = cos θ.∂ x + sin θ.∂ y , X 2 = ∂ θ , X 3 = -sin θ.∂ x + cos θ.∂ y to define ∆ = (X 1 , X 2 )
. The sub-Riemannian metric g SR is defined as the Euclidean metric on ∆. In the standard basis ∂ x , ∂ y , ∂ z , its inverse writes:

g SR (x, y, θ) ij =   cos 2 θ sin θ cos θ 0 sin θ cos θ sin 2 θ 0 0 0 1  
In practice, the sub-Riemannian metric is usually approximated the Riemannian metric g R whose inverse is [START_REF] Citti | A cortical based model of perceptual completion in the rototranslation space[END_REF]:

g R (x, y, θ) ij =   cos 2 θ + 2 sin 2 θ (1 -2 ) sin θ cos θ 0 (1 -2 ) sin θ cos θ sin 2 θ + 2 cos 2 θ 0 0 0 1  
In addition, one defines a left-invariant metric g R µ as:

g R µ (0, 0, 0) ij =   µ 0 0 0 µ 0 0 0 1  
on the Lie algebra se(2). Then, one propagates it on SE(2) through left translations. g R µ is (SE( 2))-left-invariant by construction. But g R µ is not (SE( 2))-rightinvariant as there is no bi-invariant metric on SE(2) [START_REF] Miolane | Computing Bi-Invariant Pseudo-Metrics on Lie Groups for Consistent Statistics[END_REF]. g R µ is invariant by the SO(2)-left and SO(2)-right actions.

A survey of curves From Table 1 and the aforementioned structures, we survey the curves on SE(2). We have group geodesics of SE(2), Riemannian geodesics of g R µ , sub-Riemannian geodesics of g SR and their Riemannian approximation through g R . Group and Riemannian geodesics differ as g R µ is not bi-invariant. w.r.t. the right SO(2)-action, some are vertical or horizontal (taken w.r.t. g R µ ). Examples of vertical group geodesics, vertical Riemannian geodesics for g R µ and vertical sub-Riemannian geodesics for g SR are orbits of the SO(2)-action. Examples of horizontal group geodesics, horizontal Riemannian geodesics for g R µ are straight lines between two translations. Examples of horizontal sub-Riemannian geodesics for g SR are integral curves of X 1 .

w.r.t. ∆, some are ∆-vertical or ∆-horizontal. There is no ∆-vertical group geodesics, and no ∆-vertical Riemannian geodesic. Example of ∆-horizontal group geodesics and ∆-horizontal Riemannian geodesic for g R µ are orbits of the right SO(2)-action. Sub-Riemannian geodesics are always ∆-horizontal.

Structures on the image domain R 2

Projecting R 2 × S 1 along the fibers S 1 gives R 2 . Equivalently, we can quotient SE(2) by the SO(2)-right. The residual left SE(2)-action on R 2 is: (t, R) • x = R.x + t. We read the related left SO(2)-action. Regarding the metric structures, g R µ was right SO(2)-invariant. Thus the projection is a Riemannian submersion for g R µ . It induces a Riemannian metric on R 2 which is the Euclidean metric. Projecting the horizontal Riemannian geodesics gives linear curves in R 2 . The projection of the sub-Riemannian geodesics gives the elastica curves [START_REF] Citti | A cortical based model of perceptual completion in the rototranslation space[END_REF], which can be linear or curvilinear.

Actions Metrics

SE(2) = R 2 × S 1 • left, right translations of SE(2) • g R µ • left, right actions of SO(2) • g SR • g SR R 2 • left action of SE(2) • Euclidean metric • left action of SO(2)
(projection of g R µ ) Table 2: Structures of 2D-Neurogeometry. Use Table 1 to get the related curves.

The three steps

First step: Lift The image domain D ⊂ R 2 is lifted to D ∈ R 2 × S 1 [5]
(positions and orientations taken with directions). The lift is implemented by detecting the direction of the intensity gradient:

∇I ||∇I|| = (-sin θ, cos θ) at each point (x, y) ∈ D. Then D is mapped to a surface D: (x, y) → (x, y, θ(x, y)) in R 2 × S 1 .
At the end of this step, the intensity is a function of D. Alternatively, one can lift to the projective tangent bundle P T R 2 = SE(2)/Z 2 (positions and orientations taken without directions) [START_REF] Boscain | Hypoelliptic diffusion and human vision: Anthropomorphic Image Reconstruction via Hypoelliptic Diffusion[END_REF] . Whether one should use SE(2) of P T R 2 is discussed here [START_REF] Boscain | Hypoelliptic diffusion and human vision: Anthropomorphic Image Reconstruction via Hypoelliptic Diffusion[END_REF](rem. 4, 13).

Second step: Processing First, the processing can be the evolution of partial differential equations (PDEs) with sub-Riemannian operators. For example, the sub-Riemannian diffusion is defined with the sub-Riemannian Laplacian

∆ SR = X 2 1 + X 2 2 .
Depending on the goal of the processing, one adds drift (also called convection) to the PDE: there is drift for completion purposes [START_REF] Boscain | Hypoelliptic diffusion and human vision: Anthropomorphic Image Reconstruction via Hypoelliptic Diffusion[END_REF] and for enhancement [START_REF] Duits | Left-invariant diffusions on the space of positions and orientations and their application to crossing-preserving smoothing of hardi images[END_REF]. Equivalently, one can formulate this step as an oriented random walk. One writes the corresponding Kolmogorov equations. Some PDEs are computed with the lifted intensity I(x, y, θ). In-painting methods provide examples: one "paints" directly in the lifted space [START_REF] Boscain | Hypoelliptic diffusion and human vision: Anthropomorphic Image Reconstruction via Hypoelliptic Diffusion[END_REF]. Others compute with the activity function: u(x, y, θ) = u(x, y, θ)δ Σ where u(x, y, θ) = |X 3 (θ).∇I(x, y)|. In-painting methods provide also examples of this approach [START_REF] Sanguinetti | Image completion using a diffusion driven mean curvature flowing a sub-riemannian space[END_REF]. The corrupted image has a hole in D. The activity propagation amounts to "fill the hole" by a minimal surface. Then, one "paints" the surface by linking the isolevel sets with sub-Riemannian geodesics.

Then, the processing can be curve fitting. Which curve do we fit? One can fit a sub-Riemannian geodesic, as in the second example of in-painting above [START_REF] Sanguinetti | Image completion using a diffusion driven mean curvature flowing a sub-riemannian space[END_REF]. Another example is contour completion [START_REF] Citti | A cortical based model of perceptual completion in the rototranslation space[END_REF]. One can also fit a Riemannian geodesic or a group geodesic for enhancement of 1-dimensional structures. A comparison of the two suggests that one should prefer the group geodesic [START_REF] Duits | Left-invariant diffusions on the space of positions and orientations and their application to crossing-preserving smoothing of hardi images[END_REF][7](called the "exponential curve" here).

Third step: Projection The processed lifted image on R 2 × S 1 is projected to a "standard" image defined on R 2 . The projection can be done in two different ways. First, one can use the "verticality" along fibers of the bundle R 2 × S 1 . In this case, one projects along the fiber S 1 , choosing a θ that maximizes a likelihood criterion [START_REF] Boscain | Hypoelliptic diffusion and human vision: A semidiscrete new twist[END_REF]. Second, one can use the "∆-verticality" of sub-Riemannian geometry. In this case, one projects along the normal of the horizontal distribution ∆ through a concentration scheme [START_REF] Sanguinetti | Image completion using a diffusion driven mean curvature flowing a sub-riemannian space[END_REF]. This allows for several maxima at each point, i.e. crossings on the image.

A theoretical toolbox for 3D-Neurogeometry

As implemented by now [START_REF] Duits | Left-invariant parabolic evolutions on se (2) and contour enhancement via invertible orientation scorespart i: Linear left-invariant diffusion equations on se[END_REF] [8], image processing pipelines using 3D-neurogeometry also follows the three same steps: 1. Lift (L), 2. Processing (P) and 3. Projection (P) (see Fig. 4). This steps could be iterated or not. The difference with the 2D-neurogeometry however is the Processing. In this step, there is an additional level of structure in 3D-Neurogeometry w.r.t. the 2D case.

As in the 2D-case, we first survey the mathematical structures and summarize them in Table 5 (subsections 3.1,3.2, 3.3). Then we present the LPP-frame of a 3D-Neurogeometry (subsection 3.4). Application-oriented readers can read subsection 3.4 first, and then go to subsections 3.1, 3.2, 3.3.

Structures on the Lie group SE

(3) = R 3 × SO(3)
Group actions The law of SE(3) is, for all (t 1 , R 1 ), (t 2 , R 2 ) ∈ R 3 × SO(3):

(t 1 , R 1 ) * (t 2 , R 2 ) = (R 1 .t 2 + t 1 , R 1 .R 2 ).
We read the group actions on SE(3) and their properties (see Table 3).

As a Lie group, SE(3) acts on itself through left and right translations. As subgroups of SE(3), SO(3) and SO(2) also act on SE(3), on the left and right. The right SO(3)-action makes SE(3) a trivial principal bundle over R 3 with structure group SO(3). The right SO(2)-action on SE(3) makes the SE(3) a principal bundle over R 3 × S 2 with structure group SO(2).

Fig. 2 :

 2 Fig.2: From Left to Right. S 2 and R 2 with action of SO[START_REF] Bellaıche | Sub-riemannian geometry[END_REF]. The orbits are in blue and coincide with the curves created by the action of 1-parameter subgroups of SO(2) (as SO(2) is 1-dimensional). Riemannian geodesics on S 2 and R 2 for standard induced metric from R 3 on S 2 and the Euclidean metric on R 2 .

Fig. 3 :

 3 Fig. 3: The 3 steps of image processing in 2D neurogeometry.

Free Transitive Orbits Isotropy Quotient On R 3 3: Properties of group actions on SE [START_REF] Boscain | Existence of planar curves minimizing length and curvature[END_REF]. "Isotropy" means the isotropy groups. Actions on the R 3 -part of SE(3) = R 3 × SO [START_REF] Boscain | Existence of planar curves minimizing length and curvature[END_REF] are the main distinction between Left and Right. "Fundamental" denotes the fundamental representation on R 3 , and "Trivial" the trivial representation on R 3 .

A left-invariant metric and a bi-invariant pseudo-metric As in the 2D case, one defines the left-invariant metric g R µ on SE(3). g R µ is left-invariant by construction. But g R µ is not right-invariant. g R µ is invariant by the left and right SO(3)-actions. The left SO(3)-invariance comes from the left invariance of g R µ . The right SO(3)-invariance is shown considering the right action on the parts R 3 and SO(3) separately, as g R µ is diagonal. Consequently, g R µ is also invariant by left and right SO(2)-actions. As opposed as the 2D case, there exist bi-invariant pseudo-metrics on SE(3). We refer to [START_REF] Miolane | Computing Bi-Invariant Pseudo-Metrics on Lie Groups for Consistent Statistics[END_REF] for their explicit construction. A possible choice is:

known as the Klein form. Here I 3 is the 3D identity matrix.

A survey of curves on SE(3) From Table 1 and the aforementioned structures, we survey the curves on SE(3). We have the group geodesics of SE(3), the Riemannian geodesics of g R µ an the pseudo-Riemannian geodesics of g BI . The group geodesics coincide with the pseudo-Riemannian ones, but differ from the Riemannian ones [14] (see Table 1 We go from SE(3) to R 3 × S 2 , by quotienting the right SO(2)-action. The quotient is implemented by choosing an origin in R 3 × S 2 , usually (0, a). An element (x, n) ∈ R 3 × S 2 is represented as the result of the action of the corresponding (x, R) on (0, a), where R is precisely the rotation bringing a onto n.

Induced group actions The induced action of SE

We read the group actions on R 3 × S 2 and their properties (see Table 4).

The SE(3)-action is transitive on R 3 × S 2 . It makes R 3 × S 2 a homogeneous space. As the isotropy group is SO(2) everywhere, the orbit-stabilizer theorem gives: R 3 × S 2 = SE(3)/SO [START_REF] Bellaıche | Sub-riemannian geometry[END_REF]. Moreover, it provides the justification of the choice of an origin (0, a) in computer vision algorithms. All points are equivalent in a homogeneous space. Computations do not depend on the choice of origin. 4: Induced group actions on R 3 × S 2 . Note that there are no more right actions, as SO( 2) is not a normal group of SO(3) nor SE(3). "Isotropy" means the "isotropy groups". "Fundamental" denotes the fundamental representation on R 3 .

Induced Riemannian and pseudo-Riemannian metrics g R µ was invariant by the right SO(2)-action. Thus, the projection onto R 3 × S 2 is a Riemannian submersion for g R µ . It induces a Riemannian metric on R 3 × S 2 , still denoted g R µ . g R µ is still SE(3)-and SO(3)-invariant.

Similarly, g BI was invariant by the right SO(2)-action. It induces a Riemannian pseudo-metric on R 3 × S 2 , which is still SE(3)-and SO(3)-invariant.

A sub-Riemannian metric As in 2D, one defines a sub-Riemannian metric g SR on R 3 × S 2 by first defining ∆. We take (X 1 , X 2 , X 3 , X 4 , X 5 ) on R 3 × S 2 as:

g SR is defined as the Euclidean metric on ∆. As in the 2D-case, it would be approximated by a Riemannian metric in practice.

A survey of curves From Table 1 and the aforementioned structures, we survey the curves on SE(3). However, we have a new class of curves in 3D-Neurogeometry w.r.t. 2D-Neurogeometry: the curves of the lifted space R 3 × S 2 that are projection of curves of SE(3), as the projection of the group geodesics.

In the following, "verticality" and "horizontality" are taken w.r.t. the right SO(2)-action. Projecting horizontal (g R µ ) Riemannian geodesics gives generalized Riemannian geodesics. Projecting horizontal (for g BI ) pseudo-Riemannian geodesics gives generalized pseudo-Riemannian geodesics. More precisely, a smooth horizontal curve in SE(3) is a (pseudo-) Riemannian geodesics if and only if it is a (pseudo-) Riemannian geodesics in R 3 × S 2 . The projection of vertical curves are points. The projection of a curve that is vertical at one point has a "cusp".

Ultimately, we have the curves that are ∆-horizontal in the sense of the sub-Riemannian geometry. Among them, we have sub-Riemannian geodesics.

Structure on the image domain R 3

The previous structures are projected to R 3 , using the projection of the trivial bundle R 3 × S 2 on the first component. In particular, projecting the previous curves give curves in R 3 . We have: the projection of the sub-Riemannian geodesics (an equivalent of 2D elastica curves), the double-projection of the group geodesics (equivalently the double-projection of the pseudo-Riemannian curves for g BI ), the double-projection of the Riemannian geodesics for g R µ .

Actions Metrics

(double-projection of g R µ ) Table 5: Structures of 3D-Neurogeometry. Use Table 1 to get the related curves.

The three steps

First step: Lift As in 2D, one lifts the medical image defined on D ⊂ R 3 to an image defined on D ⊂ R 3 × S 2 , using the gradient direction at each (x, y, z) ∈ D:

Second step: Processing First, as in 2D, the processing could be performed on R 3 × S 2 without taking into account the SE(3) structure. One would only consider the sub-Riemannian structure on the lifted space R 3 × S 2 . In doing so, one could define sub-Riemannian partial differential equations as in 2D-Neurogeometry, using the X i as differential operators. For in-painting purposes, the 2D work of [START_REF] Boscain | Hypoelliptic diffusion and human vision: A semidiscrete new twist[END_REF][15] provides intuition. Similarly, one could add drift (or convection) depending on the application. Then, in contrast to 2D, the processing can be performed on SE(3). This is done by embedding R 3 × S 2 in SE(3) as the quotient of SE(3) by a SO(2)action. Then, performing SO(2)-invariant computations on SE(3) is equivalent to performing computations on R 3 × S 2 . The advantage is that one has more structures, e.g. more curves for curve fitting (compare subsections 2.2 and 3.4). This is the first main distinction between the 2D and the 3D case. In 2D-Neurogeometry, we have one (trivial) quotient of R 2 × S 2 . In contrast in 3D-Neurogeometry, one has two successive quotients of SE(3) = R 3 × SO(3).

The second distinction is the existence of bi-invariant pseudo-metrics g BI in the 3D-case, but not in the 2D-case [START_REF] Miolane | Computing Bi-Invariant Pseudo-Metrics on Lie Groups for Consistent Statistics[END_REF]. As such, g BI could represent a new powerful tool of 3D-Neurogeometry. We note that in medical computer vision, the bi-invariant pseudo-metric g BI is rarely used as opposed to algorithms in robotics [START_REF] Zefran | On the generation of smooth three-dimensional rigid body motions[END_REF]. Considering its bi-invariance property, it would be interesting to consider it for the computations. For example, g BI characterizes the group geodesics of SE(3): this could simplify computations. g BI could replace the use of g R µ as an auxiliary metric, suppressing the need of a choice of µ.

Third step: Projection The projection of the lifted image to an image defined on R 3 could be defined in two different ways, exactly as in the 2D-case.

Conclusion

This paper is a theoretical toolbox for creating new algorithms for 3D medical computer vision. We have described the mathematical structures arising in the generalization of (2D-)Neurogeometry to 3D images.