@inproceedings{b8cf5d9eda8a43f6bc160e7c0e6e9ca5,
title = "Algebraic structures and dependent records",
abstract = "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.",
author = "Virgile Prevosto and Damien Doligez and Th{\'e}r{\`e}se Hardin",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2002.; 15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002 ; Conference date: 20-08-2002 Through 23-08-2002",
year = "2002",
month = jan,
day = "1",
doi = "10.1007/3-540-45685-6\_20",
language = "English",
isbn = "3540440399",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "298--313",
editor = "Carreno, \{Victor A.\} and Munoz, \{Cesar A.\} and Sofiene Tahar",
booktitle = "Theorem Proving in Higher Order Logics - 15th International Conference, TPHOLs 2002, Proceedings",
}