EN FR
EN FR


previous Previous | up Home


Bibliography

Major publications by the team in recent years
  • 1F. Blanqui.

    Definitions by rewriting in the Calculus of Constructions, in: Mathematical Structures in Computer Science, 2005, vol. 15, no 1, pp. 37-92. [ DOI : 10.1017/S0960129504004426 ]

    http://hal.inria.fr/inria-00105648/en/
  • 2F. Blanqui, A. Koprowski.

    CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, in: Mathematical Structures in Computer Science, 2011, vol. 21, no 4, pp. 827-859.

    http://hal.inria.fr/inria-00543157/en/
  • 3M. Boespflug.

    Conception d'un noyau de vérification de preuves pour le lambda-Pi-calcul modulo, École Polytechnique, 2011.
  • 4G. Burel.

    Experimenting with Deduction Modulo, in: CADE 2011, V. Sofronie-Stokkermans, N. Bjørner (editors), Lecture Notes in Artificial Intelligence, Springer, 2011, vol. 6803, pp. 162–176.
  • 5G. Dowek.

    Polarized Resolution Modulo, in: IFIP Theoretical Computer Science, 2010.
  • 6G. Dowek, T. Hardin, C. Kirchner.

    Theorem proving modulo, in: Journal of Automated Reasoning, 2003, vol. 31, pp. 33-73.
  • 7C. Dubois, T. Hardin, V. Donzeau-Gouge.

    Building certified components within FOCAL, in: Revised Selected Papers from the Fifth Symposium on Trends in Functional Programming, TFP 2004, München, Germany, 25-26 November 2004, H.-W. Loidl (editor), Trends in Functional Programming, Intellect, 2006, vol. 5, pp. 33-48.
  • 8O. Hermant.

    Resolution is Cut-Free, in: Journal of Automated Reasoning, March 2010, vol. 44, no 3, pp. 245-276.
  • 9M. Jacquel, K. Berkani, D. Delahaye, C. Dubois.

    Verifying B Proof Rules using Deep Embedding and Automated Theorem Proving, in: Software and Systems Modeling (SoSyM), June 2013.
  • 10M. Jacquel, K. Berkani, D. Delahaye, C. Dubois.

    Tableaux Modulo Theories Using Superdeduction, in: Global Journal of Advanced Software Engineering (GJASE), December 2014, vol. 1, pp. 1 - 13. [ DOI : 10.1007/978-3-642-31365-3_26 ]

    https://hal.archives-ouvertes.fr/hal-01099338
Publications of the year

Doctoral Dissertations and Habilitation Theses

  • 11R. Cauderlier.

    Object-Oriented Mechanisms for Interoperability between Proof Systems, Conservatoire National Des Arts et Métiers, Paris, October 2016.

    https://hal.inria.fr/tel-01415945
  • 12P. Halmagrand.

    Automated Deduction and Proof Certification for the B Method, Conservatoire National Des Arts et Métiers, Paris, December 2016.

    https://hal.inria.fr/tel-01420460

Articles in International Peer-Reviewed Journals

  • 13P. Arrighi, G. Dowek.

    Free fall and cellular automata, in: Electronic Proceedings in Theoretical Computer Science, 2016, vol. 204, pp. 1 - 10. [ DOI : 10.4204/EPTCS.204.1 ]

    https://hal.inria.fr/hal-01421712

International Conferences with Proceedings

  • 14P. Arrighi, S. Martiel, S. Perdrix.

    Reversible Causal Graph Dynamics, in: Reversible Computation, Bologna, Italy, Lecture Notes in Computer Science, July 2016, vol. 9720, pp. 73-88. [ DOI : 10.1007/978-3-319-40578-0_5 ]

    https://hal.archives-ouvertes.fr/hal-01361427
  • 15R. Cauderlier.

    A Rewrite System for Proof Constructivization, in: Workshop on Logical Frameworks and Meta-Languages: Theory and Practice 2016, Porto, Portugal, June 2016, pp. 1 - 7. [ DOI : 10.1145/2966268.2966270 ]

    https://hal.inria.fr/hal-01420634
  • 16R. Cauderlier, C. Dubois.

    ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti, in: 13th ICTAC International Colloquium on Theoretical Aspects of Computing, Taipei, Taiwan, October 2016, pp. 459 - 468. [ DOI : 10.1007/978-3-319-46750-4_26 ]

    https://hal.inria.fr/hal-01420638
  • 17P. Halmagrand.

    Soundly Proving B Method Formulae Using Typed Sequent Calculus, in: 13th International Colloquium on Theoretical Aspects of Computing (ICTAC), Taipei, Taiwan, A. Sampaio, F. Wang (editors), Lecture Notes in Computer Science, Springer International Publishing, October 2016, vol. 9965, pp. 196-213. [ DOI : 10.1007/978-3-319-46750-4_12 ]

    https://hal.archives-ouvertes.fr/hal-01342849

