85 5.4.3 Définition de l'ensemble des clauses d'une preuve Spike, p.89 ,
98 6.1.1 Motivations, p.98 ,
118 7.1.1 Motivations, Perspectives : construction interactive des preuves par récurrence implicite à la Spike dans Coq Sommaire 7.1 Présentation générale de l'environnement, p.118 ,
Binary Decision Diagrams, IEEE Transactions on Computers, vol.27, issue.6, pp.27509-516, 1978. ,
DOI : 10.1109/TC.1978.1675141
Extrait du Fakhri traite d'algebre (manuscript 952, supplement arabe de la Bibliotheque imperiale ) par Abou Bekr Mohammed Ben Alhacan Alkarkhi, 1853. ,
ELAN for equational reasoning in Coq, Proceedings of 2nd Workshop on Logical Frameworks and Metalanguages . Institut National de Recherche en Informatique et en Automatique, pp.2-7261, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00107864
Term rewriting and all that, 1998. ,
Fix-Point Equations for Well-Founded Recursion in Type Theory, Theorem Proving in Higher Order Logics, pp.1-16, 2000. ,
DOI : 10.1007/3-540-44659-1_1
Satisfiability Modulo Theories, Frontiers in Artificial Intelligence and Applications, vol.185, pp.825-885, 2009. ,
URL : https://hal.archives-ouvertes.fr/hal-01095009
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant, Functional and Logic Programming, 8th International Symposium, FLOPS 2006 Proceedings, rédacteurs Masami Hagiya et Philip Wadler de Lecture Notes in Computer Science, pp.114-129, 2006. ,
DOI : 10.1023/A:1019916231463
URL : https://hal.archives-ouvertes.fr/inria-00564237
Validation of the JavaCard Platform with Implicit Induction Techniques, Proceedings of 14th International Conference, Rewriting Techniques and Applications, RTA 2003 rédacteur Robert Nieuwenhuis, volume 2706 de Lecture Notes in Computer Science, pp.337-351, 2003. ,
DOI : 10.1007/3-540-44881-0_24
Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions, 2004. ,
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237
Automated Proof Construction in Type Theory Using Resolution, J. Autom. Reasoning, vol.29, pp.3-4253, 2002. ,
DOI : 10.1007/10721959_10
Sledgehammer: Judgement Day, Proceedings of 5th International Joint Conference rédacteurs Jürgen Giesl et Reiner Hähnle, pp.107-121, 2010. ,
DOI : 10.1007/978-3-642-14203-1_9
An Overview of ELAN, Electronic Notes in Theoretical Computer Science, vol.15, pp.55-70, 1998. ,
DOI : 10.1016/S1571-0661(05)82552-6
Adel Bouhoula, Emmanuel Kounalis et Michaël Rusinowitch, Automated Mathematical Induction. J. Log. Comput, vol.5, issue.5, pp.631-668, 1995. ,
Preuves automatiques par récurrence dans les théories conditionnelles, Thèse de doctorat, 1994. ,
A Brief Overview of Agda -A Functional Language with Dependent Types Theorem Proving in Higher Order Logics, Proceedings of 22nd International Conference de Lecture Notes in Computer Science, pp.73-78, 2009. ,
A Computational Logic Handbook, 1988. ,
Integrating decision procedures into heuristic theorem provers : a case study of linear arithmetic, pp.83-124, 1988. ,
Emancipate yourself from LTac : Your first Coq plugin. http: //gallium.inria.fr/blog/your-first-coq-plugin, p.2012 ,
Précis des oeuvres mathématiques de Pierre Fermat et de l ,
Proving Properties of Programs by Structural Induction, The Computer Journal, vol.12, issue.1, pp.41-48, 1969. ,
DOI : 10.1093/comjnl/12.1.41
Handbook of proof theory, 1998. ,
An introduction to proof theory. Handbook of proof theory, pp.1-78, 1998. ,
Certified Programming with Dependent Types, 2011. ,
Clarke, Orna Grumberg et Doron Peled. Model checking, 2001. ,
Certification of Automated Termination Proofs, Proceedings of 6th International Symposium on Frontiers of Combining Systems, pp.148-162, 2007. ,
DOI : 10.1007/978-3-540-74621-8_10
URL : https://hal.archives-ouvertes.fr/hal-01125312
Facettes de la preuve. Habilitation à diriger des recherches, 2014. ,
URL : https://hal.archives-ouvertes.fr/tel-01089490
The calculus of constructions, Information and Computation, vol.76, issue.2-3, pp.95-120, 1988. ,
DOI : 10.1016/0890-5401(88)90005-3
URL : https://hal.archives-ouvertes.fr/inria-00076024
First-Order Reasoning in the Calculus of Inductive Constructions, Lecture Notes in Computer Science, vol.3085, pp.162-177, 2003. ,
DOI : 10.1007/978-3-540-24849-1_11
Proof reconstruction. Rapport technique, LIP, 1996. ,
A Tactic Language for the System Coq Logic for Programming and Automated Reasoning, Proceedings of 7th International Conference, pp.85-95, 1955. ,
Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982. ,
DOI : 10.1016/0304-3975(82)90026-3
Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol.475, issue.03, pp.795-807, 1992. ,
DOI : 10.1007/3-540-54487-9_58
Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-210, 1935. ,
DOI : 10.1007/BF01201353
Edinburgh LCF : a mechanized logic of computation, Lecture Notes in Computer Science, vol.78, 1979. ,
DOI : 10.1007/3-540-09724-4
Reachability Programming in HOL98 Using BDDs Theorem Proving in Higher Order Logics, Proceedings of 13th International Conference rédacteurs Mark Aagaard et John Harrison, volume 1869 de Lecture Notes in Computer Science, pp.179-196, 2000. ,
Strategic Issues, Problems and Challenges in Inductive Theorem Proving, Electronic Notes in Theoretical Computer Science, vol.125, issue.2, pp.5-43, 2005. ,
DOI : 10.1016/j.entcs.2005.01.006
Performing Implicit Induction Reasoning with Certifying Proof Environments, Proceedings of 4th International Symposium on Symbolic Computation in Software Science, pp.15-17, 2012. ,
DOI : 10.1093/jigpal/12.1.1
URL : https://hal.archives-ouvertes.fr/hal-00764909
Fast Tactic-Based Theorem Proving Theorem Proving in Higher Order Logics, Proceedings of 13th International Conference rédacteurs Mark Aagaard et John Harrison, volume 1869 de Lecture Notes in Computer Science, pp.252-267, 2000. ,
The formulas-as-types notion of construction Curry : Essays on Combinatory Logic, Lambda Calculus, and Formalism, J. P. Seldin et J. R. Hindley, pp.479-490, 1980. ,
Integrating Gandalf and HOL, Proceedings 12th International Conference Theorem Proving in Higher Order Logics, TPHOLs'99, pp.311-322, 1999. ,
DOI : 10.1007/3-540-48256-3_21
First-order proof tactics in higher-order logic theorem provers. Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports, pp.56-68, 2003. ,
INKA : The Next Generation. Dans Automated Deduction -CADE-13, Proceedings of 13th International Conference on Automated Deduction, pp.288-292, 1996. ,
Validation des preuves par récurrence implicite avec des outils basés sur le calcul des constructions inductives, 2005. ,
Integrating automated and interactive theorem proving in type theory, AVOCS, vol.2, 2010. ,
Agda as a platform for the development of verified railway interlocking systems, Thèse de doctorat, 2012. ,
seL4, Communications of the ACM, vol.53, issue.6, pp.53107-115, 2010. ,
DOI : 10.1145/1743546.1743574
Simple Word Problems in Universal Algebras, Automation of Reasoning, pp.342-376, 1983. ,
DOI : 10.1007/978-3-642-81955-1_23
Mechanizing inductive reasoning, Bulletin of the EATCS, vol.41, pp.216-226, 1990. ,
The Nuprl Proof Development System, Version 5 : Reference Manual and User's Guide, 2002. ,
Didier Rémy et Jérôme Vouillon. The OCaml system release 4, p.2, 2014. ,
Correctness of a compiler for arithmetic expressions, Mathematical aspects of computer science, vol.1, 1967. ,
DOI : 10.1090/psapm/019/0242403
A basis for a mathematical theory of computation, Studies in Logic and the Foundations of Mathematics, pp.33-70, 1959. ,
Automation for interactive proof: First prototype, Information and Computation, vol.204, issue.10, pp.1575-1596, 2006. ,
DOI : 10.1016/j.ic.2005.05.010
On Proving Inductive Properties of Abstract Data Types, Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, pp.154-162, 1980. ,
User Guide for the PVS Specification and Verification System (Beta Release), 1993. ,
Pascal : oeuvres complètes, 1963. ,
Inductive definitions in the system Coq rules and properties, Proceedings of International Conference on Typed Lambda Calculi and Applications, TLCA '93, pp.328-345, 1993. ,
DOI : 10.1007/BFb0037116
Formulaire de mathématiques, Bocca frères, vol.5, 1908. ,
La science et l'hypothèse, Science, vol.6, pp.1-13, 1898. ,
Lazy generation of induction hypotheses, Proceedings of 12th International Conference on Automated Deduction, pp.42-56, 1994. ,
DOI : 10.1007/3-540-58156-1_4
Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm, Proceedings of 12th International Conference, Computer Aided Verification, pp.344-357, 2000. ,
DOI : 10.1007/10722167_27
URL : https://hal.archives-ouvertes.fr/inria-00099167
Michaël Rusinowitch, Sorin Stratulat et Francis Klay Mechanical verification of an ideal incremental ABR conformance algorithm, J. Autom. Reasoning, vol.30, issue.2, pp.53-177, 2003. ,
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants, Proceedings of 1st International Joint Conference, Automated Reasoning, 2001. ,
DOI : 10.1007/3-540-45744-5_34
Preuves par récurrence avec ensembles couvrants contextuels. Applications á la vérification de logiciels de télécommunications, Thèse de doctorat, 2000. ,
A General Framework to Build Contextual Cover Set Induction Provers, Journal of Symbolic Computation, vol.32, issue.4, pp.403-445, 2001. ,
DOI : 10.1006/jsco.2000.0469
URL : https://hal.archives-ouvertes.fr/inria-00100927
The CADE-16 ATP System Competition, Journal of Automated Reasoning, vol.24, issue.3, pp.371-396, 2000. ,
DOI : 10.1023/A:1006393501098
The collected papers of Gerhard Gentzen, 1969. ,
Reasoning [The HOL development team] The HOL development team. The HOL System TUTORIAL. http://hol.sourceforge.net/. [The ISABELLE development team] The ISABELLE development team. ISABELLE. http: //isabelle.in.tum.de/. [The PROOFTREE development team] The PROOFTREE development team. PROOFTREE. http://askra.de/software/prooftree/. [The PVS development team] The PVS development team, pp.199-204, 1997. ,
Descente infinie proofs in Coq, Proceedings of the 1st Coq Workshop, 2009. ,
Descente Infinie + Deduction, Logic Journal of IGPL, vol.12, issue.1, pp.1-96, 2004. ,
DOI : 10.1093/jigpal/12.1.1