Algorithms and proofs inheritance in the FOC language

Virgile Prevosto; Damien Doligez

doi:10.1023/A:1021979218446

Algorithms and proofs inheritance in the FOC language

Virgile Prevosto
, Damien Doligez

Research output: Contribution to journal › Article › peer-review

Abstract

In this paper, we present the FOC language, dedicated to the development of certified computer algebra libraries (that is sets of programs). These libraries are based on a hierarchy of implementations of mathematical structures. After presenting the core set of features of our language, we describe the static analyses, which reject inconsistent programs. We then show how we translate FOC definitions into OCAML and Coq, our target languages for the computational part and the proof checking, respectively.

Original language	English
Pages (from-to)	337-363
Number of pages	27
Journal	Journal of Automated Reasoning
Volume	29
Issue number	3-4
DOIs	https://doi.org/10.1023/A:1021979218446
Publication status	Published - 1 Dec 2002
Externally published	Yes

Keywords

Computer algebra
FOC language

Access to Document

10.1023/A:1021979218446

Cite this

@article{606061607f204cd5a19a658b6d31e948,

title = "Algorithms and proofs inheritance in the FOC language",

abstract = "In this paper, we present the FOC language, dedicated to the development of certified computer algebra libraries (that is sets of programs). These libraries are based on a hierarchy of implementations of mathematical structures. After presenting the core set of features of our language, we describe the static analyses, which reject inconsistent programs. We then show how we translate FOC definitions into OCAML and Coq, our target languages for the computational part and the proof checking, respectively.",

keywords = "Computer algebra, FOC language",

author = "Virgile Prevosto and Damien Doligez",

year = "2002",

month = dec,

day = "1",

doi = "10.1023/A:1021979218446",

language = "English",

volume = "29",

pages = "337--363",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

number = "3-4",

}

TY - JOUR

T1 - Algorithms and proofs inheritance in the FOC language

AU - Prevosto, Virgile

AU - Doligez, Damien

PY - 2002/12/1

Y1 - 2002/12/1

N2 - In this paper, we present the FOC language, dedicated to the development of certified computer algebra libraries (that is sets of programs). These libraries are based on a hierarchy of implementations of mathematical structures. After presenting the core set of features of our language, we describe the static analyses, which reject inconsistent programs. We then show how we translate FOC definitions into OCAML and Coq, our target languages for the computational part and the proof checking, respectively.

AB - In this paper, we present the FOC language, dedicated to the development of certified computer algebra libraries (that is sets of programs). These libraries are based on a hierarchy of implementations of mathematical structures. After presenting the core set of features of our language, we describe the static analyses, which reject inconsistent programs. We then show how we translate FOC definitions into OCAML and Coq, our target languages for the computational part and the proof checking, respectively.

KW - Computer algebra

KW - FOC language

UR - https://www.scopus.com/pages/publications/0036992174

U2 - 10.1023/A:1021979218446

DO - 10.1023/A:1021979218446

M3 - Article

AN - SCOPUS:0036992174

SN - 0168-7433

VL - 29

SP - 337

EP - 363

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 3-4

ER -

Algorithms and proofs inheritance in the FOC language

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this