Calcul Formel et Preuves Formelles

Mahboubi, Assia

Journées Nationales de Calcul Formel. 22 – 26 Janvier 2018, Les cours du CIRM, no. 1 (2018), Exposé no. 2, 10 p.

DOI : 10.5802/ccirm.27

@article{CCIRM_2018__6_1_A2_0,
     author = {Mahboubi, Assia},
     title = {Calcul {Formel} et {Preuves} {Formelles}},
     booktitle = {Journ\'ees Nationales de Calcul Formel. 22 {\textendash} 26 Janvier 2018},
     series = {Les cours du CIRM},
     note = {talk:2},
     pages = {1--10},
     publisher = {CIRM},
     number = {1},
     year = {2018},
     doi = {10.5802/ccirm.27},
     language = {fr},
     url = {http://archive.numdam.org/articles/10.5802/ccirm.27/}
}

TY  - JOUR
AU  - Mahboubi, Assia
TI  - Calcul Formel et Preuves Formelles
BT  - Journées Nationales de Calcul Formel. 22 – 26 Janvier 2018
AU  - Collectif
T3  - Les cours du CIRM
N1  - talk:2
PY  - 2018
SP  - 1
EP  - 10
IS  - 1
PB  - CIRM
UR  - http://archive.numdam.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 Mahboubi, Assia
%T Calcul Formel et Preuves Formelles
%B Journées Nationales de Calcul Formel. 22 – 26 Janvier 2018
%A Collectif
%S Les cours du CIRM
%Z talk:2
%D 2018
%P 1-10
%N 1
%I CIRM
%U http://archive.numdam.org/articles/10.5802/ccirm.27/
%R 10.5802/ccirm.27
%G fr
%F CCIRM_2018__6_1_A2_0

Mahboubi, Assia. Calcul Formel et Preuves Formelles, dans Journées Nationales de Calcul Formel. 22 – 26 Janvier 2018, Les cours du CIRM, no. 1 (2018), Exposé no. 2, 10 p. doi : 10.5802/ccirm.27. http://archive.numdam.org/articles/10.5802/ccirm.27/

Bibliographie
Cité par

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

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

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

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

[5] Bostan, Alin; Chyzak, FrÃ©dÃ©ric; Giusti, Marc; Lebreton, Romain; Lecerf, GrÃ©goire; Salvy, Bruno; Schost, Éric 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] Bourbaki, Nicolas L’architecture des mathÃ©matiques, Les grands courants de la pensÃ©e mathÃ©matique (Lionnais, FranÃ§ois Le, ed.), Cahiers du Sud, 1948

[7] Boyer, Robert S.; Kaufmann, Matt; Moore, J S. 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] Boyer, Robert S.; Moore, J S. 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] Brock, Bishop; Kaufmann, Matt; Moore, J S. ACL2 theorems about commercial microprocessors, Formal Methods in Computer-Aided Design (Srivas, Mandayam; Camilleri, Albert, eds.), Springer Berlin Heidelberg, Berlin, Heidelberg (1996), pp. 275-293 | DOI

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

[11] Church, Alonzo 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] Chyzak, Frédéric; Mahboubi, Assia; Sibut-Pinote, Thomas; Tassi, Enrico A Computer-Algebra-Based Formal Proof of the Irrationality of $ζ$ (3), Interactive Theorem Proving (Gerwin Klein, Ruben Gamboa, ed.) (Lecture Notes in Computer Science), Volume 8558, Springer (2014) | DOI | Zbl

[13] Cohen, Cyril; Mahboubi, Assia 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] Coquand, Thierry Une thÃ©orie des constructions, Paris 7 (1985), 1 Vol. (92 p.) pages http://www.theses.fr/1985PA07F126 (Ph. D. Thesis ThÃ¨se de doctorat dirigÃ©e par Huet, GÃ©rard)

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

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

[17] Gödel, Kurt Ü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] Grégoire, Benjamin; Leroy, Xavier A compiled implementation of strong reduction, International Conference on Functional Programming 2002, ACM Press (2002), pp. 235-246 | Zbl

[19] Grégoire, Benjamin; Théry, Laurent; Werner, Benjamin 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, Springer (2006), pp. 97-113 | Zbl

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

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

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

[23] Harrison, John 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 (Bernardo, Marco; Cimatti, Alessandro, eds.) (Lecture Notes in Computer Science), Volume 3965, Springer-Verlag, Bertinoro, Italy (2006), pp. 211-242

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

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

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

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

[29] Jevons, William Stanley 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] Kaufmann, Matt; Moore, J S. 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] Mahboubi, Assia 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] Mahboubi, Assia; Melquiond, Guillaume; Sibut-Pinote, Thomas Formally Verified Approximations of Definite Integrals (2017) (Under review) | HAL | Zbl

[33] Martin-Dorel, Erik; Roux, Pierre 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, ACM, http ://www.acm.org/ (2017), pp. 90-99 | DOI

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

[35] Milner, Robin Lcf : A way of doing proofs with a machine, Mathematical Foundations of Computer Science 1979 (Bečvář, Jiří, ed.), Springer Berlin Heidelberg, Berlin, Heidelberg (1979), pp. 146-159 | DOI | Zbl

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

[37] Nipkow, Tobias; Bauer, Gertrud; Schultz, Paula 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] Nipkow, Tobias; Wenzel, Markus; Paulson, Lawrence C. Isabelle/HOL : A Proof Assistant for Higher-order Logic, Springer-Verlag, Berlin, Heidelberg, 2002 | Zbl

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

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

[41] Tucker, Warwick 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] Univalent Foundations Program, The Homotopy Type Theory : Univalent Foundations of Mathematics, https://homotopytypetheory.org/book, Institute for Advanced Study, 2013 | Zbl

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

[44] Wiedijk, Freek 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 :