Calcul Formel et Preuves Formelles

Assia Mahboubi

doi:10.5802/ccirm.27

Assia Mahboubi

Les cours du CIRM, Tome 6 (2018) no. 1, Exposé no. 2, 10 p.

Publié le : 2019-01-28

DOI : 10.5802/ccirm.27

@article{CCIRM_2018__6_1_A2_0,
     author = {Assia Mahboubi},
     title = {Calcul {Formel} et {Preuves} {Formelles}},
     journal = {Les cours du CIRM},
     note = {talk:2},
     publisher = {CIRM},
     volume = {6},
     number = {1},
     year = {2018},
     doi = {10.5802/ccirm.27},
     language = {fr},
     url = {https://ccirm.centre-mersenne.org/articles/10.5802/ccirm.27/}
}

TY  - JOUR
AU  - Assia Mahboubi
TI  - Calcul Formel et Preuves Formelles
JO  - Les cours du CIRM
N1  - talk:2
PY  - 2018
VL  - 6
IS  - 1
PB  - CIRM
UR  - https://ccirm.centre-mersenne.org/articles/10.5802/ccirm.27/
DO  - 10.5802/ccirm.27
LA  - fr
ID  - CCIRM_2018__6_1_A2_0
ER  -

%0 Journal Article
%A Assia Mahboubi
%T Calcul Formel et Preuves Formelles
%J Les cours du CIRM
%Z talk:2
%D 2018
%V 6
%N 1
%I CIRM
%U https://ccirm.centre-mersenne.org/articles/10.5802/ccirm.27/
%R 10.5802/ccirm.27
%G fr
%F CCIRM_2018__6_1_A2_0

Assia Mahboubi. Calcul Formel et Preuves Formelles. Les cours du CIRM, Tome 6 (2018) no. 1, Exposé no. 2, 10 p. doi : 10.5802/ccirm.27. https://ccirm.centre-mersenne.org/articles/10.5802/ccirm.27/

Bibliographie
Cité par

[1] Evmorfia-Iro Bartzia; Pierre-Yves Strub A Formal Library for Elliptic Curves in the Coq Proof Assistant, Interactive Theorem Proving (2014), pp. 77-92 | DOI | Zbl

[2] Yves Bertot; Pierre Castran Interactive Theorem Proving and Program Development : Coq’Art The Calculus of Inductive Constructions, Springer Publishing Company, Incorporated, 2010 | Zbl

[3] Mathieu Boespflug; Maxime Dénès; Benjamin Grégoire Full reduction at full throttle, First International Conference on Certified Programs and Proofs, Tawain, December 7-9 (Lecture Notes in Computer Science) (2011) | DOI

[4] Sascha Böhme; Tobias Nipkow Sledgehammer : Judgement Day, Proceedings of the 5th International Conference on Automated Reasoning (IJCAR’10) (2010), pp. 107-121 | DOI | Zbl

[5] Alin Bostan; FrÃ©dÃ©ric Chyzak; Marc Giusti; Romain Lebreton; GrÃ©goire Lecerf; Bruno Salvy; Éric Schost Algorithmes Efficaces en Calcul Formel, FrÃ©dÃ©ric Chyzak (auto-Ã©dit.), Palaiseau, 2017 https://hal.archives-ouvertes.fr/AECF/ (686 pages. ImprimÃ© par CreateSpace. Aussi disponible en version Ã©lectronique)

[6] Nicolas Bourbaki L’architecture des mathÃ©matiques, Les grands courants de la pensÃ©e mathÃ©matique (FranÃ§ois Le Lionnais, ed.), Cahiers du Sud, 1948

[7] Robert S. Boyer; Matt Kaufmann; J S. Moore The Boyer-Moore theorem prover and its interactive enhancement, Computers & Mathematics with Applications, Volume 29 (1995) no. 2, pp. 27 -62 http://www.sciencedirect.com/science/article/pii/0898122194002157 | DOI | MR

[8] Robert S. Boyer; J S. Moore Proving Theorems About LISP Functions, J. ACM, Volume 22 (1975) no. 1, pp. 129-144 http://doi.acm.org/10.1145/321864.321875 | DOI | MR | Zbl

[9] Bishop Brock; Matt Kaufmann; J S. Moore ACL2 theorems about commercial microprocessors, Formal Methods in Computer-Aided Design (1996), pp. 275-293 | DOI

[10] Thierry Coquand Catarina Coquand Structured type theory, Workshop on Logical Frameworks and Metalanguages (1999) | Zbl

[11] Alonzo Church A Formulation of the Simple Theory of Types, J. Symbolic Logic, Volume 5 (1940) no. 2, pp. 56-68 https://projecteuclid.org:443/euclid.jsl/1183387805 | DOI | MR | Zbl

[12] Frédéric Chyzak; Assia Mahboubi; Thomas Sibut-Pinote; Enrico Tassi A Computer-Algebra-Based Formal Proof of the Irrationality of $ζ$ (3), Interactive Theorem Proving (Lecture Notes in Computer Science), Volume 8558 (2014) | DOI | Zbl

[13] Cyril Cohen; Assia Mahboubi Formal proof in real algebraic geometry : from ordered fields to quantifier elimination, Logical Methods in Computer Sciences, Volume 8 (2012) no. 1 :2, pp. 1-40 | MR | Zbl

[14] Thierry Coquand Une thÃ©orie des constructions, Paris 7 (1985), 1 Vol. (92 p.) pages http://www.theses.fr/1985PA07F126 (Ph. D. Thesis)

[15] Leonardo MendonÃ§a de Moura; Soonho Kong; Jeremy Avigad; Floris van Doorn; Jakob von Raumer The Lean Theorem Prover (System Description)., CADE (Lecture Notes in Computer Science), Volume 9195 (2015), pp. 378-388 http://dblp.uni-trier.de/db/conf/cade/cade2015.html#MouraKADR15 | MR | Zbl

[16] Manuel Eberl Proving Divide and Conquer Complexities in Isabelle/HOL, J. Autom. Reason., Volume 58 (2017) no. 4, pp. 483-508 | DOI | MR | Zbl

[17] Kurt Gödel Über Formal Unentscheidbare Sätze der Principia Mathematica und Verwandter Systeme, I, Monatshefte für Math.u.Physik, Volume 38 (1931), pp. 173-198 | DOI | Zbl

[18] Benjamin Grégoire; Xavier Leroy A compiled implementation of strong reduction, International Conference on Functional Programming 2002 (2002), pp. 235-246 | Zbl

[19] Benjamin Grégoire; Laurent Théry; Benjamin Werner A Computational Approach to Pocklington Certificates in Type Theory, Functional and Logic Programming, 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006, Proceedings (Lecture Notes in Computer Science), Volume 3945 (2006), pp. 97-113 | Zbl

[20] Thomas Hales; Mark Adams; Gertrud Bauer; Tat Dat Dang; John Harrison; Le Truong Hoang; Cezary Kaliszyk; Victor Magron; Sean McLaughlin; Tat Thang Nguyen; et al. A formal proof of the Kepler conjecture, Forum of Mathematics, Pi, Volume 5 (2017) | DOI | MR | Zbl

[21] Thomas C. Hales A proof of the Kepler conjecture, Annals of Mathematics, Volume 162 (2005) no. 3, pp. 1065-1185 | MR | Zbl

[22] John Harrison HOL Light : A Tutorial Introduction, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD’96) (Lecture Notes in Computer Science), Volume 1166 (1996), pp. 265-269 | DOI

