@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, in Journées Nationales de Calcul Formel. 22 – 26 Janvier 2018, Les cours du CIRM, no. 1 (2018), Talk no. 2, 10 p. doi : 10.5802/ccirm.27. http://archive.numdam.org/articles/10.5802/ccirm.27/
[1] 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] Interactive Theorem Proving and Program Development : Coq’Art The Calculus of Inductive Constructions, Springer Publishing Company, Incorporated, 2010 | Zbl
[3] 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] 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] 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] L’architecture des mathématiques, Les grands courants de la pensée mathématique (Lionnais, François Le, ed.), Cahiers du Sud, 1948
[7] 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] 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] 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] Structured type theory, Workshop on Logical Frameworks and Metalanguages (1999)
[11] 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] 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] 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] 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] 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] Proving Divide and Conquer Complexities in Isabelle/HOL, J. Autom. Reason., Volume 58 (2017) no. 4, pp. 483-508 | DOI | MR | Zbl
[17] Ü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] A compiled implementation of strong reduction, International Conference on Functional Programming 2002, ACM Press (2002), pp. 235-246 | Zbl
[19] 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] A formal proof of the Kepler conjecture, Forum of Mathematics, Pi, Volume 5 (2017) | DOI | MR | Zbl
[21] A proof of the Kepler conjecture, Annals of Mathematics, Volume 162 (2005) no. 3, pp. 1065-1185 | DOI | MR | Zbl
[22] 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] 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] 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] 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] A Skeptic’s Approach to Combining HOL and Maple, J. Autom. Reason., Volume 21 (1998) no. 3, pp. 279-294 | DOI | MR | Zbl
[27] Schur Number Five, https://arxiv.org/abs/1711.08076, 2018 (Accepted for publication at AAAI 2018)
[28] 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] 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] 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] 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] Formally Verified Approximations of Definite Integrals (2017) (Under review) | HAL | Zbl
[33] 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] Intuitionistic type theory, Studies in proof theory, Bibliopolis, 1984 https://books.google.fr/books?id=_D0ZAQAAIAAJ
[35] 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] 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] Isabelle/HOL : A Proof Assistant for Higher-order Logic, Springer-Verlag, Berlin, Heidelberg, 2002 | Zbl
[39] Formal Computations and Methods, University of Pittsburgh (2012) (Ph. D. Thesis) | MR
[40] The MIZAR-QC/6000 logic information language, Association for Literary and Linguistic Computing Bulletin, Volume 6 (1978), pp. 136-140
[41] 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] Homotopy Type Theory : Univalent Foundations of Mathematics, https://homotopytypetheory.org/book, Institute for Advanced Study, 2013 | Zbl
[43] Checking Landau’s « Grundlagen » in the automath system, Mathematical Centre tracts, Mathematisch Centrum, 1979 https://books.google.fr/books?id=xwjwngEACAAJ | Zbl
[44] 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
Cited by Sources: