1. Recherche
23 résultats  enregistrer la recherche
...
inria-00515548v4  Article dans une revue
Georges Gonthier, Assia Mahboubi. An introduction to small scale reflection in Coq
Journal of Formalized Reasoning, ASDD-AlmaDL, 2010, 3 (2), pp.95-152
...
hal-01363284v1  Article dans une revue
Assia Mahboubi. Machine-checked mathematics
Nieuw Archief voor Wiskunde, Richard Boucherie, 2016, 5/17 (3), pp.5. <http://www.nieuwarchief.nl/serie5/pdf/naw5-2016-17-3-172.pdf>
...
inria-00368403v2  Communication dans un congrès
François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau. Packaging Mathematical Structures
Tobias Nipkow and Christian Urban. Theorem Proving in Higher Order Logics, 2009, Munich, Germany. Springer, 5674, 2009, Lecture Notes in Computer Science
...
hal-01426164v3  Pré-publication, Document de travail
Henri Lombardi, Assia Mahboubi. Théories géométriques pour l'algèbre des nombres réels
2017
...
hal-00854426v1  Communication dans un congrès
Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi. A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus
Alberto Momigliano and Brigitte Pientka and Randy Pollack. LFMTP - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - 2013, Sep 2013, Boston, United States. ACM, 2013, <10.1145/2503887.2503892>
...
inria-00604656v1  Pré-publication, Document de travail
Jade Alglave, Assia Mahboubi. A Generic Formalised Framework for Reasoning About Weak Memory Models
2011
...
hal-00825074v3  Communication dans un congrès
Assia Mahboubi. The Rooster and the Butterflies
Jacques Carette and David Aspinal and Christopher Lange and Petr Sojka and Wolfgang Windsteiger. CICM 2013 - Conference on Intelligent Computer Mathematics - 2013, Jul 2013, Bath, United Kingdom. Springer, 7961, pp.1-18, 2013, Lecture Notes in Artificial Intelligence. <10.1007/978-3-642-39320-4_1>
...
hal-00690392v1  Pré-publication, Document de travail
Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi. Simulating the DPLL(T ) procedure in a sequent calculus with focusing
2012
...
hal-00690044v1  Rapport
Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi. Two simulations about DPLL(T)
2012
...
hal-01289616v2  Communication dans un congrès
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals
Jasmin Christian Blanchette; Stephan Merz. Interactive Theorem Proving, Aug 2016, Nancy, France. 9807, 2016, Lecture Notes in Computer Science. <https://itp2016.inria.fr/>. <10.1007/978-3-319-43144-4_17>
...
hal-00687640v2  Communication dans un congrès
François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Assia Mahboubi et al.  A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
Bernhard Gramlich and Dale Miller and Uli Sattler. 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.67-81, 2012, <10.1007/978-3-642-31365-3_8>
...
hal-00816699v1  Communication dans un congrès
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen et al.  A Machine-Checked Proof of the Odd Order Theorem
Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.163-179, 2013, LNCS. <10.1007/978-3-642-39634-2_14>
...
hal-00984057v1  Communication dans un congrès
Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi. A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
ITP - 5th International Conference on Interactive Theorem Proving, 2014, Vienna, Austria. 2014
hal-01107944v1  Communication dans un congrès
Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Jean-Marc Notin, Assia Mahboubi. Axiomatic constraint systems for proof search modulo theories
C. Lutz and S. Ranise. 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), Sep 2015, Wroclaw, Poland. Springer, Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), 9322, 2014, LNAI. <10.1007/978-3-319-24246-0_14>
hal-01107941v1  Communication dans un congrès
Assia Mahboubi. Computer-checked mathematics: a formal proof of the odd order theorem
The Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2014, Vienna, Austria. <10.1145/2603088.2603090>
...
inria-00464237v3  Communication dans un congrès
Cyril Cohen, Assia Mahboubi. A formal quantifier elimination for algebraically closed fields
Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, 6167, pp.189-203, 2010, Computer Science; Intelligent Computer Mathematics. <10.1007/978-3-642-14128-7_17>
...
hal-00816703v2  Communication dans un congrès
Assia Mahboubi, Enrico Tassi. Canonical Structures for the working Coq user
Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.19-34, 2013, LNCS. <10.1007/978-3-642-39634-2_5>
...
inria-00258384v17  Rapport
Georges Gonthier, Assia Mahboubi, Enrico Tassi. A Small Scale Reflection Extension for the Coq system
[Research Report] RR-6455, Inria Saclay Ile de France. 2016
hal-00935057v1  Ouvrage (y compris édition critique et traduction)
Peter Aczel, Benedikt Ahrens, Thorsten Altenkirch, Steve Awodey, Bruno Barras et al.  Homotopy Type Theory: Univalent Foundations of Mathematics
Aucun, pp.448, 2013
...
hal-01376054v1  Article dans une revue
Assia Mahboubi. An Induction Principle over Real Numbers
Archive for Mathematical Logic, Springer Verlag, 2016, <10.1007/s00153-016-0513-8>
...
inria-00593738v4  Article dans une revue
Cyril Cohen, Assia Mahboubi. Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (1:02), pp.1-40. <10.2168/LMCS-8 (1:02) 2012>
...
inria-00503017v2  Article dans une revue
Yves Bertot, Frédérique Guilhot, Assia Mahboubi. A formal study of Bernstein coefficients and polynomials
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2011, 21 (04), pp.731-761. <10.1017/S0960129511000090>

Contact


archive-ouverte@inria.fr