Hypermap Specification and Certified Linked Implementation using Orbits

We propose a revised constructive specification and a certified hierarchized linked implementation of combinatorial hypermaps using a general notion of orbit. Combinatorial hypermaps help to prove theorems in algebraic topology and to develop algorithms in computational geometry. Orbits unify the presentation at conceptual and concrete levels and reduce the proof effort. All the development is formalized and verified in the Coq proof assistant. The implementation is easily proved observationally equivalent to the specification and translated in C language. Our method is transferable to a great class of algebraic specifications implemented into complex data structures with hierarchized linear, circular or symmetric linked lists, and pointer arrays.

J-F. Dufourd

Interactive Theorem Proving , Number 8558 , page 242--257 - 2014
Additionnal material

International conference with proceedings Hypermap Specification and Certified Linked Implementation using Orbits, Interactive Theorem Proving, Vienna, Austria, pages 242--257, Springer-Verlag, LNCS, n° 8558, juillet 2014, doi:10.1007/978-3-319-08970-6_16 Research team : IGG

 author = {Dufourd, J-F.},
 title = {Hypermap Specification and Certified Linked Implementation using Orbits},
 booktitle  = {Interactive Theorem Proving},
 number = {8558},
 series = {LNCS},
 pages = {242--257},
 month = {Jul},
 year = {2014},
 publisher = {Springer-Verlag},
 type = {Selective conference},
 doi = {10.1007/978-3-319-08970-6_16},
 x-international-audience = {Yes},
 x-language = {EN},
 url = {http://icube-publis.unistra.fr/4-Dufo14}

See publications of the same authors