Conferences without Proceedings

  • 18A. Assaf, G. Dowek, J.-P. Jouannaud, J. Liu.

    Encoding Proofs in Dedukti: the case of Coq proofs, in: Proceedings Hammers for Type Theories, Coimbra, Portugal, Proc. Higher-Order rewriting Workshop, Easy Chair, July 2016.

    https://hal.inria.fr/hal-01330980
  • 19A. Assaf, G. Dowek, J.-P. Jouannaud, J. Liu.

    Untyped Confluence in Dependent Type Theories, in: Proceedings Higher-Order Rewriting Workshop, Porto, Portugal, Proc. Higher-Order rewriting Workshop, Easy-Chair, June 2016.

    https://hal.inria.fr/hal-01330955
  • 20K. Ji.

    Resolution in Solving Graph Problems, in: 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), Toronto, Canada, July 2016.

    https://hal.archives-ouvertes.fr/hal-01245138
  • 21S. Wang.

    Higher Order Proof Engineering: Proof Collaboration, Transformation, Checking and Retrieval, in: AITP 2016 - Conference on Artificial Intelligence and Theorem Proving, Obergurgl, Austria, April 2016.

    https://hal.inria.fr/hal-01250197

Other Publications

References in notes
  • 26Y. Bertot, P. Castéran.

    Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions, Springer-Verlag, 2004.
  • 27D. Cousineau, G. Dowek.

    Embedding Pure Type Systems in the lambda-Pi-calculus modulo, in: Typed lambda calculi and applications, S. Ronchi della Rocca (editor), Lecture Notes in Computer Science, Springer-Verlag, 2007, vol. 4583, pp. 102-117.
  • 28D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, O. Hermant.

    Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps, in: IWIL - 10th International Workshop on the Implementation of Logics - 2013, Stellenbosch, South Africa, S. Schulz, G. Sutcliffe, B. Konev (editors), EasyChair, December 2013.

    https://hal.inria.fr/hal-00909688
  • 29D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, O. Hermant.

    Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo, in: LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Stellenbosch, South Africa, K. McMillan, A. Middeldorp, A. Voronkov (editors), Springer, December 2013, vol. 8312, pp. 274-290. [ DOI : 10.1007/978-3-642-45221-5_20 ]

    https://hal.inria.fr/hal-00909784
  • 30D. Delahaye, M. Jacquel.

    Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction, in: electronic Journal of Mathematics and Technology, February 2013, vol. 7, no 2, pp. 1 - 20.

    https://hal.archives-ouvertes.fr/hal-01099371
  • 31R. Gandy.

    Church's Thesis and Principles for Mechanisms, in: The Kleene Symposium, North-Holland, 1980.
  • 32R. Harper, F. Honsell, G. Plotkin.

    A Framework for Defining Logics, in: Journal of the association for computing machinery, 1993, pp. 194–204.
  • 33J. Harrison.

    HOL Light: An Overview, in: Theorem Proving in Higher Order Logics, S. Berghofer, T. Nipkow, C. Urban, M. Wenzel (editors), Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2009, vol. 5674, pp. 60-66.

    http://dx.doi.org/10.1007/978-3-642-03359-9_4
  • 34M. Jacquel, K. Berkani, D. Delahaye, C. Dubois.

    Verifying B Proof Rules using Deep Embedding and Automated Theorem Proving, in: Software Engineering and Formal Methods, November 2011, vol. 7041, pp. 253-268. [ DOI : 10.1007/978-3-642-24690-6_18 ]

    https://hal.archives-ouvertes.fr/hal-00722373
  • 35M. Jacquel, K. Berkani, D. Delahaye, C. Dubois.

    Tableaux Modulo Theories Using Superdeduction, in: Global Journal of Advanced Software Engineering (GJASE), December 2014, vol. 1, pp. 1 - 13. [ DOI : 10.1007/978-3-642-31365-3_26 ]

    https://hal.archives-ouvertes.fr/hal-01099338
  • 36K. Korovin.

    iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description), in: IJCAR, A. Armando, P. Baumgartner (editors), Lecture Notes in Artificial Intelligence, Springer, 2008, vol. 5195, pp. 292-298.
  • 37F. Rabe, M. Kohlhase.

    A Scalable Module System, in: Inf. Comput., September 2013, vol. 230, pp. 1–54.

    http://dx.doi.org/10.1016/j.ic.2013.06.001


previous Previous | up Home