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, n^o 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, n^o 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, n^o 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

• 11K. Q. Ly.
  
  Automated verification of termination certificates, Université Joseph Fourier, October 2014.
  
  https://hal.inria.fr/tel-01097793

Articles in International Peer-Reviewed Journals

• 12A. Assaf, A. Díaz-Caro, S. Perdrix, C. Tasson, B. Valiron.
  
  Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus, in: Logical Methods in Computer Science, December 2014, vol. 10:4, n^o 8, 40 p. [ DOI : 10.2168/LMCS-10(4:8)2014 ]
  
  https://hal.inria.fr/hal-01097602
• 13M. 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

Invited Conferences

• 14G. Dowek.
  
  Deduction modulo theory, in: All about proofs. Proofs for all., Wien, Austria, July 2014.
  
  https://hal.inria.fr/hal-01101829

International Conferences with Proceedings

• 15G. Burel.
  
  Cut Admissibility by Saturation, in: Joint International Conference, RTA-TLCA, Vienna, Austria, G. Dowek (editor), Lecture Notes in Computer Science, Springer, July 2014, vol. 8560, pp. 124-138. [ DOI : 10.1007/978-3-319-08918-8_9 ]
  
  https://hal.inria.fr/hal-01097428
• 16S. Cruanes.
  
  Logtk : A Logic ToolKit for Automated Reasoning and its Implementation, in: 4th Workshop on Practical Aspects of Automated Reasoning, Vienna, Austria, July 2014.
  
  https://hal.inria.fr/hal-01101057

Conferences without Proceedings

• 17P. Halmagrand.
  
  Using Deduction Modulo in Set Theory, in: SETS14, 1st International Workshop about Sets and Tools, Toulouse, France, June 2014, 12 p.
  
  https://hal.inria.fr/hal-01100512

Other Publications

• 18A. Assaf.
  
  A calculus of constructions with explicit subtyping, 2014.
  
  https://hal.archives-ouvertes.fr/hal-01097401
• 19A. Assaf, G. Burel.
  
  Translating HOL to Dedukti, 2014.
  
  https://hal.archives-ouvertes.fr/hal-01097412
• 20F. Blanqui.
  
  A point on fixpoints in posets, January 2014.
  
  https://hal.inria.fr/hal-01097809
• 21R. Cauderlier, C. Dubois.
  
  Objects and subtyping in the λΠ-calculus modulo, December 2014.
  
  https://hal.inria.fr/hal-01097444
• 22G. Dowek.
  
  Models and termination of proof-reduction in the λΠ-calculus modulo theory, January 2015.
  
  https://hal.inria.fr/hal-01101834
• 23G. Dowek, Y. Jiang.
  
  A Logical Approach to CTL, January 2014.
  
  https://hal.inria.fr/hal-00919467
• 24G. Dowek, Y. Jiang.
  
  Axiomatizing truth in a finite model, January 2014.
  
  https://hal.inria.fr/hal-00919469
• 25G. Dowek, Y. Jiang.
  
  Cut-elimination and the decidability of reachability in alternating pushdown systems, January 2015.
  
  https://hal.inria.fr/hal-01101835
• 26A. Díaz-Caro, G. Dowek.
  
  Simply Typed Lambda-Calculus Modulo Type Isomorphisms, August 2014.
  
  https://hal.inria.fr/hal-01109104
• 27R. Saillard.
  
  Dedukti : un vérificateur de preuves universel, June 2014, Journées de seconde année de l'Ecole Doctorale à Mines ParisTech.
  
  https://hal-mines-paristech.archives-ouvertes.fr/hal-01100519

References in notes

• 28A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi.
  
  A compact kernel for the calculus of inductive constructions, in: Sadhana, 2009, vol. 34, n^o 1, pp. 71-144.
  
  http://dx.doi.org/10.1007/s12046-009-0003-3
• 29L. Benthem Jutting, J. McKinna, R. Pollack.
  
  Checking algorithms for Pure Type Systems, in: Types for Proofs and Programs, H. Barendregt, T. Nipkow (editors), Lecture Notes in Computer Science, Springer Berlin Heidelberg, 1994, vol. 806, pp. 19-61.
• 30Y. Bertot, P. Castéran.
  
  Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions, Springer-Verlag, 2004.
• 31F. Blanqui.
  
  Terminaison des systèmes de réécriture d'ordre supérieur basée sur la notion de clôture de calculabilité, Université Paris-Diderot - Paris VII, July 2012, HDR.
  
  http://tel.archives-ouvertes.fr/tel-00724233
• 32D. 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.
• 33D. 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
• 34D. 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
• 35D. Delahaye, M. Jacquel.
  
  Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction, in: electronic Journal of Mathematics and Technology, February 2013, vol. 7, n^o 2, pp. 1 - 20.
  
  https://hal.archives-ouvertes.fr/hal-01099371
• 36R. Gandy.
  
  Church's Thesis and Principles for Mechanisms, in: The Kleene Symposium, North-Holland, 1980.
• 37J.-Y. Girard, Y. Lafont, P. Taylor.
  
  Proofs and Types, Cambridge University Press, 1988.
• 38R. Harper, F. Honsell, G. Plotkin.
  
  A Framework for Defining Logics, in: Journal of the association for computing machinery, 1993, pp. 194–204.
• 39J. 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
• 40L. M. Hines.
  
  STR$\dot{+}$VE$\subseteq$: The STR$\dot{+}$VE-Based Subset Prover, in: Conference on Automated Deduction (CADE), Kaiserslautern (Germany), LNCS, Springer, July 1990, pp. 193–206.
• 41J. Hurd.
  
  The OpenTheory Standard Theory Library, in: NASA Formal Methods, M. Bobaru, K. Havelund, G. Holzmann, R. Joshi (editors), Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2011, vol. 6617, pp. 177-191.
  
  http://dx.doi.org/10.1007/978-3-642-20398-5_14
• 42M. 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
• 43J.-P. Jouannaud, A. Rubio.
  
  Polymorphic Higher-Order Recursive Path Orderings, in: Journal of the ACM, 2007, vol. 54, n^o 1, pp. 1-48.
• 44J.-P. Jouannaud, A. Rubio.
  
  The Higher-Order Recursive Path Ordering, in: Proceedings of the 14th IEEE Symposium on Logic in Computer Science, 1999.
• 45A. Kersani, N. Peltier.
  
  Combining Superposition and Induction: A Practical Realization, in: FroCoS 2013 - 9th International Symposium on s of Combining Systems (co-located with TABLEAUX 2013), Nancy, France, P. Fontaine, C. Ringeissen, R. A. Schmidt (editors), Lecture Notes in Computer Science (LNCS), Springer, September 2013, vol. 8152, pp. 7-22, Session: Inductive Theorem Proving. [ DOI : 10.1007/978-3-642-40885-4_2 ]
  
  https://hal.archives-ouvertes.fr/hal-00934610
• 46K. 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.
• 47F. 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
• 48B. R. Salinas.
  
  Puntos fijos en conjuntos ordenados, Publicaciones del Seminario Matematico Garcia de Galdeano, Consejo Superior de Investigationes Cientificas, Facultad de Ciencas de Zaragoza, 1969, English summary on http://www.ams.org/mathscinet-getitem?mr=250943 .
• 49R. Statman.
  
  A New Type Assignment for Strongly Normalizable Terms, in: Computer Science Logic 2013 (CSL 2013), Dagstuhl, Germany, S. R. D. Rocca (editor), Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2013, vol. 23, pp. 634–652.