Sites Inria

Version française

LEMME Research team

LEMME team publications

2019

Poster communications

titre
Smart framework for real-time monitoring and control of subsurface processes in managed aquifer recharge applications: project outlook
auteur
Jana Glass, Catalin Stefan, Cristiano Almeida, Christoph Sprenger, Chakrabarti Ronjon, Jean-Christophe Maréchal, Alexandre Duzan, Géraldine Picot-Colbeaux, Ralf Junghanns
article
10th International Symposium on Managed Aquifer Recharge - ISMAR10, May 2019, Madrid, Spain. 2019
Accès au texte intégral et bibtex
https://hal-brgm.archives-ouvertes.fr/hal-02355044/file/Smart-framework-for-real-time-monitoring-and-control-of-subsurface-processes-in-managed-aquifer-recharge-applications-project-outlook.pdf BibTex

2007

Journal articles

titre
Implementing the cylindrical algebraic decomposition within the Coq system
auteur
Assia Mahboubi
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2007, 17 (1), pp.99-127. ⟨10.1017/S096012950600586X⟩
Accès au bibtex
BibTex

2006

Conference papers

titre
Calcul de formules affines et de séries entières en arithmétique exacte avec types co-inductifs
auteur
Yves Bertot
article
Journées Francophones des Langages Applicatifs, INRIA, Jan 2006, Pauillac, pp.41-55
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000480/file/exactreals.pdf BibTex

2005

Conference papers

titre
Proving Equalities in a Commutative Ring Done Right in Coq
auteur
Assia Mahboubi, Benjamin Gregoire
article
TPHOLs 2005, Aug 2005, Oxford, United Kingdom. pp.98-113, ⟨10.1007/11541868_7⟩
Accès au bibtex
BibTex
titre
Programming and certifying a CAD algorithm in the Coq system
auteur
Assia Mahboubi
article
Dagstuhl Seminar 05021 - Mathematics, Algorithms, Proofs, Jan 2005, Dagstuhl, Germany
Accès au bibtex
BibTex

Reports

titre
Toward a geometric view on computations
auteur
Philippe Audebaud
article
RR-5492, INRIA. 2005, pp.16
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070515/file/RR-5492.pdf BibTex
titre
Simplifying Polynomial Expressions in a Proof Assistant
auteur
Laurent Théry
article
[Research Report] RR-5614, INRIA. 2005, pp.16
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070394/file/RR-5614.pdf BibTex

2004

Reports

titre
Vérification formelle d'extractions de racines
auteur
Yves Bertot
article
RR-5344, INRIA. 2004, pp.23
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070657/file/RR-5344.pdf BibTex
titre
Filters on Co-Inductive streams: an application to Eratosthenes' sieve
auteur
Yves Bertot
article
RR-5343, INRIA. 2004, pp.21
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070658/file/RR-5343.pdf BibTex
titre
Proof by reflection in semantics
auteur
Kuntal das Barman, Yves Bertot
article
RR-5134, INRIA. 2004
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071449/file/RR-5134.pdf BibTex

2003

Conference papers

titre
Pure Patterns Type Systems
auteur
Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori
article
Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, New Orleans, LA, USA — January 15 - 17, 2003, Jan 2003, New Orleans, United States. pp.250 - 261, ⟨10.1145/604131.604152⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00099463/file/2003-popl-03.pdf BibTex

Reports

titre
Premiers pas vers un cours de géométrie en Coq pour le lycée
auteur
Frédérique Guilhot
article
RR-4893, INRIA. 2003
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071689/file/RR-4893.pdf BibTex
titre
Simulation Logic, Applets and Compositional Verification
auteur
Christoph Sprenger, Dilian Gurov, Marieke Huisman
article
RR-4890, INRIA. 2003
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071692/file/RR-4890.pdf BibTex
titre
QArith: Coq Formalisation of Lazy Rational Arithmetic
auteur
Milad Niqui, Yves Bertot
article
[Research Report] RR-5004, INRIA. 2003, pp.19
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00077041/file/RR-5004.pdf BibTex
titre
A Table-Driven Compiler for Pretty Printing Specifications
auteur
Laurent Théry
article
[Technical Report] RT-0288, INRIA. 2003, pp.31
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00069891/file/RT-0288.pdf BibTex

Theses

titre
Changements de Représentation des Données dans le Calcul des Constructions
auteur
Nicolas Magaud
article
Génie logiciel [cs.SE]. Université Nice Sophia Antipolis, 2003. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00005903/file/tel-00005903.pdf BibTex

2002

Journal articles

titre
Interactive layout and handling of mathematical formulas in structured documents
auteur
Hanane Naciri, Laurence Rideau
article
Revue Africaine de la Recherche en Informatique et Mathématiques Appliquées, INRIA, 2002, 1, pp.95-125
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01261698/file/arima00105.pdf BibTex

Conference papers

titre
Élimination des quantificateurs sur les réels pour Coq
auteur
Assia Mahboubi, Loïc Pottier
article
Journées Francophones des Langages Applicatifs, Jan 2002, Anglet, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00819482/file/jfla02.pdf BibTex

Reports

