TY - GEN
T1 - Algebraic structures and dependent records
AU - Prevosto, Virgile
AU - Doligez, Damien
AU - Hardin, Thérèse
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2002.
PY - 2002/1/1
Y1 - 2002/1/1
N2 - In mathematics, algebraic structures are defined according to a rather strict hierarchy: rings come up after groups, which rely themselves on monoids, and so on. In the Foe project, we represent these structures by species. A species is made up of algorithms as well as proofs that these algorithms meet their specifications, and it can be built from existing species through inheritance and refinement mechanisms. To avoid inconsistencies, these mechanisms must be used carefully. In this paper, we recall the conditions that must be fulfilled when going from a species to another, as formalized by S. Boulme in his PhD [3]. We then show how these conditions can be checked through a static analysis of the Foe code. Finally, we describe how to translate Foe declarations into Coq.
AB - In mathematics, algebraic structures are defined according to a rather strict hierarchy: rings come up after groups, which rely themselves on monoids, and so on. In the Foe project, we represent these structures by species. A species is made up of algorithms as well as proofs that these algorithms meet their specifications, and it can be built from existing species through inheritance and refinement mechanisms. To avoid inconsistencies, these mechanisms must be used carefully. In this paper, we recall the conditions that must be fulfilled when going from a species to another, as formalized by S. Boulme in his PhD [3]. We then show how these conditions can be checked through a static analysis of the Foe code. Finally, we describe how to translate Foe declarations into Coq.
UR - https://www.scopus.com/pages/publications/33745642354
U2 - 10.1007/3-540-45685-6_20
DO - 10.1007/3-540-45685-6_20
M3 - Conference contribution
AN - SCOPUS:33745642354
SN - 3540440399
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 298
EP - 313
BT - Theorem Proving in Higher Order Logics - 15th International Conference, TPHOLs 2002, Proceedings
A2 - Carreno, Victor A.
A2 - Munoz, Cesar A.
A2 - Tahar, Sofiene
PB - Springer Verlag
T2 - 15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002
Y2 - 20 August 2002 through 23 August 2002
ER -