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

LIP6, UPMC Sorbonne Universités - Paris 6
INRIA Rocquencourt

Résultats de recherche: Contribution à un journal › Article › Revue par des pairs

Résumé

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.

langue originale	Anglais
Pages (de - à)	337-363
Nombre de pages	27
journal	Journal of Automated Reasoning
Volume	29
Numéro de publication	3-4
Les DOIs	https://doi.org/10.1023/A:1021979218446
état	Publié - 1 déc. 2002
Modification externe	Oui

Accès au document

10.1023/A:1021979218446

Contient cette citation

@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

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

Résumé

Accès au document

Empreinte digitale

Contient cette citation