titre
A Tour of Formal Verification with Coq:Knuth's Algorithm for Prime Numbers
auteur
Laurent Théry
article
RR-4600, INRIA. 2002
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071985/file/RR-4600.pdf BibTex
titre
Proofs with Coq of theorems in plane geometry using oriented angles
auteur
Frédérique Guilhot
article
RR-4356, INRIA. 2002
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072232/file/RR-4356.pdf BibTex
titre
Stålmarck's Algorithm in Coq: A Three-Level Approach
auteur
Laurent Théry
article
RR-4353, INRIA. 2002
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072235/file/RR-4353.pdf BibTex
titre
Proofs with Coq of theorems in plane geometry using oriented angles
auteur
Frédérique Guilhot
article
RR-4362, INRIA. 2002
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072226/file/RR-4362.pdf BibTex
titre
A proof of GMP square root using the Coq assistant
auteur
Yves Bertot, Nicolas Magaud, Paul Zimmermann
article
[Research Report] RR-4475, INRIA. 2002
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072113/file/RR-4475.pdf BibTex

2001

Conference papers

titre
A Generic Library for Floating-Point Numbers and Its Application to Exact Computing
auteur
Marc Daumas, Laurence Rideau, Laurent Thery
article
Theorem Proving in Higher Order Logics, 2001, Edinburgh, United Kingdom. pp.169-184
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00157285/file/DauRidThe01.pdf BibTex

Reports

titre
Mathematics and Proof Presentation in Pcoq
auteur
Ahmed Amerkad, Yves Bertot, Loïc Pottier, Laurence Rideau
article
RR-4313, INRIA. 2001
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072274/file/RR-4313.pdf BibTex
titre
An Integrated Development of Buchberger's Algorithm in Coq
auteur
Henrik Persson
article
RR-4271, INRIA. 2001
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072316/file/RR-4271.pdf BibTex
titre
une formalisation des faisceaux et des schémas affines en théorie des types avec Coq
auteur
Laurent Chicli
article
RR-4216, INRIA. 2001
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072403/file/RR-4216.pdf BibTex
titre
Affichage et manipulation interactive de formules mathématiques dans les documents structurés
auteur
Hanane Naciri, Laurence Rideau
article
RR-4140, INRIA. 2001
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072486/file/RR-4140.pdf BibTex

Preprints, Working Papers, ...

titre
Computer validated proofs of a toolset for adaptable arithmetic
auteur
Sylvie Boldo, Marc Daumas, Claire Moreau-Finot, Laurent Thery
article
2001
Accès au bibtex
https://arxiv.org/pdf/cs.MS/0107025 BibTex

2000

Conference papers

titre
A distributed editing environment for XML documents
auteur
Claude Pasquier, Laurent Théry
article
1st ECOOP Workshop on XML and Object Technology, Jun 2000, Sophia Antipolis, France
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00362451/file/paper.pdf BibTex

Reports

titre
Graphes de dépendance pour les démonstrateurs de théorèmes intéractifs
auteur
Yves Bertot, Olivier Pons, Loïc Pottier
article
RR-4052, INRIA. 2000
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072585/file/RR-4052.pdf BibTex
titre
Quotients dans le CCI
auteur
Loïc Pottier
article
RR-4053, INRIA. 2000
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072584/file/RR-4053.pdf BibTex
titre
Changements de représentation des données dans le calcul des constructions inductives
auteur
Nicolas Magaud, Yves Bertot
article
[Rapport de recherche] RR-4039, INRIA. 2000, pp.29
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072599/file/RR-4039.pdf BibTex
titre
A Coq Formalization of a Type Checker for Object Initialization in the Java Virtual Machine
auteur
Yves Bertot
article
[Research Report] RR-4047, INRIA. 2000, pp.53
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072591/file/RR-4047.pdf BibTex
titre
Extraction dans le Cci
auteur
Loïc Pottier
article
[Rapport de recherche] RR-4026, INRIA. 2000, pp.13
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072614/file/RR-4026.pdf BibTex

1999

Conference papers

titre
On-Line Handwritten Formula Recognition using Hidden Markov Models and Context Dependent Graph Grammars
auteur
Andreas Kosmala, Gerhard Rigoll, Stéphane Lavirotte, Loïc Pottier
article
Fifth International Conference on Document Analysis and Recognition, IEEE Computer Society, Sep 1999, Bangalore, India
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00564645/file/kosmala-rigoll-etal_1999.pdf BibTex

Poster communications

titre
On-line handwritten formula recognition using hidden Markov models and context dependent graph grammars
auteur
Andreas Kosmala, Gerhard Rigoll, Stéphane Lavirotte, Loïc Pottier
article
International Conference on Document Analysis and Recognition, Sep 1999, Bangalore, India. 1999, Proceeding of the Fifth International Conference on Document Analysis and Recognition. ⟨10.1109/ICDAR.1999.791736⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01349212/file/kosmala-rigoll-etal1999.pdf BibTex

1998

Conference papers

titre
Mathematical formula recognition using graph grammar
auteur
Stéphane Lavirotte, Loïc Pottier
article
Electronic Imaging, Jan 1998, San José, United States
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01349210/file/ei98.pdf BibTex