Références

1

<< Action Coopérative "Calcul Formel Certifié" >>.
INRIA, http://www.inria. fr/croap/CFC/in dex.html.

2

<< Certification d'une implantation de PGP >>.
Proposition de stage 1999, INRIA, CROAP, http://www.inria.fr/croap/stages99/p gp.html.

3

<< Géométrie algorithmique certifiée >>.
Proposition de stage 1999, INRIA, CROAP, http://www-sop.inria.fr/croap/stages99/ geometrie.html.

4

Bruno BARRAS BENJAMIN WERNER .
<< COQ IN COQ >>.
JOURNAL OF AUTOMATED REASONING, À PARA^ITRE.

1

BENJAMIN P. BERMAN RICHARD J. FATEMAN .
<< OPTICAL CHARACTER RECOGNITION FOR TYPESET MATHEMATICS >>.
INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION (ISSAC'94), 348-353, OXFORD, 1994. ACM.

2

YVES BERTOT .
<< DIRECT MANIPULATION OF ALGEBRAIC FORMULAE IN INTERACTIVE PROOF SYSTEMS >>.
ELECTRONIC PROCEEDINGS FOR THE CONFERENCE UITP'97, SOPHIA ANTIPOLIS, 1997.

3

YVES BERTOT .
<< HEAD-TACTICS SIMPLIFICATION >>.
ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, 1349 LECTURE NOTES IN COMPUTER SCIENCE, SYDNEY, AUSTRALIE, 1997. SPRINGER VERLAG.

4

YVES BERTOT .
<< A CERTIFIED COMPILER FOR AN IMPERATIVE LANGUAGE >>.
RAPPORT DE RECHERCHE RR-3488, INRIA, 1998.

5

YVES BERTOT .
<< THE CTCOQ SYSTEM: DESIGN AND ARCHITECTURE >>.
RAPPORT DE RECHERCHE RR-3540, INRIA, 1998.

6

YVES BERTOT RANAN FRAER .
<< REASONING WITH EXECUTABLE SPECIFICATIONS >>.
PROCEEDINGS OF THE INTERNATIONAL JOINT CONFERENCE ON THEORY AND PRACTICE OF SOFTWARE DEVELOPMENT (TAPSOFT'95), 915 LECTURE NOTES IN COMPUTER SCIENCE, 531-545, AARHUS, DANEMARK, 1995.

11

YVES BERTOT , GILLES KAHN , LAURENT THÉRY .
<< PROOF BY POINTING >>.
THEORETICAL ASPECTS OF COMPUTER SOFTWARE, 789 LECTURE NOTES IN COMPUTER SCIENCE, 141-160, SENDAI, JAPAN, 1994.

7

YVES BERTOT , THOMAS KLEYMANN-SCHREIBER , DILIP SEQUEIRA .
<< IMPLEMENTING PROOF BY POINTING WITHOUT A STRUCTURE EDITOR >>.
TECHNICAL REPORT ECS-LFCS-97-368, UNIVERSITÉ D'´EDIMBOURG, 1997.
ÉGALEMENT RAPPORT DE RECHERCHE INRIA 3286.

8

YVES BERTOT LAURENT THÉRY .
<< A GENERIC APPROACH TO BUILDING USER INTERFACES FOR THEOREM PROVERS >>.
JOURNAL OF SYMBOLIC COMPUTATION, 25:161-194, 1998.

9

DOMINIQUE BOLIGNANO .
<< TOWARDS A MECHANIZATION OF CRYPTOGRAPHIC PROTOCOL VERIFICATION >>.
PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON COMPUTER-AIDED VERIFICATION (CAV'97), 1997.

10

SAMUEL BOUTIN .
<< RÉFLEXIONS SUR LES QUOTIENTS >>.
THÈSE D'UNIVERSITÉ, PARIS 7, AVRIL 1997.

11

N. G. DE BRUIJN .
<< TELESCOPIC MAPPINGS IN TYPED LAMBDA CALCULUS >>.
INFORMATION AND COMPUTATION, 91(2):189-204, 1991.

12

BRUNO BUCHBERGER , TUDOR JEBELEAN , FRANZ KRIFTNER , MIRCEA MARIN , ELENA TOMUTA , DANIELA VASARU .
<< A SURVEY ON THE THEOREMA PROJECT >>.
INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION (ISSAC'97), MAUI, HAWAII, 1997. ACM.

13

EDMUND M. CLARKE JEANNETTE M. WING .
<< FORMAL METHODS: STATE OF THE ART AND FUTURE DIRECTIONS >>.
ACM SURVEY, 1997.
HTTP://WWW.CS.CMU.EDU/AFS/CS/PROJECT/CALDER/WWW/ACM.HTML .

14

PROJET COQ .
<< CONTRIBUTIONS AU SYSTÈME COQ >>.
HTTP://PAUILLAC.INRIA.FR/COQ/CONTRIB S-FRA.HTML.

15

YANN COSCOY , GILLES KAHN , LAURENT THÉRY .
<< EXTRACTING TEXT FROM PROOF >>.
PROCEEDINGS OF "TYPED LAMBDA-CALCULI AND APPLICATIONS" (TLCA `95), 905 LNCS, EDIMBOURG, 1995. SPRINGER-VERLAG, 1995.

16

JOËLLE DESPEYROUX .
<< PROOF OF TRANSLATION IN NATURAL SEMANTICS >>.
SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, 193-205, CAMBRIDGE, MASSACHUSETTS, JUIN 1986. IEEE COMPUTER SOCIETY.

17

PHILIPPE FLAJOLET , XAVIER GOURDON , DANIEL PANARIO .
<< THE COMPLETE ANALYSIS OF A POLYNOMIAL FACTORIZATION ALGORITHM OVER FINITE FIELDS >>.
RAPPORT DE RECHERCHE 3370, INRIA, MARS 1998.

18

KEITH O. GEDDES , STEPHEN R. CZAPOR , GEORGE LABAHN .
ALGORITHMS FOR COMPUTER ALGEBRA.
KLUWER, 1992.

19

JOHN R. HARRISON .
THEOREM PROVING WITH THE REAL NUMBERS.
SPRINGER-VERLAG, 1998.

20

GILLES KAHN .
<< NATURAL SEMANTICS >>.
K. FUCHI MAURICE NIVAT , , PROGRAMMING OF FUTURE GENERATION COMPUTERS. NORTH-HOLLAND, 1988.
(ÉGALEMENT RAPPORT DE RECHERCHE INRIA NO. 601).

21

ANDREAS KOSMALA , JOERG ROTTLAND , GERHARD RIGOLL .
<< IMPROVED ON-LINE HANDWRITING RECOGNITION USING CONTEXT DEPENDENT HIDDEN MARKOV MODEL >>.
PROC. OF INTERNATIONAL CONFERENCE ON DOCUMENT ANALYSIS AND RECOGNITION (ICDAR'97), ULM, ALLEMAGNE, 1997.

22

STÉPHANE LAVIROTTE LOÏC POTTIER .
<< OPTICAL FORMULA RECOGNITION >>.
"PROC. OF INTERNATIONAL CONFERENCE ON DOCUMENT ANALYSIS AND RECOGNITION (ICDAR'97)", ULM, ALLEMAGNE, 1997.

23

STÉPHANE LAVIROTTE LOÏC POTTIER .
<< MATHEMATICAL FORMULA RECOGNITION USING GRAPH GRAMMAR >>.
IS&T/SPIE'S 10TH INTERNATIONAL SYMPOSIUM ``ELECTRONIC IMAGING: SCIENCE AND TECHNOLOGY'', SAN JOSE, USA, 1998.

24

PIERRE LETOUZEY .
<< ALGORITHME CERTIFIÉ DE STÅLMARCK >>.
STAGE DE PREMIÈRE ANNÉE, ENS ULM, SEPTEMBRE 1998.
HTTP://WWW.ELEVES.ENS.FR:8080/HOME/LETOUZEY/RAPPORT.PS.G Z.

25

FRANÇOIS MAUREL .
<< FACTORISATION DE POLYNÔMES À COEFFICIENTS DANS UN CORPS FINI >>.
STAGE DE PREMIÈRE ANNÉE, ENS ULM, SEPTEMBRE 1998.

26

JEAN-FRANÇOIS MONIN .
COMPRENDRE LES MÉTHODES FORMELLES.
COLLECTION TECHNIQUE ET SCIENTIFIQUE DES TÉLÉCOMMUNICATIONS. MASSON, PARIS, MILAN, BARCELONE, 1996.

27

BENGT NORDSTR¨OM .
<< TERMINATING GENERAL RECURSION >>.
BIT, 28, 1988.

28

MARIS A. OZOLS , KATHERINE A. EASTAUGHFFE , ANTONY CANT .
<< XISABELLE: A SYSTEM DESCRIPTION >>.
AUTOMATED DEDUCTION (CADE-14), 1249 LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, 400-403, TOWNSVILLE, NORTH QUEENSLAND, AUSTRALIE, 1997. SPRINGER-VERLAG.

29

CHRISTINE PAULIN-MOHRING .
<< INDUCTIVE DEFINITIONS IN THE SYSTEM COQ - RULES A ND PROPERTIES >>.
M. BEZEM J.-F. GROOTE , , PROCEEDINGS OF THE CONFERENCE TYPED LAMBDA CALCULI A ND APPLICATIONS, 664 LECTURE NOTES IN COMPUTER SCIENCE, 1993.
LIP RESEARCH REPORT 92-49.

30

CHRISTINE PAULIN-MOHRING BENJAMIN WERNER .
<< SYNTHESIS OF ML PROGRAMS IN THE SYSTEM COQ >>.
JOURNAL OF SYMBOLIC COMPUTATION, 15:607-640, 1993.

31

LAWRENCE C. PAULSON TOBIAS NIPKOW .
ISABELLE : A GENERIC THEOREM PROVER, 828 LECTURE NOTES IN COMPUTER SCIENCE.
SPRINGER-VERLAG, 1994.

32

LOÏC POTTIER .
<< CERTIFICATION D'ALGORITHMES EN COQ >>.
SÉMINAIRE ENS-LYON, INRIA, JUIN 1997.

33

LOÏC POTTIER .
<< MATHEMATICAL FORMULA RECOGNITION >>.
"INTERNATIONAL WORKSHOP ON RETRODIGITALIZATION OF MATHEMATICAL DOCUMENTS", ESSEN, ALLEMAGNE, 1997.

34

LOÏC POTTIER .
<< UN DÉBUT DE FORMALISATION DE L'ALGÈBRE EN COQ ET CTCOQ >>.
RAPPORT DE RECHERCHE À PARAÎTRE, INRIA, 1998.

35

LOÏC POTTIER LAURENT THÉRY .
<< CERTIFIED COMPUTER ALGEBRA >>.
CALCULEMUS WORKSHOP, EINDHOVEN, JUILLET 1998.
EXTENDED ABSTRACT.

36

DELPHINE TERRASSE .
<< ENCODING NATURAL SEMANTICS IN COQ >>.
PROCEEDINGS OF THE FOURTH INTERNATIONAL CONFERENCE ON ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, AMAST'95, SPRINGER-VERLAG LNCS, JUILLET 1995.

37

DELPHINE TERRASSE .
<< VERS UN ENVIRONNEMENT D'AIDE AU DÉVELOPPEMENT DE PREUVES EN SÉMANTIQUE NATURELLE >>.
PHD THESIS, ECOLE NATIONALE DES PONTS ET CHAUSSÉES, 1995.

38

LAURENT THÉRY .
<< A PROOF DEVELOPMENT SYSTEM FOR THE HOL THEOREM PROVER >>.
PROCEEDINGS OF THE 6TH INTERNATIONAL WORKSHOP ON HIGHER ORDER LOGIC THEOREM PROVING AND ITS APPLICATIONS (HUG'93), 780 LNCS, 115-128, VANCOUVER, AOÛT 1993. SPRINGER-VERLAG, 1994.

39

LAURENT THÉRY .
<< A CERTIFIED VERSION OF BUCHBERGER'S ALGORITHM >>.
AUTOMATED DEDUCTION--CADE-15, 1421 LNAI, 349-364. SPRINGER-VERLAG, 1998.

40

LAURENT THÉRY , YVES BERTOT , GILLES KAHN .
<< REAL THEOREM PROVERS DESERVE REAL USER-INTERFACES >>.
SOFTWARE ENGINEERING NOTES, 17(5):120-129, 1992.
5TH SYMPOSIUM ON SOFTWARE DEVELOPMENT ENVIRONMENTS.