[23] John Harrison Floating-Point Verification using Theorem Proving, Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006 (Lecture Notes in Computer Science), Volume 3965 (2006), pp. 211-242

[24] John Harrison Verifying nonlinear real formulas via sums of squares, Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007 (Lecture Notes in Computer Science), Volume 4732 (2007), pp. 102-118 | MR

[25] John Harrison Formal proofs of hypergeometric sums (Dedicated to the memory of Andrzej Trybulec), Journal of Automated Reasoning, Volume 55 (2015), pp. 223-243 | DOI | MR | Zbl

[26] John Harrison; Laurent Théry A Skeptic’s Approach to Combining HOL and Maple, J. Autom. Reason., Volume 21 (1998) no. 3, pp. 279-294 | DOI | MR | Zbl

[27] Marijn J.H. Heule Schur Number Five, https://arxiv.org/abs/1711.08076, 2018 (Accepted for publication at AAAI 2018)

[28] Fabian Immler A Verified Enclosure for the Lorenz Attractor (Rough Diamond), Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings (2015), pp. 221-226 | DOI | Zbl

[29] William Stanley Jevons On the Mechanical Performance of Logical Inference, Philosophical Transactions of the Royal Society of London for the year 1870, Volume 160 II, Taylor and Francis, 1870, pp. 497-518

