OrienRepr is a formal verification project in Coq, for "Orientation Representation (OR)" problem, which is focused on derivation of popular models or algorithms for OR, including Euler Angles, Rotation Matrices, Axis-Angles, and Unit Quaternion.
Note that, OrienRepr project is part of VFCS (Verified Flight Control System) project, which is not published for now.
This project need FinMatrix library, which is a formal matrix library in Coq, and located in FinMatrix project.
Below are main links of this project: