EN FR
EN FR


Bibliography

Major publications by the team in recent years
  • 1A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, R. Saillard.

    Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system, in: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi SAd, Serbia, May 2016.

    https://hal-mines-paristech.archives-ouvertes.fr/hal-01441751
  • 2F. 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/
  • 3F. Blanqui, J.-P. Jouannaud, A. Rubio.

    The Computability Path Ordering, in: Logical Methods in Computer Science, October 2015. [ DOI : 10.2168/LMCS-11(4:3)2015 ]

    https://hal.inria.fr/hal-01163091
  • 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.
  • 5D. 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.
  • 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

Articles in International Peer-Reviewed Journals

Invited Conferences

  • 12G. Dowek.

    Analyzing individual proofs as the basis of interoperability between proof systems, in: PxTP 2017 - Fifth Workshop on Proof eXchange for Theorem Proving, Brasilia, Brazil, September 2017.

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

International Conferences with Proceedings

  • 13A. Díaz-Caro, G. Dowek.

    Typing Quantum Superpositions and Measurement, in: TPNC 2017 - 6th International Conference on the Theory and Practice of Natural Computing, Prague, Czech Republic, C. Martín-Vide, R. Neruda, M. A. Vega-Rodríguez (editors), Lecture Notes in Computer Science, Springer, December 2017, vol. 10687, 13 p, https://arxiv.org/abs/1601.04294. [ DOI : 10.1007/978-3-319-71069-3_22 ]

    https://hal.inria.fr/hal-01670387
  • 14F. Gilbert.

    Automated Constructivization of Proofs, in: FoSSaCS 2017, Uppsala, Sweden, April 2017. [ DOI : 10.1007/978-3-662-54458-7_28 ]

    https://hal.inria.fr/hal-01516788
  • 15F. Gilbert.

    Proof certificates in PVS, in: ITP 2017, Brasilia, Brazil, September 2017. [ DOI : 10.1007/978-3-319-66107-0_17 ]

    https://hal.inria.fr/hal-01673517
  • 16J.-P. Jouannaud, P.-Y. Strub.

    Coq without Type Casts: A Complete Proof of Coq Modulo Theory, in: LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 2017.

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

Scientific Popularization

Other Publications

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

    Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions, Springer-Verlag, 2004.
  • 28F. Bobot, J.-C. Filliâtre, C. Marché, A. Paskevich.

    Why3: Shepherd Your Herd of Provers, in: First International Workshop on Intermediate Verification Languages, 2011.

    http://hal.inria.fr/hal-00790310
  • 29M. Boespflug.

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

    A Theory Independent Curry-de Bruijn-howard Correspondence, in: Proceedings of the 39th International Colloquium Conference on Automata, Languages, and Programming - Volume Part II, Berlin, Heidelberg, ICALP'12, Springer-Verlag, 2012, pp. 13–15.

    http://dx.doi.org/10.1007/978-3-642-31585-5_2
  • 31R. Harper, F. Honsell, G. Plotkin.

    A Framework for Defining Logics, in: Journal of the association for computing machinery, 1993, pp. 194–204.
  • 32J. 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
  • 33J. Hughes, L. Pareto, A. Sabry.

    Proving the correctness of reactive systems using sized types, in: Proceedings of the 23th ACM Symposium on Principles of Programming Languages, 1996.

    http://doi.org/10.1145/237721.240882
  • 34C. S. Lee, N. D. Jones, A. M. Ben-Amram.

    The size-change principle for program termination, in: Proceedings of the 28th ACM Symposium on Principles of Programming Languages, 2001.
  • 35R. Lepigre.

    PML2, programming language with support for program proofs, 2017, Submitted for the post-proceedings of TYPES.

    https://lepigre.fr/files/docs/lepigre2017_pml2.pdf
  • 36R. Lepigre.

    Lambdapi, implementation of the λΠ-calculus modulo rewriting, 2017.

    https://github.com/rlepigre/lambdapi
  • 37R. Lepigre.

    Semantics and Implementation of an Extension of ML for program proving, Université Grenoble Alpes, France, 2017.

    https://github.com/rlepigre/phd/blob/master/manuscript_archived.pdf
  • 38R. Lepigre, C. Raffalli.

    Bindlib, representation of binders in OCaml, 2015.

    https://github.com/rlepigre/ocaml-bindlib
  • 39R. Lepigre, C. Raffalli.

    Practical Subtyping for System F with Sized (Co-)Induction, 2017, Submitted to the TOPLAS journal (under revision).

    http://lepigre.fr/files/docs/subtyping2017.pdf
  • 40D. Wahlstedt.

    Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion, Chalmers University of Technology, 2007, ISBN 978-91-7291-979-2.

    http://www.cse.chalmers.se/alumni/davidw/wdt_phd_printed_version.pdf