[30] Matt Kaufmann; J S. Moore An Industrial Strength Theorem Prover for a Logic Based on Common Lisp, IEEE Trans. Softw. Eng., Volume 23 (1997) no. 4, pp. 203-213 | DOI

[31] Assia Mahboubi Un ordinateur pour vÃ©rifier des preuves mathÃ©matiques, Images des MathÃ©matiques, en partenariat avec le sÃ©minaire Bourbaki, 2014 (http://images.math.cnrs.fr/Un-ordinateur-pour-verifier-les.html)

[32] Assia Mahboubi; Guillaume Melquiond; Thomas Sibut-Pinote Formally Verified Approximations of Definite Integrals (2017) (Under review) | HAL | Zbl

[33] Erik Martin-Dorel; Pierre Roux A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations (regular paper), ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), Paris, 16/01/2017-17/01/2017 (2017), pp. 90-99 | DOI

[34] Per Martin-Löf; Giovanni Sambin Intuitionistic type theory, Studies in proof theory, Bibliopolis, 1984 https://books.google.fr/books?id=_D0ZAQAAIAAJ

[35] Robin Milner Lcf : A way of doing proofs with a machine, Mathematical Foundations of Computer Science 1979 (1979), pp. 146-159 | DOI | Zbl

[36] Selected Papers on Automath (Rob Nederpelt; Herman Geuvers; Roel de Vrijer, eds.), Studies in Logic and the Foundations of Mathematics, 133, North-Holland, 1994 | MR

[37] Tobias Nipkow; Gertrud Bauer; Paula Schultz Flyspeck I : Tame Graphs, Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (2006), pp. 21-35 | DOI | Zbl

[38] Tobias Nipkow; Markus Wenzel; Lawrence C. Paulson Isabelle/HOL : A Proof Assistant for Higher-order Logic, Springer-Verlag, Berlin, Heidelberg, 2002 | Zbl

[39] Alexey Solovyev Formal Computations and Methods, University of Pittsburgh (2012) (Ph. D. Thesis) | MR

[40] Andrzej Trybulec The MIZAR-QC/6000 logic information language, Association for Literary and Linguistic Computing Bulletin, Volume 6 (1978), pp. 136-140

[41] Warwick Tucker A Rigorous ODE Solver and Smale’s 14th Problem, Foundations of Computational Mathematics, Volume 2 (2002) no. 1, pp. 53-117 | DOI | MR | Zbl

[42] The Univalent Foundations Program Homotopy Type Theory : Univalent Foundations of Mathematics, https://homotopytypetheory.org/book, Institute for Advanced Study, 2013 | Zbl

[43] Lambert S. van Benthem Jutting Checking Landau’s « Grundlagen » in the automath system, Mathematical Centre tracts, Mathematisch Centrum, 1979 https://books.google.fr/books?id=xwjwngEACAAJ | Zbl

[44] Freek Wiedijk The Seventeen Provers of the World : Foreword by Dana S. Scott (Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence), Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2006

Cité par Sources :