Research Method
Our methodology is a combination of theoretical research and technological development. The core is provided by the work package 1 (WP1) and the main tools will be provided by the Mathematical Components project. The goal of WP1 is to maintain and design these tools so that they can be used by the other work packages. WP2 shall first use the already existing tool SSReflect (Small Scale Reflect) for developing a basic library of linear algebra (Milestone 2). It will later, using the new tactics using reflections (Milestone 3) to be developed by WP1, build more sophisticated linear algebra (matrix over ring coefficients). This will be used by WP3 for representing the main algorithms of the system \Kenzo (Milestone 4), and by WP4 for representing theorems used in robotics (Milestone 5) and hybrid systems (Milestone 6).
Work package 1: Mathematical Interfaces and Reflexive Tactics
This work package is the core of the project, since it will maintain and develop the tools (mathematical components, interface, and tactics) used by the other work packages. The first part of the work package, on mathematical interface, will maintain the SSReflect library and extend it to allow a flexible access to mathematical structures and a convenient way to use reflexive tactics. The second part will develop these reflexive tactics, that are essential for the formal specification and development of mathematical software.
Work package 2: A library of Linear Algebra
This work package will develop a library of linear algebra. This work package is the mathematical core, since linear algebra plays a central role in most of the other tasks of this project. We intend to formalise most of the linear algebra program as taught in first-year university curricula.
Work package 3: A library of Homological Algebra and Algebraic Topology
This is the first mathematical application on homological algebra and algebraic topology. The team from La Rioja is developing a sophisticated computer algebra system (Kenzo) for computations in algebraic topology, and this work package intends to specify some crucial part of this software. The potential application will be to enhance topological processors of digital images, increasing the reliability of these software systems.
Work package 4: Computation with Real Numbers
This is the second mathematical application of this proposal, this time to real number computation and basic numerical analysis. One theme will be to use convex optimisation techniques, semi-definite programming, and exact real number computation to prove inequalities. The objectives will be the specification and implementation of a simple ODE solver, and a formal representation of Rohn's theorem. The potential applications are in robotics and hybrid systems.